diff --git a/quint/apalache-dist-tests.md b/quint/apalache-dist-tests.md index cc8438821..180692ca7 100644 --- a/quint/apalache-dist-tests.md +++ b/quint/apalache-dist-tests.md @@ -72,7 +72,7 @@ quint verify ../examples/language-features/booleans.qnt ``` -error: Apalache gRPC endpoint is corrupted. Error reading from streaming API: No connection established +error: Failed to obtain a connection to Apalache after 5 seconds. ``` ### Inability to connect to the server produces an errer (`APALACHE_DIST` set) diff --git a/quint/src/quintVerifier.ts b/quint/src/quintVerifier.ts index b927f4e6c..6aa0c9cfd 100644 --- a/quint/src/quintVerifier.ts +++ b/quint/src/quintVerifier.ts @@ -213,6 +213,7 @@ function loadProtoDefViaDistribution(dist: ApalacheDist): VerifyResult> { + // Types of the gRPC interface. type ServerReflectionRequest = { file_containing_symbol: string } type ServerReflectionResponseSuccess = { file_descriptor_response: { @@ -235,46 +236,43 @@ async function loadProtoDefViaReflection(): Promise = await new Promise( - (resolve, reject) => { - const call = reflectionClient.ServerReflectionInfo() - call.on('data', (r: ServerReflectionResponse) => { - call.end() - resolve(r) + // Query reflection endpoint (retry if server is unreachable) + return retryWithTimeout( + () => + 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' }) }) - call.on('error', (e: grpc.StatusObject) => reject(e)) - - call.write({ file_containing_symbol: 'shai.cmdExecutor.CmdExecutor' }) - } - ) - .then(right) - .catch(e => err(`Apalache gRPC endpoint is corrupted. Error reading from streaming API: ${e.details}`)) + ).then(response => + // 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}` + ) + } - return 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}` + // Decode reflection response to FileDescriptorProto + let fileDescriptorProtos = protoDefResponse.file_descriptor_response.file_descriptor_proto.map( + bytes => protobufDescriptor.FileDescriptorProto.decode(bytes) as protobufDescriptor.IFileDescriptorProto ) - } - - // Decode reflection response to FileDescriptorProto - let fileDescriptorProtos = protoDefResponse.file_descriptor_response.file_descriptor_proto.map( - bytes => protobufDescriptor.FileDescriptorProto.decode(bytes) as protobufDescriptor.IFileDescriptorProto - ) - // Use proto-loader to load the FileDescriptorProto wrapped in a FileDescriptorSet - return right(proto.loadFileDescriptorSetFromObject({ file: fileDescriptorProtos }, grpcStubOptions)) - }) + // Use proto-loader to load the FileDescriptorProto wrapped in a FileDescriptorSet + return right(proto.loadFileDescriptorSetFromObject({ file: fileDescriptorProtos }, grpcStubOptions)) + }) + ) } function loadGrpcClient(protoDef: ProtoPackageDefinition): VerifyResult {