Commit e76223ed authored by MARCHE Claude's avatar MARCHE Claude

doc: fix section 4.2.2 (uninstalled provers)

parent acb7937d
......@@ -55,7 +55,7 @@ liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev
It is also installable from sources, available from the site
\url{http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html}
\item For \texttt{why3 bench}, the OCaml bindings of the sqlite3 library
\item \todo{remove, obsolete} For \texttt{why3 bench}, the OCaml bindings of the sqlite3 library
are needed.
For Debian-based Linux distributions, you can install the package
\begin{verbatim}
......@@ -142,12 +142,12 @@ file (see Sec.~\ref{sec:why3config}) accordingly.
\subsection{Multiple Versions of the Same Prover}
\why is able to use several versions of the same
prover, \eg it can use both CVC3 2.2 and CVC3 2.4.1 at the same time.
prover, \eg it can use both CVC4 1.4 and CVC4 1.5 at the same time.
The automatic detection of provers looks for typical names for their
executable command, \eg \texttt{cvc3} for CVC3. However, if you
install several version of the same prover it is likely that you would
use specialized executable names, such as \texttt{cvc3-2.2} or
\texttt{cvc3-2.4.1}. If needed, option \verb|--add-prover| can be
executable command, \eg \texttt{cvc4} for CVC3. However, if you
install several versions of the same prover it is likely that you would
use specialized executable names, such as \texttt{cvc4-1.4} or
\texttt{cvc4-1.5}. If needed, option \verb|--add-prover| can be
added to the \texttt{config} command to specify names of prover executables, \eg
\index{add-prover@\verb+--add-prover+}
\begin{verbatim}
......@@ -165,35 +165,31 @@ Appendix~\ref{sec:proverdetecttiondata} for details.
If you happen to upgrade a prover, \eg installing CVC4 1.5 in place
of CVC4 1.4, then the proof sessions formerly recorded will still
refer to the old version of the prover. If you open one such a session
with the GUI, and replay the proofs, you will be asked to choose
with the GUI, and replay the proofs, a popup window will show up for asking you to choose
between three options:
\begin{itemize}
\item Keep the former proofs as they are. They will be marked as
``archived''.
\item Upgrade the former proofs to an installed prover (typically a
\item Keep the former proof attempts as they are, with the old prover version. They will not be replayed.
\item Upgrade the former proof attempts to an installed prover (typically a
upgraded version). The corresponding proof attempts will become
attached to this new prover, and marked as obsolete,
to make their replay mandatory.
to make their replay mandatory. Note that you need to invoke again the replay command to replay those proof attempts.
\item Copy the former proofs to an installed prover. This is a
combination of the actions above: each proof attempt is duplicated,
one with the former prover marked as archived, and one for the new
prover marked as obsolete.
one with the former prover version, and one for the new
version marked as obsolete.
\end{itemize}
Notice that if the prover under consideration is an interactive one, then
the copy option will duplicate also the edited proof scripts, whereas
the upgrade-without-archive option will just reuse the former proof scripts.
the upgrade-without-copy option will just reuse the former proof scripts.
Your choice between the three options above will be recorded, one for
each prover, in the \why configuration file. Within the GUI, you can
discard these choices via the \textsf{Preferences} dialog.
discard these choices via the \textsf{Preferences} dialog: just click on one choice to remove it.
Outside the GUI, the prover upgrades are handled as follows. The
\texttt{replay} command will just ignore proof attempts marked as
archived\index{archived}.
Conversely, a non-archived proof attempt with a non-existent
prover will be reported as a replay failure. The
\texttt{session} command performs move or copy operations on
\texttt{replay} command will take into account any prover upgrade policy stored in the configuration.
The \texttt{session} command performs move or copy operations on
proof attempts in a fine-grained way, using filters, as detailed in
Section~\ref{sec:why3session}.
......
......@@ -293,7 +293,7 @@ Additionally, a proof attempt can have the following attributes:
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[archived]\index{archived!proof attempt} The proof attempt is not useful
\item[archived]\index{archived!proof attempt} \todo{obsolete} The proof attempt is not useful
anymore; it is kept for history; no \why tools will select it by
default. Section \ref{sec:uninstalledprovers} shows an example
of this usage.
......@@ -748,7 +748,7 @@ The available subcommands are as follows:
\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{copy-archive}] same as copy but also archives the
\item[\texttt{copy-archive}] \todo{obsolete} same as copy but also archives the
original proofs\index{archived!proof attempt}.
\item[\texttt{rm}] removes some of the proofs, selected by a filter.
\end{description}
......@@ -801,7 +801,7 @@ 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| and if it is archived we mark it with an \verb|A|.
\verb|O| and if it is \todo{obsolete} archived we mark it with an \verb|A|.
For example, here are the session tree produced on the ``hello
proof'' example of Section~\ref{chap:starting}.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment