[Why3-club] Questions about the why3 ide

Delphine Demange delphine.demange at irisa.fr
Fri Mar 29 10:16:26 CET 2019

Dear Claude,

>> - close a file from the IDE directly
> What do you mean by "closing"? removing the tab?
Yes, removing the tab.
I'm not sure of what it would mean in terms of the session.
Perhaps saving the current state of the theories/goals of the file, before the tab disappears from the IDE.

>> - reset the session from the IDE
> What do you mean by "reset"? abandon all changes? That is what you can achieve by exiting without saving and reloading?
Sometimes I like to 1) exit without saving the session 2) remove manually the session dir 3) relaunch the IDE.
It's to either make sure the changes in my settings (provers/timers/memory) are taken into account, or to replay manually all the "proof scenario" from scratch. So, by "reset", I probably meant "remove all proof nodes (proven or not), and hard-refresh the session".

>> Perhaps these features were already introduced in a version more recent than mine.
> No they aren't, but we are willing to add them if you think it is useful.
Those three items are the one that miss the most. That would be great indeed.
I should perhaps emphasize that my use-cases are mostly in a teaching context.
Hence, usually, modules are standalone (they just import theories from the stdlib), theories are short, and proofs are discharged automatically or with simple strategies (repeated splits, and 0 / 1 / 2 auto levels).


More information about the Why3-club mailing list