install.tex 8.05 KB
Newer Older
1 2 3

\chapter{Compilation, Installation}

6 7 8 9 10 11 12 13 14
\section{Installing Why3}

\subsection{Installation via \opam}

The simplest way to install Why3 is via \opam, the OCaml
package manager. It is as simple as
> opam install why3
Then jump to Section~\ref{provers} to install external provers.
16 17 18 19

\subsection{Installation Instructions from Source Distribution}

In short, installation from sources proceeds as follows.
21 22 23
  > ./configure\\
  > make\\
  > make install \mbox{\rmfamily (as super-user)}
24 25 26 27

After unpacking the distribution, go to the newly created directory
\texttt{why3-\whyversion}. Compilation must start with a
configuration phase which is run as
> ./configure
31 32 33 34
This analyzes your current configuration and checks if requirements hold.
Compilation requires:
\item The Objective Caml compiler. It is
36 37 38 39 40 41 42 43 44 45 46 47
  available as a binary package for most Unix distributions. For
  Debian-based Linux distributions, you can install the packages
ocaml ocaml-native-compilers
It is also installable from sources, downloadable from the site

For some of the \why tools, additional OCaml libraries are needed:
48 49
\item For the graphical interface, the Lablgtk2 library is needed.
  It provides OCaml
50 51 52 53 54 55 56 57
  bindings of the gtk2 graphical library. For Debian-based Linux
  distributions, you can install the packages
liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev
It is also installable from sources, available from the site

58 59 60 61 62 63 64 65
% \item 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}
% libsqlite3-ocaml-dev
% \end{verbatim}
% It is also installable from sources, available from the site
% \url{}
66 67


Guillaume Melquiond's avatar
Guillaume Melquiond committed
If you want to use the Coq realizations
70 71
(Section~\ref{sec:realizations}), then Coq has to be installed before
\why. Look at the summary printed at the end of the configuration
Guillaume Melquiond's avatar
Guillaume Melquiond committed
72 73 74
script to check if Coq has been detected properly. Similarly, in order to
use PVS (Section~\ref{sec:pvs}) or Isabelle (Section~\ref{sec:isabelle})
to discharge proofs, PVS and Isabelle must be
75 76
installed before \why. You should check that those proof assistants
are correctly detected by the configure script.

78 79 80 81 82 83 84 85
When configuration is finished, you can compile \why.
Installation is performed (as super-user if needed) using
make install
Installation can be tested as follows:
\item install some external provers (see Section~\ref{provers} below)
\item run \verb|why3 config --detect|
\item run some examples from the distribution, \eg you should
91 92
obtain the following (provided the required provers are installed on
your machine):
93 94
$ cd examples
$ why3 replay logic/scottish-private-club
96 97 98
 1/1 (replay OK)
$ why3 replay same_fringe
 18/18 (replay OK)
99 100 101

\subsubsection{Local Use, Without Installation}
103 104 105 106 107 108 109 110 111 112

It is not mandatory to install \why into system directories.
\why can be configured and compiled for local use as follows:
./configure --enable-local
The \why executables are then available in the subdirectory
\texttt{bin/}. This directory can be added in your \texttt{PATH}.

\subsubsection{Installation of the \why API}

By default, the \why API is not installed. It can be installed using
117 118
make byte opt \\
make install-lib \mbox{\rmfamily (as super-user)}
120 121

\section{Installing External Provers}
123 124 125 126

\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
127 128
them. There is no need to install automatic provers, \eg SMT solvers,
before compiling and installing \why.
For installation of external provers, please refer to the specific
130 131 132
section about provers from \url{}.
(If you have installed \why via \opam, note that you can install the
SMT solver Alt-Ergo via \opam as well.)

134 135 136 137 138 139
Once you have installed a prover, or a new version of a prover, you
have to run the following command:
> why3 config --detect
It scans your \texttt{PATH} for provers and updates your configuration
file (see Section~\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 CVC4 1.4 and CVC4 1.5 at the same time.
The automatic detection of provers looks for typical names for their
147 148 149 150
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
why3 config --add-prover cvc4 cvc4-dev /usr/local/bin/cvc4-dev
156 157 158 159 160 161
the first argument (here \verb|cvc4|) must be one of the family of
provers known. The list of these famillies can be obtain using
why3 config --list-prover-families
as they are in fact listed in the file \verb|provers-detection-data.conf|, typically
162 163
located in \verb|/usr/local/share/why3| after installation. See
Appendix~\ref{sec:proverdetecttiondata} for details.
164 165

\subsection{Session Update after Prover Upgrade}

169 170
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
MARCHE Claude's avatar
MARCHE Claude committed
refer to the old version of the prover. If you open one such a session
with the GUI, and replay the proofs, a popup window will show up for asking you to choose
between three options:
\item Keep the former proof attempts as they are, with the old prover version. They will not be replayed.
176 177 178 179 180 181 182 183
\item Remove the former proof attempts.
\item Upgrade the former proof attempts to an installed prover
  (typically an upgraded version). The corresponding proof attempts
  will become attached to this new prover, and marked as obsolete, to
  make their replay mandatory. If a proof attempt with this installed prover
  is already present the old proof attempt is just removed. Note that you
  need to invoke again the replay command to replay those proof
184 185
\item Copy the former proofs to an installed prover. This is a
  combination of the actions above: each proof attempt is duplicated,
186 187
  one with the former prover version, and one for the new
  version marked as obsolete.
188 189

MARCHE Claude's avatar
MARCHE Claude committed
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-copy option will just reuse the former proof scripts.
193 194 195

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: just click on one choice to remove it.

MARCHE Claude's avatar
MARCHE Claude committed
Outside the GUI, the prover upgrades are handled as follows. The
199 200
\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
203 204

% pour l'instant on ne documente pas
MARCHE Claude's avatar
MARCHE Claude committed
% {que devient l'option -to-known-prover de why3session ?
207 208 209 210
%   (d'ailleurs documenté en tant que --convert-unknown ??) Pourrait-on
%   permettre à why3session d'appliquer les choix d'association
%   vieux-prover/nouveau-prouveur stockés par l'IDE ?}

211 212 213 214 215 216

%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End: