[Why3-club] lemma visibility

Julia Lawall julia.lawall at lip6.fr
Thu Jan 24 13:50:49 CET 2019



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.

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