Add compile subcommand

[shonfeder]

We currently offer the following subcommands in the CLI:

  quint parse <input>      parse a Quint specification
  quint typecheck <input>  check types and effects of a Quint specification
  quint repl               run an interactive Read-Evaluate-Print-Loop [default]
  quint run <input>        Simulate a Quint specification and check invariants
  quint test <input>       Run tests against a Quint specification
  quint verify <input>     Verify a Quint specification via Apalache
  quint docs <input>       produces documentation from docstrings in a Quint
                           specification

parse and typecheck can be used to check an input's validity for syntax and typechecking, respectively, and to produce the intermediate stage of IR resulting from those processes. However, run, test, verify do not operate on the result of typechecking: instead they all require post-processing that includes forms of flattening and inlining.

This stage of the process is not exposed through the CLI currently, even tho it would be helpful for debugging and is probably what other tooling would want to consume.

I propose exposing this stage of the process through a compile subcommand, which will also become the recommended way for users to perform all static analysis and processing to a spec before passing it off to other tools.

[konnov]

I am so happy that we both came up with the same idea independently! #359

[shonfeder]

Ah yeah, I remember that issue now! I was probably channeling subconscious recollection of it :)

I think I agree with the functionality I'm not sure if I agree on the preferred interface.

We can probably merge these issues. The main thing I need is output of the stage that includes flattening, and a compile sub command seems like the right place to put that.

As to whether we should merge the parse and typecheck commands into compile, I'm not so sure. I'm not opposed, I just don't see a problem with having distinct subcommands here or what the benefit is of moving it into flags under a single subcommand. I guess our current interface seems a bit more like cargo than go, in that cargo has both build and check?

[shonfeder]

Closing as duplicate of #359

[konnov]

If you would like to introduce a third command along with parse and typecheck, I am afraid it would get just too complicated from the user perspective. Who would know all these nuances? I think people can still get the difference between parse and typecheck, but what would compile do in their understanding?

[bugarela]

I Believe @shonfeder meant to close this, so closing (GitHub UI is terrible for this IMO)