[Why3-club] Why3 IDE

Per Lindgren Per.Lindgren at ltu.se
Wed Oct 19 19:37:05 CEST 2016


Dear Claude

Thanks for your prompt answer. I will look into this. 

The version I’ve been working with is the one checked out through opam (0.87.2). Is this the same version as the master branch, or?

Indeed, simply c/i/s works (I believe I tried all key combinations, just not the plain keystrokes ;)

> I'm not sure about what you ask exactly. Strategies are not "officially"
> supported in the release 0.87.2, but they are if you follow the git
> master branch. In that case you will find information in the
> documentation, section 10.6.

I mean the list of buttons (Compute, Inline, Split). These occur also in the drop down under Tools/Strategies (0.87.2). Maybe you mean some other type of strategies (referring to the git master branch).

>> And perhaps most importantly: 4. Is there a simple way to undo a
>> ...
> 
> Unfortunately it is not possible. If you are lucky and just loaded the
> session, or just saved the session into disk, then you have the
> possibility to exit without saving and reload.
Would it be possible to implement this as a stack (or possibly two stacks, for redo), storing the  “session” information, and then on e.g. Cmd-Z/Cmd-Shift-Z (undo/redo) push current session to the redo stack, and pop the undo, and on the result call the function that processes the “session” information. Perhaps that would essentially amount to restarting the whole Why3 on undo/redo, but at least it would be more convenient than the suggested exit/restart.

I will look into the GTK and editing to see if I can make any sense out of it...

Best,
  Per

> On 19 Oct 2016, at 17:12, Claude Marché <Claude.Marche at inria.fr> wrote:
> 
> 
> Hello,
> 
> Le 16/10/2016 à 17:47, Per Lindgren a écrit :
>> 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)
> 
> Simply type the character, without the Ctrl key nor the Shift key or
> whatever.
> 
>> 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)
> 
> I'm not sure about what you ask exactly. Strategies are not "officially"
> supported in the release 0.87.2, but they are if you follow the git
> master branch. In that case you will find information in the
> documentation, section 10.6.
> 
> Roughly speaking, your own strategies can be coded using a very basic
> programming language. Codes of strategies can be given textually in why3
> config files, you don't need to modify the Why3 source code.
> 
>> 3. Alternatively, can one associate shortcuts also to those
>> Transformations under Tools, (maybe there is already shortcuts, but
>> the key bindings are now shown)
> 
> Adding shortcuts is part of the mechanism for defining strategies in
> Why3 config files.
> 
>> 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).
> 
> Unfortunately it is not possible. If you are lucky and just loaded the
> session, or just saved the session into disk, then you have the
> possibility to exit without saving and reload.
> 
>> 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).
> 
> Indeed the ability the edit the source directly was experimented. If you
> want to give a try, modify the source file src/ide/gmain.ml, in the line
> 
> let allow_editing = false (* not reliable enough yet *)
> 
> replace the false by true, and recompile. In order to re-interpret the
> edited file, I'm afraid you will have to type both Ctrl-S (to save on
> disk) and then Ctrl-R (to update the session view)
> 
> I'm not sure I remember why we did not want to make it possible by
> default. It may be because we found no way to check whether the file
> needs saving before exiting, so that we can ensure the user would not
> lose her/his modifications without notice.
> 
>> 
>> 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…)
> 
> The code for the GTK interface is indeed ugly. Anyway, if you succeed to
> modify the code in a satisfactory way, we would be happy to accept a patch !
> 
> - Claude
> 
> -- 
> Claude Marché                          | tel: +33 1 69 15 66 08
> INRIA Saclay - Île-de-France           |
> Université Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
> F-91405 ORSAY Cedex                    |
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/why3-club



More information about the Why3-club mailing list