diff --git a/quint/src/quintVerifier.ts b/quint/src/quintVerifier.ts index 8b412babb..d34626494 100644 --- a/quint/src/quintVerifier.ts +++ b/quint/src/quintVerifier.ts @@ -246,22 +246,18 @@ async function loadProtoDefViaReflection(): Promise - new Promise((resolve, reject) => { - const call = reflectionClient.ServerReflectionInfo() - call.on('data', (r: ServerReflectionResponse) => { - call.end() - resolve(r) - }) - call.on('error', (e: grpc.StatusObject) => reject(e)) + // Query reflection endpoint + return new Promise((resolve, reject) => { + const call = reflectionClient.ServerReflectionInfo() + call.on('data', (r: ServerReflectionResponse) => { + call.end() + resolve(r) + }) + call.on('error', (e: grpc.StatusObject) => reject(e)) - call.write({ file_containing_symbol: 'shai.cmdExecutor.CmdExecutor' }) - }) - ).then(response => + call.write({ file_containing_symbol: 'shai.cmdExecutor.CmdExecutor' }) + }).then(protoDefResponse => { // Construct a proto definition of the reflection response. - response.chain((protoDefResponse: ServerReflectionResponse) => { if ('error_response' in protoDefResponse) { return err( `Apalache gRPC endpoint is corrupted. Could not extract proto file: ${protoDefResponse.error_response.error_message}` @@ -275,8 +271,8 @@ async function loadProtoDefViaReflection(): Promise err(`Error querying reflection endpoint: ${error}`)) } function loadGrpcClient(protoDef: ProtoPackageDefinition): AsyncCmdExecutor { @@ -284,7 +280,8 @@ function loadGrpcClient(protoDef: ProtoPackageDefinition): AsyncCmdExecutor { // The cast thru `unkown` lets us convince the type system of anything // See https://basarat.gitbook.io/typescript/type-system/type-assertion#double-assertion const pkg = protoDescriptor.shai as unknown as ShaiPkg - const stub = new pkg.cmdExecutor.CmdExecutor(APALACHE_SERVER_URI, grpc.credentials.createInsecure()) + const stub: any = new pkg.cmdExecutor.CmdExecutor(APALACHE_SERVER_URI, grpc.credentials.createInsecure()) + console.log(`Connectivity state: ${stub.getChannel().getConnectivityState(true)}`) const impl: AsyncCmdExecutor = { run: promisify((data: RunRequest, cb: AsyncCallBack) => stub.run(data, cb)), ping: promisify((cb: AsyncCallBack) => stub.ping({}, cb)),