install.tex 6.98 KB
 MARCHE Claude committed Apr 10, 2012 1 2 3 4 5 6 7  \chapter{Compilation, Installation} \label{sec:install} In short, installation proceeds as follows. \begin{flushleft}\ttfamily  Guillaume Melquiond committed May 09, 2012 8 9  ./configure\\ make\\  MARCHE Claude committed Apr 10, 2012 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}  MARCHE Claude committed Apr 17, 2012 24 \item The Objective Caml compiler, version 3.11.2 or higher. It is  MARCHE Claude committed Apr 10, 2012 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}  Guillaume Melquiond committed May 09, 2012 55 If you want to use the specific Coq features, \ie the Coq  MARCHE Claude committed May 07, 2012 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.  MARCHE Claude committed Apr 10, 2012 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|  Guillaume Melquiond committed May 09, 2012 73 \item run some examples from the distribution, \eg you should  MARCHE Claude committed Apr 10, 2012 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}.  Jean-Christophe Filliâtre committed Aug 21, 2012 103 104 \section{Installation of the \why API} \label{sec:installlib}\index{API}  MARCHE Claude committed Apr 10, 2012 105   Jean-Christophe Filliâtre committed Aug 21, 2012 106 By default, the \why API is not installed. It can be installed using  MARCHE Claude committed Apr 10, 2012 107 108 \begin{flushleft}\ttfamily make byte opt \\  Jean-Christophe Filliâtre committed Aug 21, 2012 109 make install-lib \mbox{\rmfamily (as super-user)}  MARCHE Claude committed Apr 10, 2012 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}  MARCHE Claude committed Apr 12, 2012 128 Since version 0.72, \why is able to use several versions of the same  Guillaume Melquiond committed May 09, 2012 129 prover, \eg it can use both CVC3 2.2 and CVC3 2.4.1 at the same time.  MARCHE Claude committed Apr 10, 2012 130 The automatic detection of provers looks for typical names for their  Guillaume Melquiond committed May 09, 2012 131 executable command, \eg \texttt{cvc3} for CVC3. However, if you  MARCHE Claude committed Apr 10, 2012 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  Guillaume Melquiond committed May 09, 2012 136 \texttt{why3config}, \eg  MARCHE Claude committed Apr 10, 2012 137 \begin{verbatim}  MARCHE Claude committed Apr 12, 2012 138 why3config --detect --add-prover cvc3-2.4 /usr/local/bin/cvc3-2.4.1  MARCHE Claude committed Apr 10, 2012 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  MARCHE Claude committed Apr 12, 2012 142 143 located in \verb|/usr/local/share/why3| after installation. See Appendix~\ref{sec:proverdetecttiondata} for details.  MARCHE Claude committed Apr 10, 2012 144 145 146  \section{Session Update after Prover Upgrade}  MARCHE Claude committed Apr 13, 2012 147 \label{sec:uninstalledprovers}  MARCHE Claude committed Apr 10, 2012 148   Guillaume Melquiond committed May 09, 2012 149 If you happen to upgrade a prover, \eg installing CVC3 2.4.1 in place  MARCHE Claude committed Apr 10, 2012 150 of CVC3 2.2, then the proof sessions formerly recorded will still  MARCHE Claude committed Apr 10, 2012 151 refer to the old version of the prover. If you open one such a session  MARCHE Claude committed Apr 10, 2012 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 committed Apr 10, 2012 167 Notice that if the prover under consideration is an interactive one, then  MARCHE Claude committed Apr 10, 2012 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 committed Apr 10, 2012 175 176 Outside the GUI, the prover upgrades are handled as follows. The \texttt{why3replayer} tool will just ignore proof attempts marked as  MARCHE Claude committed Apr 13, 2012 177 178 archived. Conversely, a non-archived proof attempt with a non-existent prover will be reported as a replay failure. The tool  MARCHE Claude committed Apr 10, 2012 179 \texttt{why3session} allows you to perform move or copy operations on  MARCHE Claude committed Apr 13, 2012 180 181 proof attempts in a fine-grain way, using filters, as detailed in Section~\ref{sec:why3session}.  MARCHE Claude committed Apr 10, 2012 182 183   MARCHE Claude committed Apr 17, 2012 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 ?}  MARCHE Claude committed Apr 10, 2012 190 191 192 193 194 195  %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: