install.tex 6.98 KB
Newer Older
1
2
3
4
5
6
7

\chapter{Compilation, Installation}
\label{sec:install}


In short, installation proceeds as follows.
\begin{flushleft}\ttfamily
8
9
  ./configure\\
  make\\
10
11
12
13
14
15
16
17
18
19
20
21
22
23
  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}
24
\item The Objective Caml compiler, version 3.11.2 or higher. It is
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
  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}

55
If you want to use the specific Coq features, \ie the Coq
MARCHE Claude's avatar
MARCHE Claude committed
56
57
58
59
60
tactic~\ref{chap:tactic} and Coq realizations~\ref{chap:realizations},
then Coq has to be installed before \why. Look at the summary printed
at the end of the configuration script to check if Coq has been
detected properly.

61
62
63
64
65
66
67
68
69
70
71
72
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|
73
\item run some examples from the distribution, \eg you should
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
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}.

103
104
\section{Installation of the \why API}
\label{sec:installlib}\index{API}
105

106
By default, the \why API is not installed. It can be installed using
107
108
\begin{flushleft}\ttfamily
make byte opt \\
109
make install-lib \mbox{\rmfamily (as super-user)}
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
\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}

128
Since version 0.72, \why is able to use several versions of the same
129
prover, \eg it can use both CVC3 2.2 and CVC3 2.4.1 at the same time.
130
The automatic detection of provers looks for typical names for their
131
executable command, \eg \texttt{cvc3} for CVC3. However, if you
132
133
134
135
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
136
\texttt{why3config}, \eg
137
\begin{verbatim}
138
why3config --detect --add-prover cvc3-2.4 /usr/local/bin/cvc3-2.4.1
139
140
141
\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
142
143
located in \verb|/usr/local/share/why3| after installation. See
Appendix~\ref{sec:proverdetecttiondata} for details.
144
145
146


\section{Session Update after Prover Upgrade}
147
\label{sec:uninstalledprovers}
148

149
If you happen to upgrade a prover, \eg installing CVC3 2.4.1 in place
150
of CVC3 2.2, then the proof sessions formerly recorded will still
MARCHE Claude's avatar
MARCHE Claude committed
151
refer to the old version of the prover. If you open one such a session
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
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}

MARCHE Claude's avatar
MARCHE Claude committed
167
Notice that if the prover under consideration is an interactive one, then
168
169
170
171
172
173
174
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.

MARCHE Claude's avatar
MARCHE Claude committed
175
176
Outside the GUI, the prover upgrades are handled as follows. The
\texttt{why3replayer} tool will just ignore proof attempts marked as
177
178
archived. Conversely, a non-archived proof attempt with a non-existent
prover will be reported as a replay failure. The tool
179
\texttt{why3session} allows you to perform move or copy operations on
180
181
proof attempts in a fine-grain way, using filters, as detailed in
Section~\ref{sec:why3session}.
182
183


184
185
186
187
188
189
% pour l'instant on ne documente pas
% \todo{que devient l'option -to-known-prover de why3session ?
%   (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 ?}

190
191
192
193
194
195

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