install.tex 8.05 KB
Newer Older
1 2 3

\chapter{Compilation, Installation}
\label{sec:install}
4
%HEVEA\cutname{install.html}
5

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
\begin{verbatim}
> opam install why3
\end{verbatim}
15
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.
20
\begin{flushleft}\ttfamily
21 22 23
  > ./configure\\
  > make\\
  > make install \mbox{\rmfamily (as super-user)}
24 25 26 27
\end{flushleft}

After unpacking the distribution, go to the newly created directory
\texttt{why3-\whyversion}. Compilation must start with a
28
configuration phase which is run as
29
\begin{verbatim}
30
> ./configure
31 32 33 34
\end{verbatim}
This analyzes your current configuration and checks if requirements hold.
Compilation requires:
\begin{itemize}
35
\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
\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}
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
\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}

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{http://ocaml.info/home/ocaml_sources.html#ocaml-sqlite3}
66 67
\end{itemize}

68

Guillaume Melquiond's avatar
Guillaume Melquiond committed
69
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.
77

78 79 80 81 82 83 84 85
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}
86
Installation can be tested as follows:
87
\begin{enumerate}
88
\item install some external provers (see Section~\ref{provers} below)
89
\item run \verb|why3 config --detect|
90
\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
\begin{verbatim}
$ cd examples
95
$ why3 replay logic/scottish-private-club
96 97 98
 1/1 (replay OK)
$ why3 replay same_fringe
 18/18 (replay OK)
99 100 101
\end{verbatim}
\end{enumerate}

102
\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:
\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}.

113
\subsubsection{Installation of the \why API}
114
\label{sec:installlib}\index{API}
115

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

122
\section{Installing External Provers}
123 124 125 126
\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
127 128
them. There is no need to install automatic provers, \eg SMT solvers,
before compiling and installing \why.
129
For installation of external provers, please refer to the specific
130 131 132
section about provers from \url{http://why3.lri.fr/}.
(If you have installed \why via \opam, note that you can install the
SMT solver Alt-Ergo via \opam as well.)
133

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:
\begin{verbatim}
> why3 config --detect
\end{verbatim}
It scans your \texttt{PATH} for provers and updates your configuration
140
file (see Section~\ref{sec:why3config}) accordingly.
141

142
\subsection{Multiple Versions of the Same Prover}
143

144
\why is able to use several versions of the same
145
prover, \eg it can use both CVC4 1.4 and CVC4 1.5 at the same time.
146
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
151
added to the \texttt{config} command to specify names of prover executables, \eg
152
\index{add-prover@\verb+--add-prover+}
153
\begin{verbatim}
154
why3 config --add-prover cvc4 cvc4-dev /usr/local/bin/cvc4-dev
155
\end{verbatim}
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
\begin{verbatim}
why3 config --list-prover-families
\end{verbatim}
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


166
\subsection{Session Update after Prover Upgrade}
167
\label{sec:uninstalledprovers}
168

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
171
refer to the old version of the prover. If you open one such a session
172
with the GUI, and replay the proofs, a popup window will show up for asking you to choose
173
between three options:
174
\begin{itemize}
175
\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
  attempts.
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
\end{itemize}

MARCHE Claude's avatar
MARCHE Claude committed
190
Notice that if the prover under consideration is an interactive one, then
191
the copy option will duplicate also the edited proof scripts, whereas
192
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
196
discard these choices via the \textsf{Preferences} dialog: just click on one choice to remove it.
197

MARCHE Claude's avatar
MARCHE Claude committed
198
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
201
proof attempts in a fine-grained way, using filters, as detailed in
202
Section~\ref{sec:why3session}.
203 204


205
% pour l'instant on ne documente pas
MARCHE Claude's avatar
MARCHE Claude committed
206
% {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: