Change placeholders to `{test}` and `{seq}`, stop enforcing `.itf.json` extension, rename `test --output` to `test --out-itf` #1485

romac · 2024-08-21T06:40:55Z

Closes: #1484
Closes: #1137

`run`, `test`

Change placeholders from {} to {test} and from {#} to {seq}

`run`

Auto-append trace sequence number to filename if more than one trace is present and {seq} is not specified

`test`

Stop enforcing .itf.json extension
Rename --output to --out-itf, add hidden alias for the former
Show output (ie. test results) even if --out-itf is set

`verify`

Add warning if --out-itf option contains {test} or {seq} as those have no effect since Apalache only produces a single trace

bugarela

Hi, thanks for taking care of this! I see that a couple of integration tests are breaking because the expected files were not created on quint run with --n-traces. Just flagging this if you want to take a look - otherwise I'll debug this later in the week

romac · 2024-08-21T11:18:54Z

Sure, I'll take a look :)

konnov · 2024-08-22T09:54:59Z

Just a note on {#}. I guess, it is my fault introducing it. The issue is that GNU parallel is using the same substitution syntax for the job number. If you plan to use Quint with parallel, this is going to be a problem.

bugarela · 2024-08-22T12:07:55Z

Just a note on {#}. I guess, it is my fault introducing it. The issue is that GNU parallel is using the same substitution syntax for the job number. If you plan to use Quint with parallel, this is going to be a problem.

Hmm interesting. I think it's a good idea to use the same standard as other program. I guess you can always wrap your quint command in a shell script or something and then call parallel on that to avoid the issue?

bugarela

LGTM ✨

romac · 2024-08-22T12:28:03Z

Ah good point @konnov, I did not think of that.

I guess the solution @bugarela works, but it's also possible to change the parallel replacement string to something else using its --seqreplace option: https://www.gnu.org/software/parallel/parallel_tutorial.html

@konnov What do you think, are those workarounds good enough for you?

konnov · 2024-08-22T14:31:57Z

Ah good point @konnov, I did not think of that.

I guess the solution @bugarela works, but it's also possible to change the parallel replacement string to something else using its --seqreplace option: https://www.gnu.org/software/parallel/parallel_tutorial.html

@konnov What do you think, are those workarounds good enough for you?

Well, it would kind of work, but parallel is tough enough alone, so adding complexity on top of it would make things even harder :)

romac · 2024-08-22T15:12:22Z

I agree it's a bit more complex, but you only have to figure out the right invocation of parallel once, then you can re-use it everywhere. On the other hand, changing the variable would involve making a breaking change in the Quint CLI, since we also use {#} and {} in other commands as well (i.e. quint test --output).

That said, I empathize with the goal of building tools (Quint in this case) which work well with other pre-existing tools, as per the UNIX philosophy, so I am not sure how to weigh one against the other.

What do you think, @bugarela?

bugarela · 2024-08-22T15:53:53Z

What about doing something more like what TLC does and just produce a pattern without requiring the user to specify it? It takes away the ability of the user to customize the filenames to their liking, but it makes it easier for new users, which won't have to learn how to write this parameter.

So if I run

quint run --out-itf=foo.json --n-traces=2

it will produce foo1.json and foo2.json (or something like that)

konnov · 2024-08-22T16:20:34Z

What about doing something more like what TLC does and just produce a pattern without requiring the user to specify it? It takes away the ability of the user to customize the filenames to their liking, but it makes it easier for new users, which won't have to learn how to write this parameter.

So if I run
quint run --out-itf=foo.json --n-traces=2
it will produce foo1.json and foo2.json (or something like that)

This actually looks nice to me.

romac · 2024-08-22T20:53:12Z

Agreed, that's perhaps the most user-friendly and pragmatic option 👍

romac · 2024-08-23T07:34:14Z

What shall we do about quint test --output?

  --output       write a trace for every test, e.g., out{#}{}.itf.json where {}
                 is the name of a test, {#} is the test sequence number [string]

Shall we keep the {} placeholder, remove {#} and automatically append the sequence number like for run/verify --out-itf?

romac · 2024-08-23T07:39:56Z

An alternative is to change the placeholders to from {} to {test} and {#} to {seq} or something like that for test, and from {#} to {seq} for run and verify, and automatically append the seq number if the {seq} parameter is not present.

quint run/verify --n-traces 3 --out-itf trace_{seq}.itf.json
- => trace_0.itf.json, trace_1.itf.json, trace_2.itf.json
quint run/verify --n-traces 3 --out-itf trace.itf.json
- => trace0.itf.json, trace1.itf.json, trace2.itf.json
quint test --n-traces 3 --output {test}_{seq}.itf.json
- => someTest_0.itf.json, someTest_1.itf.json, someTest_2.itf.json
quint test --n-traces 3 --output {test}.itf.json
- => someTest0.itf.json, someTest1.itf.json, someTest2.itf.json

This way we get the best of both worlds, being both user-friendly and configurable.

Also, how about we also change test --output to test --out-itf for consistency with run and verify, but keep --output as an alias for --out-itf?

bugarela · 2024-08-26T12:57:09Z

I think that would be absolutely amazing! It's a good thing to have the templates optionally, and using seq and test solves the problem of conflict with parallel while also being much clearer. Thanks for thinking this through!

…ess of whether it ends with `.itf.json`

…ut` argument

… the former

…ded, even when not needed

bugarela · 2024-08-28T15:37:43Z

check.sh

+# Loop through each .qnt file and check its header
+for file in $qnt_files; do
+  if [[ "$(head -n 1 "$file")" != "// -*- mode: Bluespec; -*-" ]]; then
+    echo "File $file does not start with // -*- mode: Bluespec; -*-"


Great idea! This will be useful 😄

Woops forgot to remove this, wanted to do this in a GitHub Actions workflow. Will open a separate PR for it.

bugarela · 2024-08-28T15:43:40Z

quint/io-cli-tests.md

@@ -864,7 +864,7 @@ rm out-itf-example.itf.json

 <!-- !test in run with n-traces itf -->
 ```
-quint run --out-itf=out-itf-example.itf.json --n-traces=3 --max-steps=5 --seed=123  ../examples/tutorials/coin.qnt
+quint run --out-itf='out-itf-example{seq}.itf.json' --n-traces=3 --max-steps=5 --seed=123  ../examples/tutorials/coin.qnt


Do we actually need to update this? Isn't the behavior on the old version of the test still the default?

My bad, forgot to revert this!

bugarela · 2024-08-28T15:51:27Z

quint/src/cliCommands.ts

+  return args.out ? 0 : args.verbosity
+}
+
+const Placeholders = {


Can we make it fully capitalized? I don't think we have this patter of capitalization for any values in the code (only classes and types), so it's a bit odd.

Suggested change

const Placeholders = {

const PLACEHOLDERS = {

bugarela · 2024-08-28T15:58:30Z

quint/src/cliCommands.ts

+  if (template.includes(Placeholders.seq)) {
+    return template.replaceAll(Placeholders.seq, index.toString())
+  } else if (options.autoAppend && template.endsWith('.itf.json')) {
+    // Special case for the recommended extension, to avoid adding the index in between `itf` and `json`


I think this is ok, but I guess one alternative would be to add the index right before the first . in the file name, so it would work fine with .itf.json without having to treat it separately, and, although it doesn't matter a lot, it would work better with arbitrary file names (foo1.bla.json is better than foo.bla1.json I guess).

Agreed, that's a better solution!

…to filename, before any extension

bugarela

🚀

romac requested a review from bugarela August 21, 2024 06:40

bugarela reviewed Aug 21, 2024

View reviewed changes

romac requested a review from bugarela August 21, 2024 12:07

bugarela approved these changes Aug 22, 2024

View reviewed changes

romac added 7 commits August 27, 2024 10:22

Allow {#} placeholder in run commands --out-itf option, regardl…

afb4d9f

…ess of whether it ends with `.itf.json`

Remove restriction on itf.json extension in test commands `--outp…

6091d81

…ut` argument

Fix --invariant help message

766a249

Fix tests

6434789

Fix typos

09c44e1

Rename test --output to test --out-itf and add a hidden alias for…

6bc8e0c

… the former

Change placeholders from {} to {test} and from {#} to {seq}

9a5971f

romac changed the title ~~Allow {#} placeholder in run commands --out-itf option, regardless of whether it ends with .itf.json~~ Change placeholders to {test} and {seq}, stop enforcing .itf.json extension, rename test --output to test --out-itf Aug 27, 2024

romac force-pushed the romac/out-itf-option branch from c364762 to 9a5971f Compare August 27, 2024 09:10

romac requested a review from bugarela August 27, 2024 09:10

romac added 2 commits August 27, 2024 11:14

Update changelog

1305034

Fix bug in test command where sequence number would always be appen…

6f28477

…ded, even when not needed

romac force-pushed the romac/out-itf-option branch from 5963227 to 6f28477 Compare August 27, 2024 11:31

Show output of test command, even when --out-itf is specified

6e0c304

Disable output of verify command if --out-itf is set

cf3df7c

bugarela reviewed Aug 28, 2024

View reviewed changes

romac added 4 commits August 29, 2024 10:37

Remove unrelated file

25de498

Revert unnecessary changes in CLI tests

6988f0e

Change constant to uppercase

463d19f

Remove special case for .itf.json trace files, always append index …

ce713fe

…to filename, before any extension

bugarela approved these changes Aug 29, 2024

View reviewed changes

Merge branch 'main' into romac/out-itf-option

21c07da

romac enabled auto-merge August 29, 2024 12:17

romac disabled auto-merge August 29, 2024 12:17

romac enabled auto-merge August 29, 2024 12:18

romac merged commit b9f3e4d into main Aug 29, 2024
14 checks passed

romac deleted the romac/out-itf-option branch August 29, 2024 12:22

bugarela mentioned this pull request Sep 9, 2024

Release v0.21.2 #1503

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Change placeholders to `{test}` and `{seq}`, stop enforcing `.itf.json` extension, rename `test --output` to `test --out-itf` #1485

Change placeholders to `{test}` and `{seq}`, stop enforcing `.itf.json` extension, rename `test --output` to `test --out-itf` #1485

romac commented Aug 21, 2024 •

edited

Loading

bugarela left a comment

romac commented Aug 21, 2024

konnov commented Aug 22, 2024

bugarela commented Aug 22, 2024

bugarela left a comment

romac commented Aug 22, 2024

konnov commented Aug 22, 2024

romac commented Aug 22, 2024

bugarela commented Aug 22, 2024

konnov commented Aug 22, 2024

romac commented Aug 22, 2024

romac commented Aug 23, 2024

romac commented Aug 23, 2024 •

edited

Loading

bugarela commented Aug 26, 2024

bugarela Aug 28, 2024

romac Aug 28, 2024

romac Aug 29, 2024

bugarela Aug 28, 2024

romac Aug 28, 2024

romac Aug 29, 2024

bugarela Aug 28, 2024

romac Aug 28, 2024

romac Aug 29, 2024

bugarela Aug 28, 2024

romac Aug 28, 2024

romac Aug 29, 2024

bugarela left a comment

Change placeholders to {test} and {seq}, stop enforcing .itf.json extension, rename test --output to test --out-itf #1485

Change placeholders to {test} and {seq}, stop enforcing .itf.json extension, rename test --output to test --out-itf #1485

Conversation

romac commented Aug 21, 2024 • edited Loading

run, test

run

test

verify

bugarela left a comment

Choose a reason for hiding this comment

romac commented Aug 21, 2024

konnov commented Aug 22, 2024

bugarela commented Aug 22, 2024

bugarela left a comment

Choose a reason for hiding this comment

romac commented Aug 22, 2024

konnov commented Aug 22, 2024

romac commented Aug 22, 2024

bugarela commented Aug 22, 2024

konnov commented Aug 22, 2024

romac commented Aug 22, 2024

romac commented Aug 23, 2024

romac commented Aug 23, 2024 • edited Loading

bugarela commented Aug 26, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bugarela left a comment

Choose a reason for hiding this comment

Change placeholders to `{test}` and `{seq}`, stop enforcing `.itf.json` extension, rename `test --output` to `test --out-itf` #1485

Change placeholders to `{test}` and `{seq}`, stop enforcing `.itf.json` extension, rename `test --output` to `test --out-itf` #1485

romac commented Aug 21, 2024 •

edited

Loading

`run`, `test`

`run`

`test`

`verify`

romac commented Aug 23, 2024 •

edited

Loading