Clean up example runner script

[thpani]

The example runner script current uses a lot of hard-coded comparisons to set the proper flags for running examples:

https://github.com/informalsystems/quint/blob/4afc1c2351b5c941f21836cce522e5b799b80b24/examples/.scripts/run-example.sh#L24-L29

Once all (or a majority) of examples go through Apalache, we should find a way to do this more systematically.

Options discussed so far:

1. use an external config file (csv or sim)
2. put the commands into the actual modules, using some special (comment?) syntax

Follow-up to https://github.com/informalsystems/quint/pull/1070#discussion_r1272397600

[shonfeder]

My suggestion on this is that we extend quint with an ability to read default configuration values out of some annotation in a spec. E.g., using some randomly made up syntax for illustration:

#[verify:main(init=Start, step=Next, length=3)]
module Foo { ... }

#[test:main(...)]
module FooTests { ... }

which would then be used as the fallback config if values were not found via the CLI. I think this would be useful for testing and CI?

iirc, @konnov had a related thought and we discussed briefly in slack. I guess this would call for its own issue if we thought it worth while.

[shonfeder]

I don't think this issue is part of the transpliation milestone, as it's more about quint CLI utilities or our CI config (depending on how we approach it).

[konnov]

Nice idea. To achieve that, we don't even have to extend the syntax. We could simply add these annotations in comments, e.g.:

// #[verify:main(init=Start, step=Next, length=3)]
module Foo { ... }

[thpani]

I don't think this issue is part of the transpliation milestone

IMO it's tech debt that resulted from the transpilation milestone, and should be cleaned up as part of it?

[bugarela]

One note on the annotation syntax: The REPL already adds a // @mainModule foo annotation to files, that is written in .save and loaded in .load or via the REPL CLI.

I'm not attached to this syntax, but we should either make something consistent with this or deprecate it in favor of the new syntax (as oppose to forgetting about it and having 2 mismatching types of annotations).