[Why3-club] Why3 IDE

Per Lindgren Per.Lindgren at ltu.se
Sun Oct 16 17:47:40 CEST 2016

Hi folks.

I have a few usability questions.

Regarding transformations:
1. There seems to be a shortcut associated to the Strategies (Compute (c), Inline (i), Split (s)). I can’t figure out how to access those, (Ctrl-c, collapses, Ctrl-r reloads, those shortcuts works, but for the Strategies, I haven’t figured out. (I tried both under OS X and Linux)

2. Is there a simple way to add Strategies, without altering the source code. (Well they can be found under the Tools drop down, but its inconvenient)

3. Alternatively, can one associate shortcuts also to those Transformations under Tools, (maybe there is already shortcuts, but the key bindings are now shown)

And perhaps most importantly:
4. Is there a simple way to undo a transformation. Sometimes, it could be useful, when trying out a proof, to quickly be able to reverse to prior proof state(s). Especially if you are applying a transformation on a set of “split” goals, then you have to go through each goal and remove the applied transformations, or alternatively go up to the point of the split, and remove that (all subsequent transformations will then be removed, but its quite inconvenient).

Regarding why3 source code editing:
Both under OS X and linux, it seems that the source view is just a view, and does not allow for editing (I assume its the expected behaviour). Is there ongoing work towards a coq-ide like built in editor? (Seems to be the same GTK based windows, so perhaps code could be borrowed, but I’m not familiar with GTK programming.) I’ve seen you can associate external editors, and I use Emacs for coq integration that works well. Currently I use Emacs for the why3 source editing, and then reload (but errors have to be located manually, since there is no integration).

Any input welcome. (I’ve starting to look into the why3 source code, but its quite a big project, and I’m new to GTK so its challenging…)


More information about the Why3-club mailing list