Commit b9070bdb authored by MARCHE Claude's avatar MARCHE Claude

Doc: proposition for a policy in case of prover upgrade

parent e0d3cca6
\chapter{Compilation, Installation}
\label{sec:install}
In short, installation proceeds as follows.
\begin{flushleft}\ttfamily
./configure
make
make install \mbox{\rmfamily (as super-user)}
\end{flushleft}
\section{Installation Instructions from Source Distribution}
After unpacking the distribution, go to the newly created directory
\texttt{why3-\whyversion}. Compilation must start with a
configuration phase which is run as
\begin{verbatim}
./configure
\end{verbatim}
This analyzes your current configuration and checks if requirements hold.
Compilation requires:
\begin{itemize}
\item The Objective Caml compiler, version \todo{3.10} or higher. It is
available as a binary package for most Unix distributions. For
Debian-based Linux distributions, you can install the packages
\begin{verbatim}
ocaml ocaml-native-compilers
\end{verbatim}
It is also installable from sources, downloadable from the site
\url{http://caml.inria.fr/ocaml/}
\end{itemize}
\noindent
For some of the \why tools, additional OCaml libraries are needed:
\begin{itemize}
\item For the graphical interface: the Lablgtk2 library for OCaml
bindings of the gtk2 graphical library. For Debian-based Linux
distributions, you can install the packages
\begin{verbatim}
liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev
\end{verbatim}
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{why3bench}: The OCaml bindings of the sqlite3 library.
For Debian-based Linux distributions, you can install the package
\begin{verbatim}
libsqlite3-ocaml-dev
\end{verbatim}
It is also installable from sources, available from the site
\url{http://ocaml.info/home/ocaml_sources.html#ocaml-sqlite3}
\end{itemize}
When configuration is finished, you can compile \why.
\begin{verbatim}
make
\end{verbatim}
Installation is performed (as super-user if needed) using
\begin{verbatim}
make install
\end{verbatim}
Installation can be tested as follows:
\begin{enumerate}
\item install some external provers (see~Section\ref{provers} below)
\item run \verb|why3config --detect|
\item run some examples from the distribution, \emph{e.g.} you should
obtain the following:
\begin{verbatim}
$ cd examples
$ why3replayer scottish-private-club
Info: found directory 'scottish-private-club' for the project
Opening session... done
Progress: 4/4
1/1
Everything OK.
$ why3replayer programs/same_fringe
Info: found directory 'programs/same_fringe' for the project
Opening session... done
Progress: 12/12
3/3
Everything OK.
\end{verbatim}
\end{enumerate}
\section{Local use, without installation}
It is not mandatory to install \why into system directories.
\why can be configured and compiled for local use as follows:
\begin{verbatim}
./configure --enable-local
make
\end{verbatim}
The \why executables are then available in the subdirectory
\texttt{bin/}. This directory can be added in your \texttt{PATH}.
\section{Installation of the \why Library}
\label{sec:installlib}
By default, the \why library is not installed. It can be installed using
\begin{flushleft}\ttfamily
make byte opt \\
make install\_lib \mbox{\rmfamily (as super-user)}
\end{flushleft}
\section{Installation of External Provers}
\label{provers}
\why can use a wide range of external theorem provers. These need to
be installed separately, and then \why needs to be configured to use
them. There is no need to install these provers before compiling and
installing Why.
For installation of external provers, please refer to the specific
section about provers on the Web page \url{http://why3.lri.fr/}.
For configuring \why to use the provers, follow instructions given in
Section~\ref{sec:why3config}.
\section{Multiple Versions of the Same Prover}
Since version 0.72, \why is able to several versions of the same
prover, e.g. it can use both CVC3 2.2 and CVC3 2.4.1 at the same time.
The automatic detection of provers looks for typical names for their
executable command, e.g. \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}. To allow the \why detection process to recognize
these, you can use the option \verb|--add-prover| to
\texttt{why3config}, e.g.
\begin{verbatim}
why3config --detect --add-prover cvc3-2.4:/usr/local/bin/cvc3-2.4.1
\end{verbatim}
the first argument (here \verb|cvc3-2.4|) must be one of the class of
provers known in the file \verb|provers-detection-data.conf| typically
located in \verb|/usr/local/share/why3| after installation.
\section{Session Update after Prover Upgrade}
If you happen to upgrade a prover, e.g. installing CVC3 2.4.1 in place
of CVC3 2.2, then the proof sessions formerly recorded will still
refer to the old version of the proer. If you open one such a session
with the GUI, and replay the proofs, you will be asked to choose
between 3 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
upgraded version). The corresponding proof attempts will become
attached to this new prover, and marked as obsolete, to make their
replay mandatory.
\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.
\end{itemize}
Notice that 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.
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.
Outside the GUI, the prover upgrades are handled as follows. First,
the \texttt{why3replayer} tool will just ignore proof attempts where
the recorded prover does not appear to be installed. Second, the tool
\texttt{why3session} allows you to perform move or copy operations on
proof attempts in a fine-grain way, using filters, as detailed in Section~\ref{sec:why3session}.
\todo{Que faire de ce qui suit ?}
If you just want to update one session with updated provers you can
use \verb|--to-known-prover| instead of the option \verb|--to-prover|.
\begin{verbatim}
why3session copy --to-known-prover
\end{verbatim}
For each proof attempt associated to an unknown prover (a prover not in
\verb|.why3.conf|) and not archived, it will try to find a known prover
with the same name. If it finds one, the proof attempt is copied to this
prover and the old proof is set to archived. The corresponding edited
files, if any, are copied and regenerated for the new prover. An archived
proof is not replayed by why3replayer.
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End:
This diff is collapsed.
......@@ -220,16 +220,20 @@ are the following.
% \input{glossary.tex}
\input{install.tex}
\input{manpages.tex}
\input{syntaxref.tex}
\input{library.tex}
\input{manpages.tex}
\input{realizations.tex}
\input{coq_tactic.tex}
\input{technical.tex}
% \chapter{Complete API documentation} *)
% \label{chap:apidoc} *)
......
\chapter{Technical Informations}
\section{Structure of Session Files}
The proof session state is stored in an XML file named
\texttt{\textsl{<dir>}/why3session.xml}, where \texttt{\textsl{<dir>}}
is the directory of the project.
The XML file follows the DTD given in \texttt{share/why3session.dtd} and reproduced below.
\verbatiminput{../share/why3session.dtd}
\section{The \texttt{why3.conf} configuration file}
\label{sec:whyconffile}
\index{why3.conf@\texttt{why3.conf}}\index{configuration file}
\todo{THIS SECTION IS OUTDATED}
\begin{figure}[t]
\begin{verbatim}
[main ]
loadpath = "/usr/local/share/why3/theories"
magic = 2
memlimit = 0
running_provers_max = 2
timelimit = 10
[ide ]
default_editor = "emacs"
task_height = 384
tree_width = 438
verbose = 0
window_height = 779
window_width = 638
[prover coq]
command = "coqc %f"
driver = "/usr/local/share/why3/drivers/coq.drv"
editor = "coqide"
name = "Coq"
version = "8.2pl2"
[prover alt-ergo]
command = "why3-cpulimit %t %m alt-ergo %f"
driver = "/usr/local/share/why3/drivers/alt_ergo.drv"
editor = ""
name = "Alt-Ergo"
version = "0.91"
\end{verbatim}
\caption{Sample why3.conf file}
\label{fig:why3conf}
\end{figure}
One can use a custom configuration file. \texttt{why3config}
and other \texttt{why3} tools use priorities for which
user's configuration file to consider:
\begin{itemize}
\item the file specified by the \texttt{-C} or \texttt{-{}-config} options,
\item the file specified by the environment variable
\texttt{WHY3CONFIG} if set.
\item the file \texttt{\$HOME/.why3.conf}
(\texttt{\$USERPROFILE/.why3.conf} under Windows) or, in the case of
local installation, \texttt{why3.conf} in Why3 sources top directory.
\end{itemize}
If none of these files exists, a built-in default configuration is used.
The configuration file is a human-readable text file, which consists
of association pairs arranged in sections. Figure~\ref{fig:why3conf}
shows an example of configuration file.
A section begins with a header inside square brackets and ends at the
beginning of the next section. The header of a
section can be only one identifier, \texttt{main} and \texttt{ide} in
the example, or it can be composed by a family name and one family
argument, \texttt{prover} is one family name, \texttt{coq} and
\texttt{alt-ergo} are the family argument.
Inside a section, one key can be associated with an integer (\eg{} -555),
a boolean (true, false) or a string (\eg{} "emacs"). One key can appear
only once except if its a multi-value key. The order of apparition of
the keys inside a section matter only for the multi-value key.
\section{Drivers of External Provers}
\label{sec:drivers}
The drivers of external provers are readable files, in directory
\texttt{drivers}. Experimented users can modify them to change the way
the external provers are called, in particular which transformations
are applied to goals.
[TO BE COMPLETED LATER]
\section{Transformations}
\label{sec:transformations}
Here is a quick documentation of provided transformations. We give
first the non-splitting ones, \eg{} those which produce one goal as
result, and others which produces any number of goals.
Notice that the set of available transformations in your own
installation is given by
\begin{verbatim}
why3 --list-transforms
\end{verbatim}
\subsection{Non-splitting transformations}
\begin{description}
\item[eliminate\_algebraic] Replaces algebraic data types by first-order
definitions~\cite{paskevich09rr}
\item[eliminate\_builtin] Suppress definitions of symbols which are
declared as builtin in the driver, i.e. with a ``syntax'' rule.
\item[eliminate\_definition\_func]
Replaces all function definitions with axioms.
\item[eliminate\_definition\_pred]
Replaces all predicate definitions with axioms.
\item[eliminate\_definition]
Apply both transformations above.
\item[eliminate\_mutual\_recursion]
Replaces mutually recursive definitions with axioms.
\item[eliminate\_recursion]
Replaces all recursive definitions with axioms.
\item[eliminate\_if\_term] replaces terms of the form \texttt{if
formula then t2 else t3} by lifting them at the level of formulas.
This may introduce \texttt{if then else } in formulas.
\item[eliminate\_if\_fmla] replaces formulas of the form \texttt{if f1 then f2
else f3} by an equivalent formula using implications and other
connectives.
\item[eliminate\_if]
Apply both transformations above.
\item[eliminate\_inductive] replaces inductive predicates by
(incomplete) axiomatic definitions, i.e. construction axioms and
an inversion axiom.
\item[eliminate\_let\_fmla]
Eliminates \texttt{let} by substitution, at the predicate level.
\item[eliminate\_let\_term]
Eliminates \texttt{let} by substitution, at the term level.
\item[eliminate\_let]
Apply both transformations above.
% \item[encoding\_decorate\_mono]
% \item[encoding\_enumeration]
\item[encoding\_smt]
Encode polymorphic types into monomorphic type~\cite{conchon08smt}.
\item[encoding\_tptp]
Encode theories into unsorted logic. %~\cite{cruanes10}.
% \item[filter\_trigger] *)
% \item[filter\_trigger\_builtin] *)
% \item[filter\_trigger\_no\_predicate] *)
% \item[hypothesis\_selection] *)
% Filter hypothesis of goals~\cite{couchot07ftp,cruanes10}. *)
\item[inline\_all]
expands all non-recursive definitions.
\item[inline\_goal] Expands all outermost symbols of the goal that
have a non-recursive definition.
\item[inline\_trivial]
removes definitions of the form
\begin{verbatim}
function f x_1 .. x_n = (g e_1 .. e_k)
predicate p x_1 .. x_n = (q e_1 .. e_k)
\end{verbatim}
when each $e_i$ is either a ground term or one of the $x_j$, and
each $x_1$ .. $x_n$ occur at most once in the $e_i$
\item[introduce\_premises] moves antecedents of implications and
universal quantifications of the goal into the premises of the task.
% \item[remove\_triggers] *)
% removes the triggers in all quantifications. *)
\item[simplify\_array] Automatically rewrites the task using the lemma
\verb|Select_eq| of theory \verb|array.Array|.
\item[simplify\_formula] reduces trivial equalities $t=t$ to true and
then simplifies propositional structure: removes true, false, ``f
and f'' to ``f'', etc.
\item[simplify\_recursive\_definition] reduces mutually recursive
definitions if they are not really mutually recursive, e.g.:
\begin{verbatim}
function f : ... = .... g ...
with g : .. = e
\end{verbatim}
becomes
\begin{verbatim}
function g : .. = e
function f : ... = .... g ...
\end{verbatim}
if f does not occur in e
\item[simplify\_trivial\_quantification]
simplifies quantifications of the form
\begin{verbatim}
forall x, x=t -> P(x)
\end{verbatim}
or
\begin{verbatim}
forall x, t=x -> P(x)
\end{verbatim}
when x does not occur in t
into
\begin{verbatim}
P(t)
\end{verbatim}
More generally, it applies this simplification whenever x=t appear
in a negative position.
\item[simplify\_trivial\_quantification\_in\_goal]
same as above but applies only in the goal.
\item[split\_premise]
splits conjunctive premises.
\end{description}
\subsection{Splitting transformations}
\begin{description}
\item[full\_split\_all]
composition of \texttt{split\_premise} and \texttt{full\_split\_goal}.
\item[full\_split\_goal] puts the goal in a conjunctive form,
returns the corresponding set of subgoals. The number of subgoals
generated may be exponential in the size of the initial goal.
\item[simplify\_formula\_and\_task] same as \texttt{simplify\_formula}
but also removes the goal if it is equivalent to true.
\item[split\_all]
composition of \texttt{split\_premise} and \texttt{split\_goal}.
\item[split\_goal] if the goal is a conjunction of goals, returns the
corresponding set of subgoals. The number of subgoals generated is linear in
the size of the initial goal.
\item[split\_intro]
when a goal is an implication, moves the antecedents into the premises.
\end{description}
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End:
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