install.tex 8.05 KB
 MARCHE Claude committed Apr 10, 2012 1 2 3  \chapter{Compilation, Installation} \label{sec:install}  Guillaume Melquiond committed Oct 02, 2017 4 %HEVEA\cutname{install.html}  MARCHE Claude committed Apr 10, 2012 5   Jean-Christophe Filliatre committed May 24, 2018 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}  Guillaume Melquiond committed Jun 25, 2018 15 Then jump to Section~\ref{provers} to install external provers.  Jean-Christophe Filliatre committed May 24, 2018 16 17 18 19  \subsection{Installation Instructions from Source Distribution} In short, installation from sources proceeds as follows.  MARCHE Claude committed Apr 10, 2012 20 \begin{flushleft}\ttfamily  Jean-Christophe Filliatre committed May 24, 2018 21 22 23  > ./configure\\ > make\\ > make install \mbox{\rmfamily (as super-user)}  MARCHE Claude committed Apr 10, 2012 24 25 26 27 \end{flushleft} After unpacking the distribution, go to the newly created directory \texttt{why3-\whyversion}. Compilation must start with a  Guillaume Melquiond committed Mar 08, 2018 28 configuration phase which is run as  MARCHE Claude committed Apr 10, 2012 29 \begin{verbatim}  Jean-Christophe Filliatre committed May 24, 2018 30 > ./configure  MARCHE Claude committed Apr 10, 2012 31 32 33 34 \end{verbatim} This analyzes your current configuration and checks if requirements hold. Compilation requires: \begin{itemize}  Guillaume Melquiond committed Mar 08, 2018 35 \item The Objective Caml compiler. It is  MARCHE Claude committed Apr 10, 2012 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}  Guillaume Melquiond committed Jun 26, 2014 48 49 \item For the graphical interface, the Lablgtk2 library is needed. It provides OCaml  MARCHE Claude committed Apr 10, 2012 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}  MARCHE Claude committed Jun 18, 2018 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}  MARCHE Claude committed Apr 10, 2012 66 67 \end{itemize}  MARCHE Claude committed Feb 01, 2014 68   Guillaume Melquiond committed May 29, 2018 69 If you want to use the Coq realizations  MARCHE Claude committed Feb 01, 2014 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 committed May 29, 2018 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  MARCHE Claude committed Feb 01, 2014 75 76 installed before \why. You should check that those proof assistants are correctly detected by the configure script.  MARCHE Claude committed May 07, 2012 77   MARCHE Claude committed Apr 10, 2012 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}  Guillaume Melquiond committed Jun 03, 2014 86 Installation can be tested as follows:  MARCHE Claude committed Apr 10, 2012 87 \begin{enumerate}  Guillaume Melquiond committed Jun 25, 2018 88 \item install some external provers (see Section~\ref{provers} below)  Guillaume Melquiond committed Jun 03, 2014 89 \item run \verb|why3 config --detect|  Guillaume Melquiond committed May 09, 2012 90 \item run some examples from the distribution, \eg you should  Jean-Christophe Filliatre committed May 24, 2018 91 92 obtain the following (provided the required provers are installed on your machine):  MARCHE Claude committed Apr 10, 2012 93 94 \begin{verbatim} $cd examples  Guillaume Melquiond committed Jun 16, 2014 95 $ why3 replay logic/scottish-private-club  Jean-Christophe Filliatre committed May 24, 2018 96 97 98  1/1 (replay OK) \$ why3 replay same_fringe 18/18 (replay OK)  MARCHE Claude committed Apr 10, 2012 99 100 101 \end{verbatim} \end{enumerate}  Jean-Christophe Filliatre committed May 24, 2018 102 \subsubsection{Local Use, Without Installation}  MARCHE Claude committed Apr 10, 2012 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}.  Jean-Christophe Filliatre committed May 24, 2018 113 \subsubsection{Installation of the \why API}  Jean-Christophe Filliatre committed Aug 21, 2012 114 \label{sec:installlib}\index{API}  MARCHE Claude committed Apr 10, 2012 115   Jean-Christophe Filliatre committed Aug 21, 2012 116 By default, the \why API is not installed. It can be installed using  MARCHE Claude committed Apr 10, 2012 117 118 \begin{flushleft}\ttfamily make byte opt \\  Jean-Christophe Filliatre committed Aug 21, 2012 119 make install-lib \mbox{\rmfamily (as super-user)}  MARCHE Claude committed Apr 10, 2012 120 121 \end{flushleft}  Jean-Christophe Filliatre committed May 24, 2018 122 \section{Installing External Provers}  MARCHE Claude committed Apr 10, 2012 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  Guillaume Melquiond committed Jun 24, 2014 127 128 them. There is no need to install automatic provers, \eg SMT solvers, before compiling and installing \why.  MARCHE Claude committed Apr 10, 2012 129 For installation of external provers, please refer to the specific  Jean-Christophe Filliatre committed May 24, 2018 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.)  MARCHE Claude committed Apr 10, 2012 133   Jean-Christophe Filliatre committed May 24, 2018 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  Guillaume Melquiond committed Jun 25, 2018 140 file (see Section~\ref{sec:why3config}) accordingly.  MARCHE Claude committed Apr 10, 2012 141   Jean-Christophe Filliatre committed May 24, 2018 142 \subsection{Multiple Versions of the Same Prover}  MARCHE Claude committed Apr 10, 2012 143   Guillaume Melquiond committed Jun 26, 2014 144 \why is able to use several versions of the same  MARCHE Claude committed May 29, 2018 145 prover, \eg it can use both CVC4 1.4 and CVC4 1.5 at the same time.  MARCHE Claude committed Apr 10, 2012 146 The automatic detection of provers looks for typical names for their  MARCHE Claude committed May 29, 2018 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  Jean-Christophe Filliatre committed May 24, 2018 151 added to the \texttt{config} command to specify names of prover executables, \eg  Guillaume Melquiond committed Jun 26, 2014 152 \index{add-prover@\verb+--add-prover+}  MARCHE Claude committed Apr 10, 2012 153 \begin{verbatim}  DAILLER Sylvain committed Dec 19, 2018 154 why3 config --add-prover cvc4 cvc4-dev /usr/local/bin/cvc4-dev  MARCHE Claude committed Apr 10, 2012 155 \end{verbatim}  DAILLER Sylvain committed Dec 19, 2018 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  MARCHE Claude committed Apr 12, 2012 162 163 located in \verb|/usr/local/share/why3| after installation. See Appendix~\ref{sec:proverdetecttiondata} for details.  MARCHE Claude committed Apr 10, 2012 164 165   Jean-Christophe Filliatre committed May 24, 2018 166 \subsection{Session Update after Prover Upgrade}  MARCHE Claude committed Apr 13, 2012 167 \label{sec:uninstalledprovers}  MARCHE Claude committed Apr 10, 2012 168   Jean-Christophe Filliatre committed May 24, 2018 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 committed Apr 10, 2012 171 refer to the old version of the prover. If you open one such a session  MARCHE Claude committed May 29, 2018 172 with the GUI, and replay the proofs, a popup window will show up for asking you to choose  Jean-Christophe Filliatre committed May 24, 2018 173 between three options:  MARCHE Claude committed Apr 10, 2012 174 \begin{itemize}  MARCHE Claude committed May 29, 2018 175 \item Keep the former proof attempts as they are, with the old prover version. They will not be replayed.  François Bobot committed Sep 10, 2018 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.  MARCHE Claude committed Apr 10, 2012 184 185 \item Copy the former proofs to an installed prover. This is a combination of the actions above: each proof attempt is duplicated,  MARCHE Claude committed May 29, 2018 186 187  one with the former prover version, and one for the new version marked as obsolete.  MARCHE Claude committed Apr 10, 2012 188 189 \end{itemize}  MARCHE Claude committed Apr 10, 2012 190 Notice that if the prover under consideration is an interactive one, then  MARCHE Claude committed Apr 10, 2012 191 the copy option will duplicate also the edited proof scripts, whereas  MARCHE Claude committed May 29, 2018 192 the upgrade-without-copy option will just reuse the former proof scripts.  MARCHE Claude committed Apr 10, 2012 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  MARCHE Claude committed May 29, 2018 196 discard these choices via the \textsf{Preferences} dialog: just click on one choice to remove it.  MARCHE Claude committed Apr 10, 2012 197   MARCHE Claude committed Apr 10, 2012 198 Outside the GUI, the prover upgrades are handled as follows. The  MARCHE Claude committed May 29, 2018 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  Guillaume Melquiond committed Jun 03, 2014 201 proof attempts in a fine-grained way, using filters, as detailed in  MARCHE Claude committed Apr 13, 2012 202 Section~\ref{sec:why3session}.  MARCHE Claude committed Apr 10, 2012 203 204   MARCHE Claude committed Apr 17, 2012 205 % pour l'instant on ne documente pas  MARCHE Claude committed Oct 26, 2012 206 % {que devient l'option -to-known-prover de why3session ?  MARCHE Claude committed Apr 17, 2012 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 ?}  MARCHE Claude committed Apr 10, 2012 211 212 213 214 215 216  %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: