why3replayer - Man Page

execute the proofs in a Why3 session file


why3 [Options] [<FILE.why>|<DIR>]


The purpose of the why3replayer tool is to execute the proofs stored in a Why3 session file, such as the one produced by the IDE.  Its main goal is to play non-regression tests.

The tool can be invoked on a specifi file, or on a project directory containing a session file.  If the latter, all proofs in the session file are rerun.  Then, any difference between the information stored in the session file and the new run are shown.

Nothing is shown when there is no change in the results, independent of whether the considered goal is proved or not.  When all the proof runs are done, a summary of what is and is not proved is displayed using a tree-shape pretty print, similar to the IDE tree view after doing "Collapse proved goals"; that is when a goal, a theory or a file is fully proved, the subtree is not shown.


-I <dir>

Add dir to the library search path.


Force saving of the session even if replay failed.


Do not print statistics.


Print version information.

-latex <dir>

Produce LaTeX statistics in dir.

-latex <dir>

Produce LaTeX statistics in dir using an alternate tabular layout.

-html <dir>

Produce HTML statistics in dir.

-help,  --help

Show a list of options.

Exit Code

The exit code is 0 if no difference was detected, 1 if there was some difference.  Other exit codes mean some failure in running the replay.

See Also

why3(1), why3-cpulimit(1), why3bench(1), why3config(1), why3doc(1), why3ide(1), why3ml(1), why3realize(1)

Referenced By

why3(1), why3bench(1), why3config(1), why3-cpulimit(1), why3doc(1), why3ide(1), why3ml(1), why3realize(1).

1.3.3 why3