[Why3-club] lemma visibility
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:
>> 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
> 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
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 ...)
>> Hope this helps
>> - Mohamed.
>> 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
More information about the Why3-club