[Why3-club] lemma visibility

Mohamed Iguernlala iguer.auto at gmail.com
Thu Jan 24 14:03:46 CET 2019

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

- Mohamed.

> thanks,
> julia
>> Hope this helps
>> Regards,
>> - Mohamed.
>> On 24/01/2019 12:15, Julia Lawall wrote:
>>        On Tue, 8 Jan 2019, Claude Marché wrote:
>>              Hello,
>>              The easiest way to achieve this is to add, at the
>>              end of the module that needs
>>              a lemma "L" only internally, the declaration
>>        Is there any way to find out what lemmas alt-ergo is trying to
>>        use?  This
>>        could be helpful to figure out what to exclude.
>>        thanks,
>>        julia
>> _______________________________________________
>> Why3-club mailing list
>> Why3-club at lists.gforge.inria.fr
>> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> >

More information about the Why3-club mailing list