Skip to content

Commit

Permalink
Move code
Browse files Browse the repository at this point in the history
  • Loading branch information
thpani committed Aug 1, 2023
1 parent f7c4912 commit 8154456
Showing 1 changed file with 24 additions and 24 deletions.
48 changes: 24 additions & 24 deletions quint/src/quintVerifier.ts
Original file line number Diff line number Diff line change
Expand Up @@ -188,6 +188,30 @@ const grpcStubOptions = {
oneofs: true,
}

function loadProtoDefViaDistribution(dist: ApalacheDist): VerifyResult<ProtoPackageDefinition> {
const jarUtilitiyIsInstalled = spawnSync('jar', ['--version']).status === 0
if (!jarUtilitiyIsInstalled) {
return err('The `jar` utility must be installed')
}

// The proto file we extract from the apalache jar
const protoFileName = 'cmdExecutor.proto'
// Used as the target for the extracted proto file
const tmpDir = fs.mkdtempSync(path.join(os.tmpdir(), 'apalache-proto-'))
const protoFile = path.join(tmpDir, protoFileName)

const protoIsFileExtracted = spawnSync('jar', ['xf', dist.jar, protoFileName], { cwd: tmpDir }).status === 0
if (!protoIsFileExtracted) {
return err(`Apalache distribution is corrupted. Could not extract proto file from apalache.jar.`)
}

const protoDef = proto.loadSync(protoFile, grpcStubOptions)
// We have the proto file loaded, so we can delete the tmp dir
fs.rmSync(tmpDir, { recursive: true, force: true })

return right(protoDef)
}

async function loadProtoDefViaReflection(): Promise<VerifyResult<ProtoPackageDefinition>> {
type ServerReflectionResponseSuccess = {
file_descriptor_response: {
Expand Down Expand Up @@ -265,30 +289,6 @@ async function loadProtoDefViaReflection(): Promise<VerifyResult<ProtoPackageDef
})
}

function loadProtoDefViaDistribution(dist: ApalacheDist): VerifyResult<ProtoPackageDefinition> {
const jarUtilitiyIsInstalled = spawnSync('jar', ['--version']).status === 0
if (!jarUtilitiyIsInstalled) {
return err('The `jar` utility must be installed')
}

// The proto file we extract from the apalache jar
const protoFileName = 'cmdExecutor.proto'
// Used as the target for the extracted proto file
const tmpDir = fs.mkdtempSync(path.join(os.tmpdir(), 'apalache-proto-'))
const protoFile = path.join(tmpDir, protoFileName)

const protoIsFileExtracted = spawnSync('jar', ['xf', dist.jar, protoFileName], { cwd: tmpDir }).status === 0
if (!protoIsFileExtracted) {
return err(`Apalache distribution is corrupted. Could not extract proto file from apalache.jar.`)
}

const protoDef = proto.loadSync(protoFile, grpcStubOptions)
// We have the proto file loaded, so we can delete the tmp dir
fs.rmSync(tmpDir, { recursive: true, force: true })

return right(protoDef)
}

function loadGrpcClient(protoDef: ProtoPackageDefinition): VerifyResult<AsyncCmdExecutor> {
const protoDescriptor = grpc.loadPackageDefinition(protoDef)
// The cast thru `unkown` lets us convince the type system of anything
Expand Down

0 comments on commit 8154456

Please sign in to comment.