[Why3-club] lemma visibility
iguer.auto at gmail.com
Thu Jan 24 13:11:09 CET 2019
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
Hope this helps
On 24/01/2019 12:15, Julia Lawall wrote:
> On Tue, 8 Jan 2019, Claude Marché wrote:
>> 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.
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
More information about the Why3-club