You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I opened this issue because of this comment: #3326 (comment)
We have a NPM executable that connects to a gRPC server. The current gRPC support doesn't work with it.
You can reproduce this by doing the following:
git clone https://github.com/informalsystems/quint
cd quint/examples/cosmos/ics20
deno run -A npm:@informalsystems/quint verify --max-steps=3 --main=bankTests --invariant=BalanceNonNegative,NonExistantAccountsOrCoinsAreZero bank.qnt
I get the following error:
Warning: Not implemented: Http2Session.socket
Warning: Not implemented: Http2Session.socket
Internally, @informalsystems/quint downloads apalache and executes apalache server that launchs the gRPC server and then quint tries to connect to it via @grpc/grpc-js.
Version: Deno v1.44.0
I opened this issue because of this comment: #3326 (comment)
We have a NPM executable that connects to a gRPC server. The current gRPC support doesn't work with it.
You can reproduce this by doing the following:
git clone https://github.com/informalsystems/quint cd quint/examples/cosmos/ics20 deno run -A npm:@informalsystems/quint verify --max-steps=3 --main=bankTests --invariant=BalanceNonNegative,NonExistantAccountsOrCoinsAreZero bank.qnt
I get the following error:
Internally,
@informalsystems/quint
downloadsapalache
and executesapalache server
that launchs the gRPC server and thenquint
tries to connect to it via@grpc/grpc-js
.The source code for the gRPC client lives at https://github.com/informalsystems/quint/blob/main/quint/src/apalache.ts.
Am I doing anything wrong?
PS. to minimize the debugging overhead, you can just use
apalache
and this Deno script: https://gist.github.com/rnbguy/77e73b3ea9515f8013a66060acb9796f.In two different terminals:
The text was updated successfully, but these errors were encountered: