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 

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 

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…)


Why3-club mailing list

Reply via email to