Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

incorrect argument order in getting started example #1544

Open
mikekidner opened this issue Nov 6, 2024 · 3 comments
Open

incorrect argument order in getting started example #1544

mikekidner opened this issue Nov 6, 2024 · 3 comments

Comments

@mikekidner
Copy link

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
Copy link
Collaborator

bugarela commented Nov 7, 2024

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 #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 😞

@mikekidner
Copy link
Author

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

@bugarela
Copy link
Collaborator

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?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants