1WHY3REPLAYER(1)                  User Commands                 WHY3REPLAYER(1)
2
3
4

NAME

6       why3replayer - execute the proofs in a Why3 session file
7

SYNOPSIS

9       why3 [OPTIONS] [<FILE.why>|<DIR>]
10

DESCRIPTION

12       The purpose of the why3replayer tool is to execute the proofs stored in
13       a Why3 session file, such as the one produced by  the  IDE.   Its  main
14       goal is to play non-regression tests.
15
16       The  tool  can  be invoked on a specifi file, or on a project directory
17       containing a session file.  If the latter, all proofs  in  the  session
18       file are rerun.  Then, any difference between the information stored in
19       the session file and the new run are shown.
20
21       Nothing is shown when there is no change in the results, independent of
22       whether  the considered goal is proved or not.  When all the proof runs
23       are done, a summary of what is and is not proved is displayed  using  a
24       tree-shape pretty print, similar to the IDE tree view after doing "Col‐
25       lapse proved goals"; that is when a goal, a theory or a file  is  fully
26       proved, the subtree is not shown.
27

OPTIONS

29       -I <dir>
30              Add dir to the library search path.
31
32       --force
33              Force saving of the session even if replay failed.
34
35       -s     Do not print statistics.
36
37       -v     Print version information.
38
39       -latex <dir>
40              Produce LaTeX statistics in dir.
41
42       -latex <dir>
43              Produce  LaTeX statistics in dir using an alternate tabular lay‐
44              out.
45
46       -html <dir>
47              Produce HTML statistics in dir.
48
49       -help, --help
50              Show a list of options.
51

EXIT CODE

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

SEE ALSO

57       why3(1),  why3-cpulimit(1),  why3bench(1),  why3config(1),  why3doc(1),
58       why3ide(1), why3ml(1), why3realize(1)
59
60
61
62why3                                 1.4.1                     WHY3REPLAYER(1)
Impressum