Improving the Why3 CLI for proving
In the last GT we saw the new changes to why3 session-create
and the improved why3 bench
, during that session I proposed that it would be helpful for Why3 to provide a CLI interface of 'equal' power to the IDE, for the users of Why3 that for various reasons cannot or chose not to use the IDE.
In particular, I'm refering to the ability to run strategies on targetted files, potentially creating the session if necessary.
If such a command were added it could be done as a replacement for the current why3 prove
which is sort of misleadingly named as it does not use the sessions, even if they are available.
I think the requirements for this new / upgraded command would be:
- Load or create a session for the targeted files
- Ability to apply transformations, provers and strategies to goals in the file
- Should run all chosen provers and output a clear ok / reject message.
What does everyone think?