search

informalsystems / quint

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

incorrect argument order in getting started example #1544

Open mikekidner opened 3 weeks ago

mikekidner commented 3 weeks ago

In the Getting Started section of the docs, the bank example is run like: quint run bank.qnt --invariant=no_negatives This yields this error:

[DEBUG] generating undefined expr to fill hole in: valq::inv={=no_negatives
/Users/mikekidner/Downloads/bank.qnt:3:17 - error: [QNT000] no viable alternative at input '{='
3:   var balances: str -> int
                   ^^^

/Users/mikekidner/Downloads/bank.qnt:3:24 - error: [QNT000] extraneous input 'val' expecting {<EOF>, 'module', DOCCOMMENT}
3:   var balances: str -> int
                          ^^^

error: Runtime error

It should be called like: quint run --invariant=no_negatives bank.qnt

bugarela commented 2 weeks ago

Hi! It should definitely also work with quint run bank.qnt --invariant=no_negatives. This might be something specific to your setup (for example, I remember https://github.com/informalsystems/quint/issues/1473 where there is a problem specifically with local installations). Can you provide some more info about your setup? Did you install Quint via npm? Which version do you have? And what OS are you using?

From the error message, seems like somehow a {= character was inserted on the argument somehow. I don't have any ideas on how that might have happened :disappointed:

mikekidner commented 2 weeks ago

Hi, Mac OS X 12.6.3 I installed npm using brew and then quint-0.18.3 from npm.

bugarela commented 2 weeks ago

Hi, thanks! I'm a bit clueless here, most of Quint users are on MacOS and I never heard of this before. Also, although the latest version is 0.22.3 (and somehow npm from brew is not installing the latest version, this is something I noticed from several people), the issue you reported has never been a problem in no versions of Quint, so I don't think updating will help.

Can it be that your shell is doing something weird, or that copy-pasting introduced the a hidden char sequence like {=? If possible, could you try a different shell/terminal and typing the command by hand?