From 81544562287576151b3950c37e67aca976892478 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Tue, 1 Aug 2023 13:13:39 +0200 Subject: [PATCH] Move code --- quint/src/quintVerifier.ts | 48 +++++++++++++++++++------------------- 1 file changed, 24 insertions(+), 24 deletions(-) diff --git a/quint/src/quintVerifier.ts b/quint/src/quintVerifier.ts index ac385438b..9dc6450be 100644 --- a/quint/src/quintVerifier.ts +++ b/quint/src/quintVerifier.ts @@ -188,6 +188,30 @@ const grpcStubOptions = { oneofs: true, } +function loadProtoDefViaDistribution(dist: ApalacheDist): VerifyResult { + 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> { type ServerReflectionResponseSuccess = { file_descriptor_response: { @@ -265,30 +289,6 @@ async function loadProtoDefViaReflection(): Promise { - 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 { const protoDescriptor = grpc.loadPackageDefinition(protoDef) // The cast thru `unkown` lets us convince the type system of anything