Skip to content

Commit

Permalink
Move connection attempt into connect()
Browse files Browse the repository at this point in the history
  • Loading branch information
thpani committed Aug 23, 2023
1 parent dd22552 commit 265d606
Showing 1 changed file with 17 additions and 11 deletions.
28 changes: 17 additions & 11 deletions quint/src/quintVerifier.ts
Original file line number Diff line number Diff line change
Expand Up @@ -275,7 +275,7 @@ async function loadProtoDefViaReflection(): Promise<VerifyResult<ProtoPackageDef
)
}

function loadGrpcClient(protoDef: ProtoPackageDefinition): VerifyResult<AsyncCmdExecutor> {
function loadGrpcClient(protoDef: ProtoPackageDefinition): AsyncCmdExecutor {
const protoDescriptor = grpc.loadPackageDefinition(protoDef)
// The cast thru `unkown` lets us convince the type system of anything
// See https://basarat.gitbook.io/typescript/type-system/type-assertion#double-assertion
Expand All @@ -285,7 +285,7 @@ function loadGrpcClient(protoDef: ProtoPackageDefinition): VerifyResult<AsyncCmd
run: promisify((data: RunRequest, cb: AsyncCallBack<any>) => stub.run(data, cb)),
ping: promisify((cb: AsyncCallBack<void>) => stub.ping({}, cb)),
}
return right(impl)
return impl
}

// Retry a function repeatedly, in .5 second intervals, until it does not throw.
Expand Down Expand Up @@ -314,8 +314,20 @@ async function retryWithTimeout<T>(f: () => Promise<T>): Promise<VerifyResult<T>
// Try to establish a connection to the Apalache server
//
// A successful connection procudes an `Apalache` object.
async function connect(cmdExecutor: AsyncCmdExecutor): Promise<VerifyResult<Apalache>> {
return retryWithTimeout(() => cmdExecutor.ping()).then(response => response.map(_ => apalache(cmdExecutor)))
async function connect(): Promise<VerifyResult<Apalache>> {
// Attempt to load proto definition:
// - if APALACHE_DIST is set, from the Apalache distribution
// - otherwise, via gRPC reflection
const protoDefResult: VerifyResult<proto.PackageDefinition> = process.env.APALACHE_DIST
? findApalacheDistribution().chain(loadProtoDefViaDistribution)
: await loadProtoDefViaReflection()
// Load gRPC client
let maybeCmdExecutor = protoDefResult.map(loadGrpcClient)
await maybeCmdExecutor.asyncChain(cmdExecutor =>
// Try to ping the server, with a timeout
retryWithTimeout(() => cmdExecutor.ping())
)
return maybeCmdExecutor.map(apalache)
}

/**
Expand All @@ -327,12 +339,6 @@ async function connect(cmdExecutor: AsyncCmdExecutor): Promise<VerifyResult<Apal
* @returns right(void) if verification succeeds, or left(err) explaining the failure
*/
export async function verify(config: any): Promise<VerifyResult<void>> {
// Attempt to load proto definition:
// - if APALACHE_DIST is set, from the Apalache distribution
// - otherwise, via gRPC reflection
const protoDefResult = process.env.APALACHE_DIST
? findApalacheDistribution().chain(dist => loadProtoDefViaDistribution(dist))
: await loadProtoDefViaReflection()
const connectionResult = await protoDefResult.chain(loadGrpcClient).asyncChain(connect)
const connectionResult = await connect()
return connectionResult.asyncChain(conn => conn.check(config))
}

0 comments on commit 265d606

Please sign in to comment.