manpages.tex 43.4 KB
Newer Older
1
\chapter{Reference Manuals for the \why Tools}
2
\label{chap:manpages}
3
%HEVEA\cutname{manpages.html}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
4

5
This chapter details the usage of each of the command-line tools
Guillaume Melquiond's avatar
Guillaume Melquiond committed
6 7 8 9
provided by the \why environment. The main command is \texttt{why3};
it acts as an entry-point to all the features of \why. It is invoked
as such
\begin{verbatim}
10
why3 [general options...] <command> [specific options...]
Guillaume Melquiond's avatar
Guillaume Melquiond committed
11 12 13
\end{verbatim}

The following commands are available:
14
\begin{description}
Guillaume Melquiond's avatar
Guillaume Melquiond committed
15
\item[\texttt{config}] manages the user's configuration,
16
  including the detection of installed provers.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
17 18 19 20 21 22 23
\item[\texttt{doc}] produces HTML versions of \why source codes.
\item[\texttt{execute}] performs a symbolic execution of \whyml
  input files.
\item[\texttt{extract}] generates an OCaml program corresponding to
  \whyml input files.
\item[\texttt{ide}] provides a graphical interface to display goals
  and to run provers and transformations on them.
24
\item[\texttt{prove}] reads \whyml input files and calls
25
  provers, on the command-line.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
26 27
\item[\texttt{realize}] generates interactive proof skeletons for
  \why input files.
28
\item[\texttt{replay}] replays the proofs stored in a session,
29
  for regression test purposes.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
30
\item[\texttt{session}] dumps various informations from a proof
31
  session, and possibly modifies the session.
32 33
\item[\texttt{wc}] gives some token statistics about \whyml
  source files.
34
\end{description}
35

Guillaume Melquiond's avatar
Guillaume Melquiond committed
36 37 38 39 40
All these commands are also available as standalone executable files,
if needed.

The commands accept a common subset of command-line options. In
particular, option \verb|--help| displays the usage and options.
41
\begin{description}
42 43
\item[\texttt{-L \textsl{<dir>}}]
  adds \texttt{\textsl{<dir>}} in the load path, to search for theories.
44
  \index{L@\verb+-L+|see{\texttt{-{}-library}}}
45 46
\item[\texttt{-{}-library \textsl{<dir>}}]
  is the same as \verb|-L|.
47
  \index{library@\verb+--library+}
48 49
\item[\texttt{-C \textsl{<file>}}]
  reads the configuration from the given file.
50
  \index{C@\verb+-C+|see{\texttt{-{}-config}}}
51 52
\item[\texttt{-{}-config \textsl{<file>}}]
  is the same as \verb|-C|.
53
  \index{config@\verb+--config+}
54 55
\item[\texttt{-{}-extra-config \textsl{<file>}}]
  reads additional configuration from the given file.
56
  \index{extra-config@\verb+--extra-config+}
57
\item[\texttt{-{}-list-debug-flags}]
François Bobot's avatar
François Bobot committed
58
    list known debug flags.
59
  \index{list-debug-flags@\verb+--list-debug-flags+}
François Bobot's avatar
François Bobot committed
60 61 62 63 64 65 66 67 68 69 70 71 72 73 74
\item[\texttt{-{}-list-transforms}]
    list known transformations.
  \index{list-transforms@\verb+--list-transforms+}
\item[\texttt{-{}-list-printers}]
  list known printers.
  \index{list-printers@\verb+--list-printers+}
\item[\texttt{-{}-list-provers}]
  list known provers
  \index{list-provers@\verb+--list-provers+}
\item[\texttt{-{}-list-formats}]
  list known input formats
  \index{list-formats@\verb+--list-formats+}
\item[\texttt{-{}-list-metas}]
  list known metas
  \index{list-metas@\verb+--list-metas+}
75
\item[\texttt{-{}-debug-all}]
76
  sets all debug flags (except flags which change the behavior).
77
  \index{debug-all@\verb+--debug-all+}
78
\item[\texttt{-{}-debug \textsl{<flag>}}]
Guillaume Melquiond's avatar
Guillaume Melquiond committed
79
  sets a specific debug flag.
80
  \index{debug@\verb+--debug+}
Guillaume Melquiond's avatar
Guillaume Melquiond committed
81
\item[\texttt{-{}-help}]
82
  displays the usage and the exact list of options for the given tool.
83
  \index{help@\verb+--help+}
84
\end{description}
85

Guillaume Melquiond's avatar
Guillaume Melquiond committed
86
\section{The \texttt{config} Command}
Guillaume Melquiond's avatar
Guillaume Melquiond committed
87
\label{sec:why3config}
MARCHE Claude's avatar
add  
MARCHE Claude committed
88

MARCHE Claude's avatar
MARCHE Claude committed
89
\why must be configured to access external provers. Typically, this is done
Guillaume Melquiond's avatar
Guillaume Melquiond committed
90 91 92
by running the \texttt{config} command.
This must be done each time a new prover is installed.%
\index{config@\texttt{config}}%
93
\index{configuration file}
94

Guillaume Melquiond's avatar
Guillaume Melquiond committed
95
The provers that \why attempts to detect are described in
96
the readable configuration file \texttt{provers-detection-data.conf}
MARCHE Claude's avatar
MARCHE Claude committed
97
of the \why data directory (\eg
98 99 100
\texttt{/usr/local/share/why3}). Advanced users may try to modify this
file to add support for detection of other provers. (In that case,
please consider submitting a new prover configuration on the bug
101
tracking system.)
102

103
The result of provers detection is stored in the user's
104
configuration file (\verb+~/.why3.conf+ or, in the case of local
105
installation, \verb+why3.conf+ in \why sources top directory). This file
106
is also human-readable, and advanced users may modify it in order to
MARCHE Claude's avatar
MARCHE Claude committed
107
experiment with different ways of calling provers, \eg different
108
versions of the same prover, or with different options.
109

Guillaume Melquiond's avatar
Guillaume Melquiond committed
110
The \texttt{config} command also detects the plugins installed in the \why
MARCHE Claude's avatar
MARCHE Claude committed
111
plugins directory (\eg \texttt{/usr/local/lib/why3/plugins}). A
112 113
plugin must register itself as a parser, a transformation or a
printer, as explained in the corresponding section.
114
\index{plugin}
115 116

If the user's configuration file is already present,
Guillaume Melquiond's avatar
Guillaume Melquiond committed
117
\texttt{config} will only reset unset variables to default value,
118
but will not try to detect provers.
119
The option \verb|--detect-provers| should be used to force
MARCHE Claude's avatar
MARCHE Claude committed
120
\why to detect again the available
121
provers and to replace them in the configuration file. The option
122
\verb|--detect-plugins| will do the same for plugins.
123 124
\index{detect-provers@\verb+--detect-provers+}
\index{detect-plugins@\verb+--detect-plugins+}
125

126 127 128 129
If a supported prover is installed under a name
that is not automatically recognized by \texttt{why3config},
the option \verb|--add-prover| will add a specified binary
to the configuration. For example, an Alt-Ergo executable
130
\verb|/home/me/bin/alt-ergo-trunk| can be added as follows:
131
\begin{verbatim}
132
why3 config --add-prover alt-ergo /home/me/bin/alt-ergo-trunk
133
\end{verbatim}
134
As the first argument, one should put a prover
135 136
identification string. The list of known prover identifiers
can be obtained by the option \verb|--list-prover-ids|.
137 138
\index{add-prover@\verb+--add-prover+}
\index{list-prover-ids@\verb+--list-prover-ids+}
139

Guillaume Melquiond's avatar
Guillaume Melquiond committed
140
\section{The \texttt{prove} Command}
MARCHE Claude's avatar
MARCHE Claude committed
141
\label{sec:why3ref}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
142

MARCHE Claude's avatar
MARCHE Claude committed
143
\why is primarily used to call provers on goals contained in an
144
input file. By default, such a file must be written in \whyml language
François Bobot's avatar
François Bobot committed
145
(extension \texttt{.mlw}).
146
However, a dynamically loaded
147
plugin can register a parser for some other format of logical problems,
MARCHE Claude's avatar
MARCHE Claude committed
148
\eg TPTP or SMT-LIB.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
149
\index{prove@\texttt{prove}}
150

Guillaume Melquiond's avatar
Guillaume Melquiond committed
151
The \texttt{prove} command executes the following steps:
152
\begin{enumerate}
153
\item Parse the command line and report errors if needed.
154
\item Read the configuration file using the priority defined in
155 156 157 158
  Section~\ref{sec:whyconffile}.
\item Load the plugins mentioned in the configuration. It will not
  stop if some plugin fails to load.
\item Parse and typecheck the given files using the correct parser in order
MARCHE Claude's avatar
MARCHE Claude committed
159
  to obtain a set of \why theories for each file. It uses
160
  the filename extension or the \verb|--format| option to choose
161 162 163
  among the available parsers. \verb|why3 --list-formats| lists
  the registered parsers.
  \index{list-formats@\verb+--list-formats+}
164 165
  \whyml modules are turned into
  theories containing verification conditions as goals.
166
\item Extract the selected goals inside each of the selected theories
167 168
  into tasks. The goals and theories are selected using options
  \verb|-G/--goal| and \verb|-T/--theory|. Option
169 170
  \verb|-T/--theory| applies to the previous file appearing on the
  command line. Option \verb|-G/--goal| applies to the previous theory
171 172 173
  appearing on the command line. If no theories are selected in a file,
  then every theory is considered as selected. If no goals are selected
  in a theory, then every goal is considered as selected.
174 175 176 177
  \index{G@\verb+-G+|see{\texttt{-{}-goal}}}
  \index{goal@\verb+--goal+}
  \index{T@\verb+-T+|see{\texttt{-{}-theory}}}
  \index{theory@\verb+--theory+}
178
\item Apply the transformations requested
179
  with \verb|-a/--apply-transform| in their order of appearance on the
180 181
  command line. \verb|why3 --list-transforms| lists the known
  transformations; plugins can add more of them.
182 183 184
  \index{a@\verb+-a+|see{\texttt{-{}-apply-transform}}}
  \index{apply-transform@\verb+--apply-transform+}
  \index{list-transforms@\verb+--list-transforms+}
185
\item Apply the driver selected with the \verb|-D/--driver| option,
186
  or the driver of the prover selected with the \verb|-P/--prover|
187
  option. \verb|why3 --list-provers| lists the known provers, \ie the ones
188
  that appear in the configuration file.
189 190 191 192
  \index{D@\verb+-D+|see{\texttt{-{}-driver}}}
  \index{driver@\verb+--driver+}
  \index{P@\verb+-P+|see{\texttt{-{}-prover}}}
  \index{prover@\verb+--prover+}
193
  \index{list-provers@\verb+--list-provers+}
194 195
\item If option \verb|-P/--prover| is given, call the selected prover
  on each generated task and print the results. If option
196
  \verb|-D/--driver| is given, print each generated task using
197
  the format specified in the selected driver.
198 199
\end{enumerate}

200 201
%\texttt{why3} calls the provers sequentially, use \texttt{why3bench} if *)
%you want to call the provers concurrently.  *)
MARCHE Claude's avatar
MARCHE Claude committed
202

203
\subsection{Prover Results}
Guillaume Melquiond's avatar
Guillaume Melquiond committed
204
The provers can give the following output:
François Bobot's avatar
François Bobot committed
205
\begin{description}
206 207 208 209 210
\item[Valid] The goal is proved in the given context.
\item[Unknown] The prover has stopped its search.
\item[Timeout] The prover has reached the time limit.
\item[Failure] An error has occurred.
\item[Invalid] The prover knows the goal cannot be proved.
François Bobot's avatar
François Bobot committed
211
\end{description}
MARCHE Claude's avatar
MARCHE Claude committed
212
% \why can also be *)
MARCHE Claude's avatar
MARCHE Claude committed
213 214 215 216 217 218
% used to provide other informations : *)
% \begin{itemize} *)
% \item \texttt{print-namespace} print the namespace of the selected *)
%   theories *)
% \item TO BE COMPLETED *)
% \end{itemize} *)
219

Guillaume Melquiond's avatar
Guillaume Melquiond committed
220 221 222 223 224 225 226 227 228 229
%Option \verb|--bisect| changes the behavior of why3. With this
%option, \verb|-P/--prover| and \verb|-o/--output| must be given
%and a valid goal must be selected. The last step executed by why3 is
%replaced by computing a minimal set (in the great majority of the
%case) of declarations that still prove the goal. Currently it does not
%use any information provided by the prover; it calls the prover
%multiple times with reduced context. The minimal set of declarations is
%then written in the prover syntax into a file located in the directory
%given to the \verb|-o/--output| option.

230 231 232 233
\subsection{Additional Options}
\label{sec:proveoptions}

\begin{description}
234 235
%\item[\texttt{-{}-get-ce}] activates the generation of a potential
%counter-example when a proof does not succeed (experimental).
236 237 238 239 240 241
\item[\texttt{-{}-extra-expl-prefix \textsl{<s>}}] specifies
  \textsl{s} as an additional prefix for labels that denotes VC
  explanations. The option can be used several times to specify
  several prefixes.
\end{description}

Guillaume Melquiond's avatar
Guillaume Melquiond committed
242
\section{The \texttt{ide} Command}
MARCHE Claude's avatar
MARCHE Claude committed
243 244
\label{sec:ideref}

245
The basic usage of the GUI is described by the tutorial of
246 247 248 249 250 251 252 253 254 255
Section~\ref{sec:gui}. The command-line options are the common options
detailed in introduction to this chapter, plus the specific option
already described for the command \texttt{prove} in
Section~\ref{sec:proveoptions}.
\begin{description}
\item[\texttt{-{}-extra-expl-prefix \textsl{<s>}}]
\end{description}
At least one anonymous argument must be specified on the command
line. More precisely, the first anonymous argument must be the
directory of the session. If the directory does not exist, it is
256
created. The other arguments should be existing files that are going
257 258 259 260
to be added to the session. For convenience, if there is only one
anonymous argument, it can be an existing file and in this case the
session directory is obtained by removing the extension from the file
name.
261

262 263
We describe the actions of the various menus and buttons of the
interface.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
264
\index{ide@\texttt{ide}}
265 266 267

\subsection{Session}
\label{sec:idref:session}
Guillaume Melquiond's avatar
Guillaume Melquiond committed
268 269
\why stores in a session the way you achieve to prove goals that come
from a file (\texttt{.why}), from weakest-precondition (\texttt{.mlw}) or by other
270 271 272 273
means. A session stores which file you prove, by applying which
transformations, by using which prover. A proof attempt records the
complete name of a prover (name, version, optional attribute), the
time limit and memory limit given, and the result of the prover. The
Guillaume Melquiond's avatar
Guillaume Melquiond committed
274
result of the prover is the same as when you run the \texttt{prove} command. It
275
contains the time taken and the state of the proof:
276

277 278
\begin{description}
\item[Valid] The task is valid according to the prover. The
279
  goal is considered proved.
280 281 282 283 284 285 286
\item[Invalid] The task is invalid.
\item[Timeout] the prover exceeded the time limit.
\item[OufOfMemory] The prover exceeded the memory limit.
\item[Unknown] The prover cannot determine if the task
  is valid. Some additional information can be provided.
\item[Failure] The prover reported a failure.
\item[HighFailure] An error occurred while trying to call the
287
  prover, or the prover answer was not understood.
288
\end{description}
289

290
Additionally, a proof attempt can have the following attributes:
291

292 293 294
\begin{description}
\item[obsolete]\index{obsolete!proof attempt} The prover associated to
  that proof attempt has not been run on the current task, but on an
MARCHE Claude's avatar
MARCHE Claude committed
295
  earlier version of that task. You need to replay the proof
MARCHE Claude's avatar
MARCHE Claude committed
296
  attempt, \ie run the prover with the current task of the proof
MARCHE Claude's avatar
MARCHE Claude committed
297 298
  attempt, in order to update the answer of the prover and remove this
  attribute.
299 300 301 302 303 304 305 306
\item[detached]\index{detached!proof attempt} The proof attempt is not
  associated to a proof task anymore. The reason might be that a proof
  goal disappeared, or that there is a syntax or typing error in the
  current file, that makes all nodes temporarily detached until the
  parsing error is fixed. Detached nodes of the session tree are kept
  until they are explicitly removed, either using a remove command or
  the clean command. They can be reused, as any other nodes, using the
  copy/paste operation.
307
\end{description}
308

309
Generally, proof attempts are marked obsolete just after
Guillaume Melquiond's avatar
Guillaume Melquiond committed
310 311
the start of the user interface. Indeed, when you load a session in order to
modify it (not with \texttt{why3session info} for instance), \why
312
rebuilds the goals to prove by using the information provided in the
313
session. If you modify the original file (\texttt{.mlw}) or if the
Guillaume Melquiond's avatar
Guillaume Melquiond committed
314 315 316
transformations have changed (new version of \why), \why will detect
that. Since the provers might answer differently on these new
proof obligations, the corresponding proof attempts are marked obsolete.
MARCHE Claude's avatar
MARCHE Claude committed
317

318
\subsection{Context Menu}
319

320 321 322
The left toolbar that was present in former versions of Why3 is now
replaced by a context menu activited by clicking the right mouse button,
while cursor is on a given row of the proof session tree.
323

324 325 326
\begin{description}
\item[provers] The detected provers are listed. Note that you can hide some provers of that list using the preferences, tab \textsf{Provers}.
\item[strategies] the set of known strategies is listed
327
\item[Edit] starts an editor on the selected task.
328 329
\item[Replay valid obsolete proofs] all proof nodes below the selected nodes that are obsolete but whose former status was Valid are replayed.
\item[Replay all obsolete proofs] all proof nodes below the selected nodes that are obsolete are replayed.
330 331 332 333
\item[Remove] removes a proof attempt or a transformation.
\item[Clean] removes any unsuccessful proof attempt for which there is
  another successful proof attempt for the same goal
\item[Interrupt] cancels all the proof attempts currently scheduled or running.
334
\end{description}
335

336 337 338
\subsection{Global Menus}

\begin{description}
339 340
\item[Menu \textsf{File}]\emptyitem
\begin{description}
341
\item[Add File to session] adds a file in the current proof session.
342
%\item[Detect provers] runs provers auto-detection
343
\item[Preferences] opens a window for modifying preferred
344 345
  configuration parameters, see details below.
\item[Save session] saves current session state on disk. The policy to decide when to save the session is configurable, as described in the preferences below.
346 347 348
\item[Save files] saves edited soruce files on disk.
\item[Save session and files] saves both current session state and edited files on disk.
\item[Save all and Refresh session] save session and edited files, and refresh the current session tree.
349 350
\item[Quit] exits the GUI.
\end{description}
MARCHE Claude's avatar
MARCHE Claude committed
351

352
\item[Menu \textsf{Tools}]\emptyitem
MARCHE Claude's avatar
MARCHE Claude committed
353
\begin{description}
354 355 356
\item[Strategies] section provides a set of actions that are
  performed on the selected goal(s):
  \begin{description}
357 358 359 360 361 362
  \item[Split VC] splits the current goal into subgoals.
  % \item[Inline] inlines the definitions in the conclusion of the goal.
  %   It corresponds to the \verb|introduce_premises| transformation
  %   follwoed by \verb|inline_goal|.
  \item[Auto level 0] is a basic proof search strategy that applies a few provers
    on the goal with a short time limit.
363 364 365 366 367 368 369 370 371 372 373
  \item[Auto level 1] is a strategy that first applies a few provers
    on the goal with a short time limit, then splits the goal and
    tries again on the subgoals
  \item[Auto level 2] is a strategy more elaborate than level 1, that
    attempts to apply a few transformations that are typically
    useful. It also tries the provers with a larger time limit.
  \end{description}
  A more detailed description of strategies is given in
  Section~\ref{sec:strategies}, as well as a description on how to
  design strategies of your own.

374 375 376 377 378 379
\item[Provers] provide a menu item for each detected prover. Clicking on
  such an item starts the corresponding prover on the selected
  goal(s). To start a prover with a different time limit, you may
  either change the default time limit in the Preferences, or using
  the text command field and type the prover name followed by the time
  limit.
MARCHE Claude's avatar
MARCHE Claude committed
380

381
\item[Transformations] gives access to all the known transformations.
MARCHE Claude's avatar
MARCHE Claude committed
382

383
\item[Edit] starts an editor on the selected task.
MARCHE Claude's avatar
MARCHE Claude committed
384 385 386 387 388 389 390 391

  For automatic provers, this allows to see the file sent to the
  prover.

  For interactive provers, this also allows to add or modify the
  corresponding proof script. The modifications are saved, and can be
  retrieved later even if the goal was modified.

392
\item[Replay valid obsolete proofs] replays all the obsolete proofs below the current node whose former state was Valid.
MARCHE Claude's avatar
MARCHE Claude committed
393

394
\item[Replay all obsolete proofs] replays all the obsolete proofs below the current node.
MARCHE Claude's avatar
MARCHE Claude committed
395

396
\item[Clean] removes any unsuccessful proof attempt for which there is
MARCHE Claude's avatar
MARCHE Claude committed
397 398
  another successful proof attempt for the same goal

399 400 401 402 403
\item[Remove] removes a proof attempt or a transformation.

\item[Mark obsolete] marks all the proof as
  obsolete.  This allows to replay every proof.

404
\item[Interrupt] cancels all the proof attempts currently scheduled or running.
405

406
\item[Bisect] performs a reduction of the context for the the current selected proof attempt, which must be a Valid one.
407

408
\item[Focus] focus the tree session view to the current node
409

410
\item[Unfocus] undoes the Focus action
411

412
\item[Copy] Marks of proof sub-tree for copy/past action
413

414
\item[Paste] Paste the previously selected sub-tree under the current node
415

Guillaume Melquiond's avatar
Guillaume Melquiond committed
416
\end{description}
417

418 419
\item[Menu \textsf{View}]\emptyitem
\begin{description}
420 421
\item[Enlarge font] selects a large font
\item[Reduce font] selects a smaller font
422 423
\item[Collapse proved goals] closes all the rows of the tree view
  that are proved.
424 425 426 427 428 429 430 431
\item[Expand All] expands all the rows of the tree view.
\item[Collapse under node] closes all the rows of the tree view under the given node
  that are proved.
\item[Expand below node] expands the children below the current node
\item[Expand all below node] expands the whole subtree of the current node
\item[Go to parent node] move to the parent of the current node
\item[Go to first child] mode to the first child of the current node
\item[Select next unproven goal] go to the next unproven goal after the current node
432 433 434
\end{description}


435 436 437 438 439 440 441 442
\item[Menu \textsf{Help}]\emptyitem
\begin{description}
\item[Legend]
Explanations of the meaning of the various icons
\item[About]
some information about this software.
\end{description}

Guillaume Melquiond's avatar
Guillaume Melquiond committed
443
\end{description}
444

445 446 447 448 449 450 451 452 453 454 455
\subsection{Command-line interface}

Between the top-right zone containing source files and task, and the
bottom-right zone containing various messages, a text input field
allows the user to invoke commands using a textual interface (see
Figure~\ref{fig:gui1}). The 'help' command displays a basic list of
available commands. All commands available in the menus are also
available as a textual command. However the textual interface allows
for much more possibilities, including the ability to invoke
transformations with arguments.

456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478
\subsection{Key shortcuts}


\begin{itemize}
\item Save session and files : ctrl+s
\item Save all and refresh session: ctrl+r
\item Quit : ctrl+q
\item Enlarge font : ctrl+plus
\item Reduce font : ctrl+minus
\item Collapse proven goals : !
\item Collapse current node : -
\item Expand current node : +
\item Copy : ctrl+c
\item Paste : ctrl+v
\item Select parent node : ctrl+up
\item Select next unproven goal : ctrl+down
\item Change focus to command line : return
\item Edit : e
\item Replay : r
\item Clean : c
\item Remove : del
\item Mark obsolete : o
\end{itemize}
479

480
\subsection{Preferences Dialog}
MARCHE Claude's avatar
MARCHE Claude committed
481

482 483
The preferences dialog allows you to customize various settings. They
are grouped together under several tabs.
484

485 486 487 488 489 490 491
Note that there are to different buttons to close that dialog. The
``Close'' button will make modifications of any of these settings
effective only for the current run of the GUI. The ``Save\&Close''
button will save the modified settings in Why3 configuration file, to
make them permanent.


492
\begin{description}
493
\item[\textsf{General Settings} tab] allows one to set
494
  various general settings.
MARCHE Claude's avatar
MARCHE Claude committed
495
\begin{itemize}
496 497 498 499 500 501
\item the limits set on resource usages:
  \begin{itemize}
  \item the time limit given to provers, in seconds
  \item the memory given to provers, in megabytes
  \item the maximal number of simultaneous provers allowed to run in parallel
  \end{itemize}
502 503
\item option to disallow source editing within the GUI
\item the policy for saving sessions:
504 505
  \begin{itemize}
  \item always save on exit (default): the current state of the proof session is saving on exit
506 507 508
  \item never save on exit: the current state of the session is never saved
    automatically, you must use menu \textsf{File/Save session}
  \item ask whether to save: on exit, a popup window asks whether you
509 510
    want to save or not.
  \end{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
511
\end{itemize}
512 513 514 515 516 517 518 519 520 521 522 523 524 525

\item[\textsf{Appearance settings} tab]\emptyitem
  \begin{itemize}
  \item show full task context: by default, only the local context of
    formulas is shown, that is only the declarations comming from the
    same module
  \item show attributes in formulas
  \item show corecions in formulas
  \item show source locations in formulas
  \item show time and memory limits for each proof
  \end{itemize}
  Finally, it is possible to choose an alternative icon set, provided,
  one is installed first.

526
\item[\textsf{Editors} tab] allows one to customize the use
527 528 529 530
  of external editors for proof scripts.
\begin{itemize}
\item The default editor to use when the \textsf{Edit} button is
  pressed.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
531
  \urldef{\urlprfgen}{\url}{http://proofgeneral.inf.ed.ac.uk/}
532 533 534
\item For each installed prover, a specific editor can be selected to
  override the default. Typically if you install the Coq prover, then
  the editor to use will be set to ``CoqIDE'' by default, and this
535
  dialog allows you to select the Emacs editor and its
536 537
 \ahref{\urlprfgen}{Proof General} mode instead%
 \begin{latexonly} (\urlprfgen)\end{latexonly}.
538
\end{itemize}
539
\item[\textsf{Provers} tab]
540
  allows to select which of the installed provers one wants to see
541
  in the context menu.
542 543
\item[\textsf{Uninstalled Provers} tab] presents all the
  decision previously taken for missing provers, as described in
544 545 546
  Section~\ref{sec:uninstalledprovers}. You can remove any recorded
  decision by clicking on it.
\end{description}
MARCHE Claude's avatar
MARCHE Claude committed
547

548 549
\subsection{Displaying Counterexamples}

550 551 552 553 554 555 556 557 558 559 560 561 562
Why3 provides some support for extracting a potential counterexample
from failing proof attempts. It is possible to display parts of this
model in the terms of the original Why3 input.  Currently, this is
supported for CVC4 prover version 1.5 and Z3.

The counterexamples are enable when using a prover under the
alternative form called ``coutnerexamples''. After running the prover
and clicking on the prover result in, the counterexample can be
displayed in the tab Counter-example.  The counterexample is displayed
with the original Why3 code in comments.  Counterexample values for
Why3 source code elements at given line are displayed in a comment at
the line below.

MARCHE Claude's avatar
MARCHE Claude committed
563
More information how counterexamples in Why3 works can be found
564 565
in~\cite{hauzar16sefm} and in~\cite{dailler18jlamp}.

566

567
%
568
% how to use counterexamples - explain labels, projections, the option --get-ce of why3prove and the setting in why3ide
569
%
570
% problem with set logic and counterexamples
571
%
572
% which provers
573
%
574
% where it is displayed
575
%
576
% how to interpret the display
577
%
578 579
% example

580 581


582
\section{The \texttt{replay} Command}
583
\label{sec:why3replayer}
MARCHE Claude's avatar
MARCHE Claude committed
584

585
The \texttt{replay} command is meant to execute the proofs
Guillaume Melquiond's avatar
Guillaume Melquiond committed
586 587 588
stored in a \why session file, as produced by the IDE. Its
main purpose is to play non-regression tests. For instance,
\texttt{examples/regtests.sh} is a script that runs regression tests on
589
all the examples.
590
\index{replay@\texttt{replay}}
MARCHE Claude's avatar
MARCHE Claude committed
591

MARCHE Claude's avatar
MARCHE Claude committed
592
The tool is invoked in a terminal or a script using
MARCHE Claude's avatar
MARCHE Claude committed
593
\begin{flushleft}\ttfamily
594
  why3 replay \textsl{[options] <project directory>}
MARCHE Claude's avatar
MARCHE Claude committed
595 596 597
\end{flushleft}
The session file \texttt{why3session.xml} stored in the given
directory is loaded and all the proofs it contains are rerun. Then,
Guillaume Melquiond's avatar
Guillaume Melquiond committed
598
all the differences between the information stored in the session file and
599
the new run are shown.
MARCHE Claude's avatar
MARCHE Claude committed
600

Guillaume Melquiond's avatar
Guillaume Melquiond committed
601 602
Nothing is shown when there is no change in the results, whether the
considered goal is proved or not. When all the proof
603
are done, a summary of what is proved or not is displayed using a
MARCHE Claude's avatar
MARCHE Claude committed
604
tree-shape pretty print, similar to the IDE tree view after doing
Guillaume Melquiond's avatar
Guillaume Melquiond committed
605 606
``Collapse proved goals''. In other words, when a goal, a theory, or a
file is fully proved, the subtree is not shown.
MARCHE Claude's avatar
MARCHE Claude committed
607

MARCHE Claude's avatar
MARCHE Claude committed
608 609
\paragraph{Obsolete proofs}

MARCHE Claude's avatar
MARCHE Claude committed
610 611
When some proof attempts stored in the session file are
obsolete\index{obsolete!proof attempt},
612
the replay is run anyway, as with the replay button in the IDE. Then, the session
MARCHE Claude's avatar
MARCHE Claude committed
613
file will be updated if both
614 615 616 617 618 619
\begin{itemize}
\item all the replayed proof attempts give the same result as what
  is stored in the session
\item every goals are proved.
\end{itemize}
In other cases, you can use the IDE to update the session, or use the
620
option \verb|--force| described below.
MARCHE Claude's avatar
MARCHE Claude committed
621 622

\paragraph{Exit code and options}
MARCHE Claude's avatar
MARCHE Claude committed
623

624 625 626 627 628 629 630
The exit code is 0 if no difference was detected, 1 if there
was. Other exit codes mean some failure in running the replay.

Options are:
\begin{description}
\item[\texttt{-s}] suppresses the output of the final tree view.
\item[\texttt{-q}] runs quietly (no progress info).
631
\item[\texttt{-{}-force}] enforces saving the session, if all proof
632
  attempts replayed correctly, even if some goals are not proved.
633
\item[\texttt{-{}-obsolete-only}] replays the proofs only if the session
MARCHE Claude's avatar
MARCHE Claude committed
634
  contains obsolete proof attempts.
635
\item[\texttt{-{}-smoke-detector \{none|top|deep\}}] tries to detect
636
  if the context is self-contradicting.
637 638
\item[\texttt{-{}-prover \textsl{<prover>}}] restricts the replay to the
  selected provers only.
639
\end{description}
MARCHE Claude's avatar
MARCHE Claude committed
640

Guillaume Melquiond's avatar
Guillaume Melquiond committed
641
\paragraph{Smoke detector}
642

643 644 645 646
The smoke detector tries to detect if the context is
self-contradicting and, thus, that anything can be proved in this
context. The smoke detector can't be run on an outdated session and does
not modify the session.  It has three possible configurations:
647 648 649
\begin{description}
\item[\texttt{none}] Do not run the smoke detector.
\item[\texttt{top}] The negation of each proved goal is sent with the
650
  same timeout to the prover that proved the original goal.
651
\begin{verbatim}
652
  Goal G : forall x:int. q x -> (p1 x \/ p2 x)
653
\end{verbatim}
654
  becomes
655
\begin{verbatim}
656
  Goal G : ~ (forall x:int. q x -> (p1 x \/ p2 x))
657
\end{verbatim}
658 659
  In other words, if the smoke detector is triggered, it means that the context
  of the goal \texttt{G} is self-contradicting.
660
\item[\texttt{deep}] This is the same technique as \texttt{top} but
661 662 663
  the negation is pushed under the universal quantification (without
  changing them) and under the implication. The previous example
  becomes
664
\begin{verbatim}
665
  Goal G : forall x:int. q x /\ ~ (p1 x \/ p2 x)
666
\end{verbatim}
667 668 669 670 671
  In other words, the premises of goal \texttt{G} are pushed in the
  context, so that if the smoke detector is triggered, it means that
  the context of the goal \texttt{G} and its premises are
  self-contradicting. It should be clear that detecting smoke in that
  case does not necessarily means that there is a mistake: for
672
  example, this could occur in the WP of a program with an unfeasible
673
  path.
674
\end{description}
675

676 677
At the end of the replay, the name of the goals that triggered the
smoke detector are printed:
678
\begin{verbatim}
679
  goal 'G', prover 'Alt-Ergo 0.93.1': Smoke detected!!!
680
\end{verbatim}
681 682 683
Moreover \texttt{Smoke detected} (exit code 1) is printed at the end
if the smoke detector has been triggered, or \texttt{No smoke
  detected} (exit code 0) otherwise.
684 685


Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
686

Guillaume Melquiond's avatar
Guillaume Melquiond committed
687
\section{The \texttt{session} Command}
688
\label{sec:why3session}
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
689

Guillaume Melquiond's avatar
Guillaume Melquiond committed
690
The \texttt{session} command makes it possible to extract information from
691 692 693
proof sessions on the command line, or even modify them to some
extent. The invocation of this program is done under the form
\begin{verbatim}
Guillaume Melquiond's avatar
Guillaume Melquiond committed
694
why3 session <subcommand> [options] <session directories>
695
\end{verbatim}
Guillaume Melquiond's avatar
Guillaume Melquiond committed
696
The available subcommands are as follows:
697 698 699 700 701 702
\begin{description}
\item[\texttt{info}] prints informations and statistics about sessions.
\item[\texttt{latex}] outputs session contents in LaTeX format.
\item[\texttt{html}] outputs session contents in HTML format.
\item[\texttt{mod}] modifies some of the proofs, selected by a filter.
\item[\texttt{copy}] duplicates some of the proofs, selected by a filter.
703
\item[\texttt{rm}] removes some of the proofs, selected by a filter.
704 705
\end{description}

706 707
The first three commands do not modify the sessions, whereas the last
four modify them. Only the proof attempts recorded are modified. No
708
prover is called on the modified or created proof attempts, and
MARCHE Claude's avatar
MARCHE Claude committed
709
consequently the proof status is always marked as obsolete.
710 711

\subsection{Command \texttt{info}}
712

Guillaume Melquiond's avatar
Guillaume Melquiond committed
713
The command \texttt{why3 session info} reports various informations
MARCHE Claude's avatar
MARCHE Claude committed
714 715 716
about the session, depending on the following specific options.
\begin{description}
\item[\texttt{-{}-provers}] prints the provers that appear inside
MARCHE Claude's avatar
MARCHE Claude committed
717
  the session, one by line.
MARCHE Claude's avatar
MARCHE Claude committed
718
\item[\texttt{-{}-edited-files}] prints all the files that appear in
MARCHE Claude's avatar
MARCHE Claude committed
719
  the session as edited proofs.
MARCHE Claude's avatar
MARCHE Claude committed
720
\item[\texttt{-{}-stats}] prints various proofs statistics, as
721
  detailed below.
722 723 724
% OBSOLETE
% \item[\texttt{-{}-tree}] prints the structure of the session as a
%   tree in ASCII, as detailed below.
MARCHE Claude's avatar
MARCHE Claude committed
725
\item[\texttt{-{}-print0}] separates the results of the options
MARCHE Claude's avatar
MARCHE Claude committed
726 727 728 729 730
  \verb|provers| and \verb|--edited-files| by the character number 0
  instead of end of line \verb|\n|. That allows you to safely use
  (even if the filename contains space or carriage return) the result
  with other commands. For example you can count the number of proof
  line in all the coq edited files in a session with:
731
\begin{verbatim}
Guillaume Melquiond's avatar
Guillaume Melquiond committed
732
why3 session info --edited-files vstte12_bfs --print0 | xargs -0 coqwc
733 734 735 736
\end{verbatim}
  or you can add all the edited files in your favorite repository
  with:
\begin{verbatim}
Guillaume Melquiond's avatar
Guillaume Melquiond committed
737
why3 session info --edited-files --print0 vstte12_bfs.mlw | \
738 739 740
    xargs -0 git add
\end{verbatim}

MARCHE Claude's avatar
MARCHE Claude committed
741 742
\end{description}

743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775

% OBSOLETE

% \paragraph{Session Tree}

% The hierarchical structure of the session is printed as a tree in
% ASCII. The files, theories, goals are marked with a question mark
% \verb|?|, if they are not verified. A proof is usually said to be
% verified if the proof result is \verb|valid| and the proof is not
% obsolete.
% However here specially we separate these two properties. On
% the one hand if the proof suffers from an internal failure we mark it
% with an exclamation mark \verb|!|, otherwise if it is not valid we
% mark it with a question mark \verb|?|, finally if it is valid we add
% nothing. On the other hand if the proof is obsolete we mark it with an
% \verb|O|.

% For example, here are the session tree produced on the ``hello
% proof'' example of Section~\ref{chap:starting}.
% {\scriptsize
% \begin{verbatim}
% hello_proof---../hello_proof.why?---HelloProof?-+-G3-+-Simplify (1.5.4)?
%                                                 |    `-Alt-Ergo (0.94)
%                                                 |-G2?-+-split_goal?-+-G2.2-+-Simplify (1.5.4)
%                                                 |     |             |      `-Alt-Ergo (0.94)
%                                                 |     |             `-G2.1?-+-Coq (8.3pl4)?
%                                                 |     |                     |-Simplify (1.5.4)?
%                                                 |     |                     `-Alt-Ergo (0.94)?
%                                                 |     |-Simplify (1.5.4)?
%                                                 |     `-Alt-Ergo (0.94)?
%                                                 `-G1---Simplify (1.5.4)
% \end{verbatim}
% }
776

777 778
\paragraph{Session Statistics}

779 780 781 782 783
The proof statistics given by option \verb|--stats| are as follows:
\begin{itemize}
\item Number of goals: give both the total number of goals, and the
  number of those that are proved (possibly after a transformation).
\item Goals not proved: list of goals of the session which are not
MARCHE Claude's avatar
MARCHE Claude committed
784 785
  proved by any prover, even after a transformation.
\item Goals proved by only one prover: the goals for which there is only
786 787 788
  one successful proof. For each of these, the prover which was
  successful is printed. This also includes the sub-goals generated by
  transformations.
MARCHE Claude's avatar
MARCHE Claude committed
789
\item Statistics per prover: for each of the prover used in the
790
  session, the number of proved goals is given. This also includes the
MARCHE Claude's avatar
MARCHE Claude committed
791 792 793
  sub-goals generated by transformations. The respective minimum,
  maximum and average time and on average running time is
  shown. Beware that these time data are computed on the
794
  goals \emph{where the prover was successful}.
795 796
\end{itemize}

797 798
For example, here are the session statistics produced on the ``hello
proof'' example of Section~\ref{chap:starting}.
799
{\footnotesize
800
\begin{verbatim}
801 802 803 804 805
== Number of root goals ==
  total: 3  proved: 2

== Number of sub goals ==
  total: 2  proved: 1
806 807 808 809 810

== Goals not proved ==
  +-- file ../hello_proof.why
    +-- theory HelloProof
      +-- goal G2
811 812
        +-- transformation split_goal_right
          +-- goal G2.0
813 814 815 816

== Goals proved by only one prover ==
  +-- file ../hello_proof.why
    +-- theory HelloProof
817 818 819 820 821
      +-- goal G1: Alt-Ergo 0.99.1
      +-- goal G2
        +-- transformation split_goal_right
          +-- goal G2.1: Alt-Ergo 0.99.1
      +-- goal G3: Alt-Ergo 0.99.1
822 823

== Statistics per prover: number of proofs, time (minimum/maximum/average) in seconds ==
824
  Alt-Ergo 0.99.1     :   3   0.00   0.00   0.00
825
\end{verbatim}
826
}
827 828 829

\subsection{Command \texttt{latex}}

MARCHE Claude's avatar
MARCHE Claude committed
830 831 832
Command \texttt{latex} produces a summary of the replay under the form
of a tabular environment in LaTeX, one tabular for each theory, one
per file.
833

MARCHE Claude's avatar
MARCHE Claude committed
834 835
The specific options are
\begin{description}
836
\item[\texttt{-style \textsl{<n>}}] sets output style (1 or 2, default 1)
MARCHE Claude's avatar
MARCHE Claude committed
837 838
  Option \texttt{-style 2} produces an alternate version of LaTeX
  output, with a different layout of the tables.
839 840 841
\item[\texttt{-o \textsl{<dir>}}] indicates where
  to produce LaTeX files (default: the session directory).
\item[\texttt{-longtable}] uses the `longtable' environment instead of
842
  `tabular'.
843 844
\item[\texttt{-e \textsl{<elem>}}] produces a table for the given element, which is
  either a file, a theory or a root goal. The element must be specified
845
  using its path in dot notation, \eg \verb|file.theory.goal|. The
846
  file produced is named accordingly,
847
  \eg \verb|file.theory.goal.tex|.  This option can be given several
848 849 850
  times to produce several tables in one run. When this option is
  given at least once, the default behavior that is to produce one
  table per theory is disabled.
MARCHE Claude's avatar
MARCHE Claude committed
851
\end{description}
852 853 854 855 856 857

\paragraph{Customizing LaTeX output}

The generated LaTeX files contain some macros that must be defined
externally.  Various definitions can be given to them to customize the
output.
MARCHE Claude's avatar
MARCHE Claude committed
858
\begin{description}
859 860 861
\item[\texttt{\bs{}provername}] macro with one parameter, a prover name
\item[\texttt{\bs{}valid}] macro with one parameter, used where the corresponding prover answers that the goal is valid. The parameter is the time in seconds.
\item[\texttt{\bs{}noresult}] macro without parameter, used where no result
862
  exists for the corresponding prover
863 864
\item[\texttt{\bs{}timeout}] macro without parameter, used where the corresponding prover reached the time limit
\item[\texttt{\bs{}explanation}] macro with one parameter, the goal name or its explanation
MARCHE Claude's avatar
MARCHE Claude committed
865
\end{description}
866 867

\begin{figure}[t]
868
\begin{center}
869
\lstinputlisting[basicstyle={\ttfamily\small}]{./replayer_macros.tex}
870 871 872 873 874 875 876
\end{center}
\caption{Sample macros for the LaTeX command}
\label{fig:custom-latex}
\end{figure}

\begin{figure}[t]
\begin{center}
MARCHE Claude's avatar
MARCHE Claude committed
877
%HEVEA\begin{toimage}
878
\input{HelloProof.tex}
MARCHE Claude's avatar
MARCHE Claude committed
879
%HEVEA\end{toimage}
880 881
%HEVEA\imageflush
\end{center}
882
\caption{LaTeX table produced for the HelloProof example (style 1)}
MARCHE Claude's avatar
MARCHE Claude committed
883
\label{fig:latex}
884 885
\end{figure}

886 887
\begin{figure}[t]
\begin{center}
MARCHE Claude's avatar
MARCHE Claude committed
888
%HEVEA\begin{toimage}
889
\input{HelloProof-style2.tex}
MARCHE Claude's avatar
MARCHE Claude committed
890
%HEVEA\end{toimage}
891 892 893 894 895 896 897 898 899 900
%HEVEA\imageflush
\end{center}
\caption{LaTeX table produced for the HelloProof example (style 2)}
\label{fig:latexstyle2}
\end{figure}

Figure~\ref{fig:custom-latex} suggests some definitions for these
macros, while Figures~\ref{fig:latex} and~\ref{fig:latexstyle2} show
the tables obtained from the HelloProof example of
Section~\ref{chap:starting}, respectively with style 1 and 2.
901 902 903 904

\subsection{Command \texttt{html}}

This command produces a summary of the proof session in HTML syntax.
905 906
There are two styles of output: `table' and `simpletree'. The default is
`table'.
MARCHE Claude's avatar
MARCHE Claude committed
907

908 909 910 911
The file generated is named \texttt{why3session.html} and is written
in the session directory by default (see option \texttt{-o} to
override this default).

MARCHE Claude's avatar
MARCHE Claude committed
912
\begin{figure}[t]
MARCHE Claude's avatar
MARCHE Claude committed
913
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
914
\begin{center}
915
\fbox{\includegraphics[width=0.9\textwidth]{hello_proof.png}}
MARCHE Claude's avatar
MARCHE Claude committed
916
\end{center}
MARCHE Claude's avatar
MARCHE Claude committed
917
%END LATEX
918 919
\begin{htmlonly}
\begin{rawhtml}
MARCHE Claude's avatar
MARCHE Claude committed
920
<h1>Why3 Proof Results for Project "hello_proof"</h1>
921 922 923 924 925 926 927 928
<h2><span style="color:#FF0000">Theory "hello_proof.HelloProof": not fully verified</span></h2>
<table border="1" style="border-collapse:collapse"><tr><td colspan="2">Obligations</td><td text-rotation="90">Alt-Ergo 0.99.1</td><td text-rotation="90">Coq 8.7.1</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">G1</td><td style="background-color:#C0FFC0">0.00</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#FF0000" colspan="2">G2</td><td style="background-color:#FF8000">0.00</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#FF0000" colspan="2">split_goal_right</td><td style="background-color:#E0E0E0"></td><td style="background-color:#E0E0E0"></td></tr>
<tr><td rowspan="2" style="width:1ex"></td><td style="background-color:#FF0000" colspan="1">G2.0</td><td style="background-color:#FF8000">0.00</td><td style="background-color:#FF8000">0.29</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">G2.1</td><td style="background-color:#C0FFC0">0.00</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">G3</td><td style="background-color:#C0FFC0">0.00</td><td style="background-color:#E0E0E0">---</td></tr>
929 930 931
</table>
\end{rawhtml}
\end{htmlonly}
932
\caption{HTML table produced for the HelloProof example}
MARCHE Claude's avatar
MARCHE Claude committed
933 934
\label{fig:html}
\end{figure}
935

936
The style `table' outputs the contents of the session as a table,
937
similar to the LaTeX output above. Figure~\ref{fig:html} is the HTML
938
table produced for the `HelloProof' example, as typically shown in a
939 940 941 942 943
Web browser. The gray cells filled with \texttt{---} just mean that
the prover was not run on the corresponding goal. Green background
means the result was ``Valid'', other cases are in orange
background. The red background for a goal means that the goal was not
proved.
944

945 946 947
The style `simpletree' displays the contents of the session under the
form of tree, similar to the tree view in the IDE. It uses only basic
HTML tags such as \verb|<ul>| and \verb|<li>|.
948 949 950

Specific options for this command are as follows.
\begin{description}
951
\item[\texttt{-{}-style \textsl{<style>}}] sets the style to use, among
952
  \texttt{simpletree} and \texttt{table}; defaults to
MARCHE Claude's avatar
MARCHE Claude committed
953 954
  \texttt{table}.

955 956 957
\item[\texttt{-o \textsl{<dir>}}] sets the directory where to output
  the produced files (`\texttt{-}' for stdout). The default is to output
  in the same directory as the session itself.
958

MARCHE Claude's avatar
MARCHE Claude committed
959
\item[\texttt{-{}-context}] adds context around the generated code in
960
  order to allow direct visualization (header, css, ...). It also adds
MARCHE Claude's avatar
MARCHE Claude committed
961
  in the output directory all the needed external files. It can't be set with
962 963
  stdout output.

964
\item[\texttt{-{}-add\_pp \textsl{<suffix>} \textsl{<cmd>} \textsl{<out\_suffix>}}] sets a specific
965
  pretty-printer for files with the given suffix. Produced files use
966
  \texttt{\textsl{<out\_suffix>}} as suffix. \texttt{\textsl{<cmd>}} must contain
967 968
  `\texttt{\%i}' which will be replaced by the input file and
  `\texttt{\%o}' which will be replaced by the output file.
969

970
\item[\texttt{-{}-coqdoc}] uses the \verb|coqdoc| command to display Coq proof
MARCHE Claude's avatar
MARCHE Claude committed
971 972
  scripts. This is equivalent to \texttt{-{}-add\_pp .v "coqdoc
    -{}-no-index -{}-html -o \%o \%i" .html}
973 974

\end{description}
MARCHE Claude's avatar
MARCHE Claude committed
975

MARCHE Claude's avatar
doc  
MARCHE Claude committed
976

977
\section{The \texttt{doc} Command}
978 979
\label{sec:why3doc}

Guillaume Melquiond's avatar
Guillaume Melquiond committed
980 981
This tool can produce HTML pages from \why source code.
\why code for theories or modules is output in
MARCHE Claude's avatar
MARCHE Claude committed
982 983 984 985 986 987
preformatted HTML code. Comments are interpreted in three different ways.
\begin{itemize}
\item Comments starting with at least three stars are completed
  ignored.
\item Comments starting with two stars are interpreted as textual
  documentation. Special constructs are interpreted as described
Guillaume Melquiond's avatar
Guillaume Melquiond committed
988 989
  below. When the previous line is not empty, the comment is indented to
  the right, so as to be displayed as a description of that line.
MARCHE Claude's avatar
MARCHE Claude committed
990 991 992 993 994 995 996 997 998 999
\item Comments starting with one star only are interpreted as code
  comments, and are typeset as the code
\end{itemize}

Additionally, all the \why identifiers are typeset with links so that
one can navigate through the HTML documentation, going from some
identifier use to its definition.

\paragraph{Options}

1000 1001
\begin{description}
\item[\texttt{-o \textsl{<dir>}}] defines the directory where to
1002
  output the HTML files.
1003
\item[\texttt{-{}-output \textsl{<dir>}}] is the same as \verb|-o|.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1004 1005
\item[\texttt{-{}-index}] generates an index file \texttt{index.html}.
  This is the default behavior if more than one file
1006
  is passed on the command line.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1007
\item[\texttt{-{}-no-index}] prevents the generation of an index file.
1008
\item[\texttt{-{}-title \textsl{<title>}}] sets title of the
1009
  index page.
1010
\item[\texttt{-{}-stdlib-url \textsl{<url>}}] sets a URL for files
1011
  found in load path, so that links to definitions can be added.
1012
\end{description}
1013

MARCHE Claude's avatar
MARCHE Claude committed
1014 1015 1016 1017 1018
\paragraph{Typesetting textual comments}

Some constructs are interpreted:
\begin{itemize}
\item \texttt{\{\textsl{c text}\}} interprets character \textsl{c} as
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1019 1020 1021 1022 1023
  some typesetting command:
  \begin{description}
  \item[1-6] a heading of level 1 to 6 respectively
  \item[h] raw HTML
  \end{description}
1024
\item \texttt{`\textsl{code}`} is a code escape: the text
MARCHE Claude's avatar
MARCHE Claude committed
1025 1026 1027
  \textsl{code} is typeset as \why code.
\end{itemize}

Guillaume Melquiond's avatar
Guillaume Melquiond committed
1028 1029 1030
A CSS file \verb|style.css| suitable for rendering is generated in the
same directory as output files. This CSS style can be modified manually,
since regenerating the HTML documentation will not overwrite an existing
MARCHE Claude's avatar
MARCHE Claude committed
1031
\verb|style.css| file.
1032

1033 1034 1035 1036
\section{The \texttt{execute} Command}
\label{sec:why3execute}

\why can symbolically execute programs written using the \whyml language
1037
(extension \texttt{.mlw}). See also Section~\ref{sec:execute}.
1038 1039 1040 1041 1042 1043
\index{execute@\texttt{execute}}

\section{The \texttt{extract} Command}
\label{sec:why3extract}

\why can extract programs written using the \whyml language
1044
(extension \texttt{.mlw}) to OCaml. See also Section~\ref{sec:extract}.
Guillaume Melquiond's avatar