[Why3-club] lemma visibility
julia.lawall at lip6.fr
Thu Jan 24 14:09:35 CET 2019
On Thu, 24 Jan 2019, Mohamed Iguernlala wrote:
> On 24/01/2019 13:50, Julia Lawall wrote:
> > On Thu, 24 Jan 2019, Mohamed Iguernlala wrote:
> > > Hello,
> > >
> > > You can use "alt-ergo -profiling N <file>" to display some
> > > profiling information on standard output every "N"
> > > seconds (you'll probably need a big screen or to put a smaller
> > > font size for the terminal's text). There are 5 different views,
> > > and you are probably interested in the last one. To cycle through
> > > different views, use "Ctrl+C" (and "Ctrl+AltGr+\" to kill Alt-Ergo).
> > >
> > > Alternatively, you can activate debug option "-dmatching 1" to
> > > display some information about axioms instantiation activity.
> > >
> > > To finish, you can use "-save-used-context" to save the names of
> > > axioms used by Alt-Ergo during a proof (this will generate a
> > > .used file), and "-replay-used-context" to filter out the axioms
> > > that do not appear in the .used file corresponding to the input
> > > file.
> > Does this work from why3? I tried adding the -verbose option in the why3
> > configuration file, and I have the impression that why3 wrote over it. I
> > don't know whay information why3 feeds to alt-ergo, so I don't know how to
> > run alt-ergo directly.
> I don't know if one could pass options to Alt-Ergo via
> Why3 (without edition the why3.conf file). This is a question for
> Why3 team.
> What I usually do is the following:
> - From Why3 IDE, you should be able to go to "Setting" and change
> them to edit files that are not proved by Alt-Ergo with, for
> instance, Emacs editor.
> - Then, If a VC is not proved by Alt-Ergo, you should be able
> to "edit" the file that contains it. You can save this file on
> disk and try Alt-Ergo on it with the options I gave previously
> from a terminal.
> (I hope this workflow still works with Why3 1.x ...)
It looks like it works. Thanks very much!
More information about the Why3-club