[Why3-club] lemma visibility

Mohamed Iguernlala iguer.auto at gmail.com
Thu Jan 24 13:11:09 CET 2019


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.

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
-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20190124/a2bfdac2/attachment.html>


More information about the Why3-club mailing list