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

grammar: consider adding support for hashbang scripting #1500

Closed
lucab opened this issue Sep 6, 2024 · 1 comment · Fixed by #1522
Closed

grammar: consider adding support for hashbang scripting #1500

lucab opened this issue Sep 6, 2024 · 1 comment · Fixed by #1522
Labels
good first issue A simple issue to start with

Comments

@lucab
Copy link
Contributor

lucab commented Sep 6, 2024

This is a new-feature request for Quint grammar.

I recently added an example which contains this human-readable comment:

* Run in verifier with:
* quint verify --temporal correct teachingConcurrency.qnt

However, on Unix systems I'd like to be able to directly run this model as ./teachingConcurrency.qnt, by adding a starting hashbang line like the following:

#!/usr/bin/env -S quint verify --temporal correct

This is not currently possible because the starting # is not a valid token:

./teachingConcurrency.qnt:1:1 - error: [QNT000] token recognition error at: '#'
1: #!/usr/bin/env -S quint verify --temporal correct
   ^

./teachingConcurrency.qnt:1:2 - error: [QNT000] token recognition error at: '!/'
1: #!/usr/bin/env -S quint verify --temporal correct
    ^

./teachingConcurrency.qnt:1:4 - error: [QNT000] mismatched input 'usr' expecting {'module', DOCCOMMENT}
1: #!/usr/bin/env -S quint verify --temporal correct
      ^^^

error: parsing failed

For reference, Javascript was in a similar situation and recently added hashbang support in ES14 (in 2023):
https://www.w3schools.io/javascript/shebang-examples/

I think there are two alternative ways to implement this:

  1. Adding a new token rule for # as another starting marker for single-line comments (similar to // and ///), anywhere in a file.
  2. Adding a custom token rule for #! as a new starting marker for an hashbang line, only valid at the beginning of a file.
@bugarela
Copy link
Collaborator

bugarela commented Sep 9, 2024

Oh, I didn't know we could use commands like this in the hasbang! This is awesome. Thanks for reporting, this should be easy to implement as you suggest :)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
good first issue A simple issue to start with
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants