Skip to content
Snippets Groups Projects
Select Git revision
  • 9585835c1114645f8a26e2fe5f69d90d0f6aa966
  • master default protected
  • rust
  • extract-fix-master
  • extract-fix
  • extract-fix-1.0.0
6 results

manpages.tex

Blame
  • manpages.tex 43.44 KiB
    \chapter{Reference Manuals for the \why Tools}
    \label{chap:manpages}
    %HEVEA\cutname{manpages.html}
    
    This chapter details the usage of each of the command-line tools
    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}
    why3 [general options...] <command> [specific options...]
    \end{verbatim}
    
    The following commands are available:
    \begin{description}
    \item[\texttt{config}] manages the user's configuration,
      including the detection of installed provers.
    \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.
    \item[\texttt{prove}] reads \whyml input files and calls
      provers, on the command-line.
    \item[\texttt{realize}] generates interactive proof skeletons for
      \why input files.
    \item[\texttt{replay}] replays the proofs stored in a session,
      for regression test purposes.
    \item[\texttt{session}] dumps various informations from a proof
      session, and possibly modifies the session.
    \item[\texttt{wc}] gives some token statistics about \whyml
      source files.
    \end{description}
    
    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.
    \begin{description}
    \item[\texttt{-L \textsl{<dir>}}]
      adds \texttt{\textsl{<dir>}} in the load path, to search for theories.
      \index{L@\verb+-L+|see{\texttt{-{}-library}}}
    \item[\texttt{-{}-library \textsl{<dir>}}]
      is the same as \verb|-L|.
      \index{library@\verb+--library+}
    \item[\texttt{-C \textsl{<file>}}]
      reads the configuration from the given file.
      \index{C@\verb+-C+|see{\texttt{-{}-config}}}
    \item[\texttt{-{}-config \textsl{<file>}}]
      is the same as \verb|-C|.
      \index{config@\verb+--config+}
    \item[\texttt{-{}-extra-config \textsl{<file>}}]
      reads additional configuration from the given file.
      \index{extra-config@\verb+--extra-config+}
    \item[\texttt{-{}-list-debug-flags}]
        list known debug flags.
      \index{list-debug-flags@\verb+--list-debug-flags+}
    \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+}
    \item[\texttt{-{}-debug-all}]
      sets all debug flags (except flags which change the behavior).
      \index{debug-all@\verb+--debug-all+}
    \item[\texttt{-{}-debug \textsl{<flag>}}]
      sets a specific debug flag.
      \index{debug@\verb+--debug+}
    \item[\texttt{-{}-help}]
      displays the usage and the exact list of options for the given tool.
      \index{help@\verb+--help+}
    \end{description}
    
    \section{The \texttt{config} Command}
    \label{sec:why3config}
    
    \why must be configured to access external provers. Typically, this is done
    by running the \texttt{config} command.
    This must be done each time a new prover is installed.%
    \index{config@\texttt{config}}%
    \index{configuration file}
    
    The provers that \why attempts to detect are described in
    the readable configuration file \texttt{provers-detection-data.conf}
    of the \why data directory (\eg
    \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
    tracking system.)
    
    The result of provers detection is stored in the user's
    configuration file (\verb+~/.why3.conf+ or, in the case of local
    installation, \verb+why3.conf+ in \why sources top directory). This file
    is also human-readable, and advanced users may modify it in order to
    experiment with different ways of calling provers, \eg different
    versions of the same prover, or with different options.
    
    The \texttt{config} command also detects the plugins installed in the \why
    plugins directory (\eg \texttt{/usr/local/lib/why3/plugins}). A
    plugin must register itself as a parser, a transformation or a
    printer, as explained in the corresponding section.
    \index{plugin}
    
    If the user's configuration file is already present,
    \texttt{config} will only reset unset variables to default value,
    but will not try to detect provers.
    The option \verb|--detect-provers| should be used to force
    \why to detect again the available
    provers and to replace them in the configuration file. The option
    \verb|--detect-plugins| will do the same for plugins.
    \index{detect-provers@\verb+--detect-provers+}
    \index{detect-plugins@\verb+--detect-plugins+}
    
    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
    \verb|/home/me/bin/alt-ergo-trunk| can be added as follows:
    \begin{verbatim}
    why3 config --add-prover alt-ergo /home/me/bin/alt-ergo-trunk
    \end{verbatim}
    As the first argument, one should put a prover
    identification string. The list of known prover identifiers
    can be obtained by the option \verb|--list-prover-ids|.
    \index{add-prover@\verb+--add-prover+}
    \index{list-prover-ids@\verb+--list-prover-ids+}
    
    \section{The \texttt{prove} Command}
    \label{sec:why3ref}
    
    \why is primarily used to call provers on goals contained in an
    input file. By default, such a file must be written in \whyml language
    (extension \texttt{.mlw}).
    However, a dynamically loaded
    plugin can register a parser for some other format of logical problems,
    \eg TPTP or SMT-LIB.
    \index{prove@\texttt{prove}}
    
    The \texttt{prove} command executes the following steps:
    \begin{enumerate}
    \item Parse the command line and report errors if needed.
    \item Read the configuration file using the priority defined in
      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
      to obtain a set of \why theories for each file. It uses
      the filename extension or the \verb|--format| option to choose
      among the available parsers. \verb|why3 --list-formats| lists
      the registered parsers.
      \index{list-formats@\verb+--list-formats+}
      \whyml modules are turned into
      theories containing verification conditions as goals.
    \item Extract the selected goals inside each of the selected theories
      into tasks. The goals and theories are selected using options
      \verb|-G/--goal| and \verb|-T/--theory|. Option
      \verb|-T/--theory| applies to the previous file appearing on the
      command line. Option \verb|-G/--goal| applies to the previous theory
      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.
      \index{G@\verb+-G+|see{\texttt{-{}-goal}}}
      \index{goal@\verb+--goal+}
      \index{T@\verb+-T+|see{\texttt{-{}-theory}}}
      \index{theory@\verb+--theory+}
    \item Apply the transformations requested
      with \verb|-a/--apply-transform| in their order of appearance on the
      command line. \verb|why3 --list-transforms| lists the known
      transformations; plugins can add more of them.
      \index{a@\verb+-a+|see{\texttt{-{}-apply-transform}}}
      \index{apply-transform@\verb+--apply-transform+}
      \index{list-transforms@\verb+--list-transforms+}
    \item Apply the driver selected with the \verb|-D/--driver| option,
      or the driver of the prover selected with the \verb|-P/--prover|
      option. \verb|why3 --list-provers| lists the known provers, \ie the ones
      that appear in the configuration file.
      \index{D@\verb+-D+|see{\texttt{-{}-driver}}}
      \index{driver@\verb+--driver+}
      \index{P@\verb+-P+|see{\texttt{-{}-prover}}}
      \index{prover@\verb+--prover+}
      \index{list-provers@\verb+--list-provers+}
    \item If option \verb|-P/--prover| is given, call the selected prover
      on each generated task and print the results. If option
      \verb|-D/--driver| is given, print each generated task using
      the format specified in the selected driver.
    \end{enumerate}
    
    %\texttt{why3} calls the provers sequentially, use \texttt{why3bench} if *)
    %you want to call the provers concurrently.  *)
    
    \subsection{Prover Results}
    The provers can give the following output:
    \begin{description}
    \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.
    \end{description}
    % \why can also be *)
    % used to provide other informations : *)
    % \begin{itemize} *)
    % \item \texttt{print-namespace} print the namespace of the selected *)
    %   theories *)
    % \item TO BE COMPLETED *)
    % \end{itemize} *)
    
    %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.
    
    \subsection{Additional Options}
    \label{sec:proveoptions}
    
    \begin{description}
    %\item[\texttt{-{}-get-ce}] activates the generation of a potential
    %counter-example when a proof does not succeed (experimental).
    \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}
    
    \section{The \texttt{ide} Command}
    \label{sec:ideref}
    
    The basic usage of the GUI is described by the tutorial of
    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
    created. The other arguments should be existing files that are going
    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.
    
    We describe the actions of the various menus and buttons of the
    interface.
    \index{ide@\texttt{ide}}
    
    \subsection{Session}
    \label{sec:idref:session}
    \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
    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
    result of the prover is the same as when you run the \texttt{prove} command. It
    contains the time taken and the state of the proof:
    
    \begin{description}
    \item[Valid] The task is valid according to the prover. The
      goal is considered proved.
    \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
      prover, or the prover answer was not understood.
    \end{description}
    
    Additionally, a proof attempt can have the following attributes:
    
    \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
      earlier version of that task. You need to replay the proof
      attempt, \ie run the prover with the current task of the proof
      attempt, in order to update the answer of the prover and remove this
      attribute.
    \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.
    \end{description}
    
    Generally, proof attempts are marked obsolete just after
    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
    rebuilds the goals to prove by using the information provided in the
    session. If you modify the original file (\texttt{.mlw}) or if the
    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.
    
    \subsection{Context Menu}
    
    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.
    
    \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
    \item[Edit] starts an editor on the selected task.
    \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.
    \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.
    \end{description}
    
    \subsection{Global Menus}
    
    \begin{description}
    \item[Menu \textsf{File}]\emptyitem
    \begin{description}
    \item[Add File to session] adds a file in the current proof session.
    %\item[Detect provers] runs provers auto-detection
    \item[Preferences] opens a window for modifying preferred
      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.
    \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.
    \item[Quit] exits the GUI.
    \end{description}
    
    \item[Menu \textsf{Tools}]\emptyitem
    \begin{description}
    \item[Strategies] section provides a set of actions that are
      performed on the selected goal(s):
      \begin{description}
      \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.
      \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.
    
    \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.
    
    \item[Transformations] gives access to all the known transformations.
    
    \item[Edit] starts an editor on the selected task.
    
      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.
    
    \item[Replay valid obsolete proofs] replays all the obsolete proofs below the current node whose former state was Valid.
    
    \item[Replay all obsolete proofs] replays all the obsolete proofs below the current node.
    
    \item[Clean] removes any unsuccessful proof attempt for which there is
      another successful proof attempt for the same goal
    
    \item[Remove] removes a proof attempt or a transformation.
    
    \item[Mark obsolete] marks all the proof as
      obsolete.  This allows to replay every proof.
    
    \item[Interrupt] cancels all the proof attempts currently scheduled or running.
    
    \item[Bisect] performs a reduction of the context for the the current selected proof attempt, which must be a Valid one.
    
    \item[Focus] focus the tree session view to the current node
    
    \item[Unfocus] undoes the Focus action
    
    \item[Copy] Marks of proof sub-tree for copy/past action
    
    \item[Paste] Paste the previously selected sub-tree under the current node
    
    \end{description}
    
    \item[Menu \textsf{View}]\emptyitem
    \begin{description}
    \item[Enlarge font] selects a large font
    \item[Reduce font] selects a smaller font
    \item[Collapse proved goals] closes all the rows of the tree view
      that are proved.
    \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
    \end{description}
    
    
    \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}
    
    \end{description}
    
    \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.
    
    \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}
    
    \subsection{Preferences Dialog}
    
    The preferences dialog allows you to customize various settings. They
    are grouped together under several tabs.
    
    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.
    
    
    \begin{description}
    \item[\textsf{General Settings} tab] allows one to set
      various general settings.
    \begin{itemize}
    \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}
    \item option to disallow source editing within the GUI
    \item the policy for saving sessions:
      \begin{itemize}
      \item always save on exit (default): the current state of the proof session is saving on exit
      \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
        want to save or not.
      \end{itemize}
    \end{itemize}
    
    \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.
    
    \item[\textsf{Editors} tab] allows one to customize the use
      of external editors for proof scripts.
    \begin{itemize}
    \item The default editor to use when the \textsf{Edit} button is
      pressed.
      \urldef{\urlprfgen}{\url}{http://proofgeneral.inf.ed.ac.uk/}
    \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
      dialog allows you to select the Emacs editor and its
     \ahref{\urlprfgen}{Proof General} mode instead%
     \begin{latexonly} (\urlprfgen)\end{latexonly}.
    \end{itemize}
    \item[\textsf{Provers} tab]
      allows to select which of the installed provers one wants to see
      in the context menu.
    \item[\textsf{Uninstalled Provers} tab] presents all the
      decision previously taken for missing provers, as described in
      Section~\ref{sec:uninstalledprovers}. You can remove any recorded
      decision by clicking on it.
    \end{description}
    
    \subsection{Displaying Counterexamples}
    
    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.
    
    More information how counterexamples in Why3 works can be found
    in~\cite{hauzar16sefm} and in~\cite{dailler18jlamp}.
    
    
    %
    % how to use counterexamples - explain labels, projections, the option --get-ce of why3prove and the setting in why3ide
    %
    % problem with set logic and counterexamples
    %
    % which provers
    %
    % where it is displayed
    %
    % how to interpret the display
    %
    % example
    
    
    
    \section{The \texttt{replay} Command}
    \label{sec:why3replayer}
    
    The \texttt{replay} command is meant to execute the proofs
    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
    all the examples.
    \index{replay@\texttt{replay}}
    
    The tool is invoked in a terminal or a script using
    \begin{flushleft}\ttfamily
      why3 replay \textsl{[options] <project directory>}
    \end{flushleft}
    The session file \texttt{why3session.xml} stored in the given
    directory is loaded and all the proofs it contains are rerun. Then,
    all the differences 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, whether the
    considered goal is proved or not. When all the proof
    are done, a summary of what is proved or not is displayed using a
    tree-shape pretty print, similar to the IDE tree view after doing
    ``Collapse proved goals''. In other words, when a goal, a theory, or a
    file is fully proved, the subtree is not shown.
    
    \paragraph{Obsolete proofs}
    
    When some proof attempts stored in the session file are
    obsolete\index{obsolete!proof attempt},
    the replay is run anyway, as with the replay button in the IDE. Then, the session
    file will be updated if both
    \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
    option \verb|--force| described below.
    
    \paragraph{Exit code and options}
    
    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).
    \item[\texttt{-{}-force}] enforces saving the session, if all proof
      attempts replayed correctly, even if some goals are not proved.
    \item[\texttt{-{}-obsolete-only}] replays the proofs only if the session
      contains obsolete proof attempts.
    \item[\texttt{-{}-smoke-detector \{none|top|deep\}}] tries to detect
      if the context is self-contradicting.
    \item[\texttt{-{}-prover \textsl{<prover>}}] restricts the replay to the
      selected provers only.
    \end{description}
    
    \paragraph{Smoke detector}
    
    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:
    \begin{description}
    \item[\texttt{none}] Do not run the smoke detector.
    \item[\texttt{top}] The negation of each proved goal is sent with the
      same timeout to the prover that proved the original goal.
    \begin{verbatim}
      Goal G : forall x:int. q x -> (p1 x \/ p2 x)
    \end{verbatim}
      becomes
    \begin{verbatim}
      Goal G : ~ (forall x:int. q x -> (p1 x \/ p2 x))
    \end{verbatim}
      In other words, if the smoke detector is triggered, it means that the context
      of the goal \texttt{G} is self-contradicting.
    \item[\texttt{deep}] This is the same technique as \texttt{top} but
      the negation is pushed under the universal quantification (without
      changing them) and under the implication. The previous example
      becomes
    \begin{verbatim}
      Goal G : forall x:int. q x /\ ~ (p1 x \/ p2 x)
    \end{verbatim}
      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
      example, this could occur in the WP of a program with an unfeasible
      path.
    \end{description}
    
    At the end of the replay, the name of the goals that triggered the
    smoke detector are printed:
    \begin{verbatim}
      goal 'G', prover 'Alt-Ergo 0.93.1': Smoke detected!!!
    \end{verbatim}
    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.
    
    
    
    \section{The \texttt{session} Command}
    \label{sec:why3session}
    
    The \texttt{session} command makes it possible to extract information from
    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}
    why3 session <subcommand> [options] <session directories>
    \end{verbatim}
    The available subcommands are as follows:
    \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.
    \item[\texttt{rm}] removes some of the proofs, selected by a filter.
    \end{description}
    
    The first three commands do not modify the sessions, whereas the last
    four modify them. Only the proof attempts recorded are modified. No
    prover is called on the modified or created proof attempts, and
    consequently the proof status is always marked as obsolete.
    
    \subsection{Command \texttt{info}}
    
    The command \texttt{why3 session info} reports various informations
    about the session, depending on the following specific options.
    \begin{description}
    \item[\texttt{-{}-provers}] prints the provers that appear inside
      the session, one by line.
    \item[\texttt{-{}-edited-files}] prints all the files that appear in
      the session as edited proofs.
    \item[\texttt{-{}-stats}] prints various proofs statistics, as
      detailed below.
    % OBSOLETE
    % \item[\texttt{-{}-tree}] prints the structure of the session as a
    %   tree in ASCII, as detailed below.
    \item[\texttt{-{}-print0}] separates the results of the options
      \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:
    \begin{verbatim}
    why3 session info --edited-files vstte12_bfs --print0 | xargs -0 coqwc
    \end{verbatim}
      or you can add all the edited files in your favorite repository
      with:
    \begin{verbatim}
    why3 session info --edited-files --print0 vstte12_bfs.mlw | \
        xargs -0 git add
    \end{verbatim}
    
    \end{description}
    
    
    % 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}
    % }
    
    \paragraph{Session Statistics}
    
    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
      proved by any prover, even after a transformation.
    \item Goals proved by only one prover: the goals for which there is only
      one successful proof. For each of these, the prover which was
      successful is printed. This also includes the sub-goals generated by
      transformations.
    \item Statistics per prover: for each of the prover used in the
      session, the number of proved goals is given. This also includes the
      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
      goals \emph{where the prover was successful}.
    \end{itemize}
    
    For example, here are the session statistics produced on the ``hello
    proof'' example of Section~\ref{chap:starting}.
    {\footnotesize
    \begin{verbatim}
    == Number of root goals ==
      total: 3  proved: 2
    
    == Number of sub goals ==
      total: 2  proved: 1
    
    == Goals not proved ==
      +-- file ../hello_proof.why
        +-- theory HelloProof
          +-- goal G2
            +-- transformation split_goal_right
              +-- goal G2.0
    
    == Goals proved by only one prover ==
      +-- file ../hello_proof.why
        +-- theory HelloProof
          +-- 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
    
    == Statistics per prover: number of proofs, time (minimum/maximum/average) in seconds ==
      Alt-Ergo 0.99.1     :   3   0.00   0.00   0.00
     \end{verbatim}
    }
    
    \subsection{Command \texttt{latex}}
    
    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.
    
    The specific options are
    \begin{description}
    \item[\texttt{-style \textsl{<n>}}] sets output style (1 or 2, default 1)
      Option \texttt{-style 2} produces an alternate version of LaTeX
      output, with a different layout of the tables.
    \item[\texttt{-o \textsl{<dir>}}] indicates where
      to produce LaTeX files (default: the session directory).
    \item[\texttt{-longtable}] uses the `longtable' environment instead of
      `tabular'.
    \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
      using its path in dot notation, \eg \verb|file.theory.goal|. The
      file produced is named accordingly,
      \eg \verb|file.theory.goal.tex|.  This option can be given several
      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.
    \end{description}
    
    \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.
    \begin{description}
    \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
      exists for the corresponding prover
    \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
    \end{description}
    
    \begin{figure}[t]
    \begin{center}
    \lstinputlisting[basicstyle={\ttfamily\small}]{./replayer_macros.tex}
    \end{center}
    \caption{Sample macros for the LaTeX command}
    \label{fig:custom-latex}
    \end{figure}
    
    \begin{figure}[t]
    \begin{center}
    %HEVEA\begin{toimage}
    \input{HelloProof.tex}
    %HEVEA\end{toimage}
    %HEVEA\imageflush
    \end{center}
    \caption{LaTeX table produced for the HelloProof example (style 1)}
    \label{fig:latex}
    \end{figure}
    
    \begin{figure}[t]
    \begin{center}
    %HEVEA\begin{toimage}
    \input{HelloProof-style2.tex}
    %HEVEA\end{toimage}
    %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.
    
    \subsection{Command \texttt{html}}
    
    This command produces a summary of the proof session in HTML syntax.
    There are two styles of output: `table' and `simpletree'. The default is
    `table'.
    
    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).
    
    \begin{figure}[t]
    %BEGIN LATEX
    \begin{center}
    \fbox{\includegraphics[width=0.9\textwidth]{hello_proof.png}}
    \end{center}
    %END LATEX
    \begin{htmlonly}
    \begin{rawhtml}
    <h1>Why3 Proof Results for Project "hello_proof"</h1>
    <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>
    </table>
    \end{rawhtml}
    \end{htmlonly}
    \caption{HTML table produced for the HelloProof example}
    \label{fig:html}
    \end{figure}
    
    The style `table' outputs the contents of the session as a table,
    similar to the LaTeX output above. Figure~\ref{fig:html} is the HTML
    table produced for the `HelloProof' example, as typically shown in a
    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.
    
    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>|.
    
    Specific options for this command are as follows.
    \begin{description}
    \item[\texttt{-{}-style \textsl{<style>}}] sets the style to use, among
      \texttt{simpletree} and \texttt{table}; defaults to
      \texttt{table}.
    
    \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.
    
    \item[\texttt{-{}-context}] adds context around the generated code in
      order to allow direct visualization (header, css, ...). It also adds
      in the output directory all the needed external files. It can't be set with
      stdout output.
    
    \item[\texttt{-{}-add\_pp \textsl{<suffix>} \textsl{<cmd>} \textsl{<out\_suffix>}}] sets a specific
      pretty-printer for files with the given suffix. Produced files use
      \texttt{\textsl{<out\_suffix>}} as suffix. \texttt{\textsl{<cmd>}} must contain
      `\texttt{\%i}' which will be replaced by the input file and
      `\texttt{\%o}' which will be replaced by the output file.
    
    \item[\texttt{-{}-coqdoc}] uses the \verb|coqdoc| command to display Coq proof
      scripts. This is equivalent to \texttt{-{}-add\_pp .v "coqdoc
        -{}-no-index -{}-html -o \%o \%i" .html}
    
    \end{description}
    
    
    \section{The \texttt{doc} Command}
    \label{sec:why3doc}
    
    This tool can produce HTML pages from \why source code.
    \why code for theories or modules is output in
    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
      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.
    \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}
    
    \begin{description}
    \item[\texttt{-o \textsl{<dir>}}] defines the directory where to
      output the HTML files.
    \item[\texttt{-{}-output \textsl{<dir>}}] is the same as \verb|-o|.
    \item[\texttt{-{}-index}] generates an index file \texttt{index.html}.
      This is the default behavior if more than one file
      is passed on the command line.
    \item[\texttt{-{}-no-index}] prevents the generation of an index file.
    \item[\texttt{-{}-title \textsl{<title>}}] sets title of the
      index page.
    \item[\texttt{-{}-stdlib-url \textsl{<url>}}] sets a URL for files
      found in load path, so that links to definitions can be added.
    \end{description}
    
    \paragraph{Typesetting textual comments}
    
    Some constructs are interpreted:
    \begin{itemize}
    \item \texttt{\{\textsl{c text}\}} interprets character \textsl{c} as
      some typesetting command:
      \begin{description}
      \item[1-6] a heading of level 1 to 6 respectively
      \item[h] raw HTML
      \end{description}
    \item \texttt{`\textsl{code}`} is a code escape: the text
      \textsl{code} is typeset as \why code.
    \end{itemize}
    
    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
    \verb|style.css| file.
    
    \section{The \texttt{execute} Command}
    \label{sec:why3execute}
    
    \why can symbolically execute programs written using the \whyml language
    (extension \texttt{.mlw}). See also Section~\ref{sec:execute}.
    \index{execute@\texttt{execute}}
    
    \section{The \texttt{extract} Command}
    \label{sec:why3extract}
    
    \why can extract programs written using the \whyml language
    (extension \texttt{.mlw}) to OCaml. See also Section~\ref{sec:extract}.
    \index{extract@\texttt{extract}}
    
    \section{The \texttt{realize} Command}
    \label{sec:why3realize}
    
    \why can produce skeleton files for proof assistants that, once filled,
    realize the given theories. See also Section~\ref{sec:realizations}.
    \index{realize@\texttt{realize}}
    
    \section{The \texttt{wc} Command}
    \label{sec:why3wc}
    
    \why can give some token statistics about \whyml source files.
    \index{wc@\texttt{wc}}
    
    %%% Local Variables:
    %%% mode: latex
    %%% TeX-PDF-mode: t
    %%% TeX-master: "manual"
    %%% End: