informalsystems / quint

An executable specification language with delightful tooling based on the temporal logic of actions (TLA)
Apache License 2.0
782 stars 31 forks source link

deno binary builds in releases #1461

Open rnbguy opened 2 months ago

rnbguy commented 2 months ago

I have been using Quint with Deno for a while.

$ deno install -A -n quint npm:@informalsystems/quint
✅ Successfully installed quint
/home/user/.deno/bin/quint
$ quint --version
0.21.0
$ # or just
$ deno run -A npm:@informalsystems/quint --version
0.21.0

But I wished if Quint releases could include binaries directly via deno compile.

But I couldn't suggest as quint verify was breaking because of a http2 bug. Today, I resolved it on denoland/deno#24576 which makes Quint Deno-compatible. You can now try it on quint examples.

$ cd quint/examples/cosmos/ics20
$ deno run -A npm:@informalsystems/quint verify --max-steps=1 --main=bankTests --invariant=BalanceNonNegative,NonExistantAccountsOrCoinsAreZero bank.qnt

With this, would you consider including Deno compiled Quint binaries in future releases?

$ deno compile -A -o quint npm:@informalsystems/quint
$ ./quint --version
0.21.0

Pros:

Cons:

Refs:

bugarela commented 1 month ago

Thank you for fixing that issue! I agree, we should do it: Pros > Cons :smile: