Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

manpages.tex 5.72 KB
 MARCHE Claude committed Sep 06, 2010 1 \chapter{Reference manuals for the Why3 tools}  MARCHE Claude committed Sep 08, 2010 2 \label{chap:manpages}  MARCHE Claude committed Sep 06, 2010 3 4 5  \section{Compilation, Installation}  MARCHE Claude committed Sep 07, 2010 6 7 8 9 10 11 12 Compilation of Why3 must start with a configuration phase which is run as \begin{verbatim} ./configure \end{verbatim} This analyzes you current configuration and check if requirements hold. Compilation requires: \begin{itemize}  MARCHE Claude committed Dec 08, 2010 13 14 15 \item The Objective Caml compiler, version 3.10 or higher. It is available as a binary package for most Unix distributions. For debian-based Linux distributions, you can install the packages  MARCHE Claude committed Sep 07, 2010 16 17 18 19 20 \begin{verbatim} ocaml ocaml-native-compilers \end{verbatim} It is also installable from sources, downloadable from the Web site \url{http://caml.inria.fr/ocaml/}  MARCHE Claude committed Dec 13, 2010 21 \end{itemize}  MARCHE Claude committed Sep 07, 2010 22   MARCHE Claude committed Dec 13, 2010 23 24 For the IDE, additional Ocaml libraries are needed: \begin{itemize}  MARCHE Claude committed Sep 07, 2010 25 26 27 28 29 30 31 \item 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}  MARCHE Claude committed Dec 13, 2010 32 \item TODO Claude: sqlite3  MARCHE Claude committed Sep 07, 2010 33 34 \end{itemize}  MARCHE Claude committed Dec 13, 2010 35 36 37 38 39 40 41 42 \subsection{Local use, without installation} \begin{verbatim} ./configure --enable-local make \end{verbatim} commands are available in subdirectory \texttt{bin/}.  MARCHE Claude committed Sep 06, 2010 43 \section{Installation of external provers}  MARCHE Claude committed Sep 06, 2010 44   MARCHE Claude committed Dec 13, 2010 45 46 47 48 49 50 51 52 53 54 why-config ou IDE/Detect provers Provers which are auto-detected: (share/prover-detection-data) pour chaque prouveur: lien sur page why/prover tips.  MARCHE Claude committed Sep 06, 2010 55 56 57 58 59 \section{The \texttt{why3} command-line tool} \section{The \texttt{why3ml} tool} \section{The \texttt{why3ide} tool}  MARCHE Claude committed Dec 13, 2010 60 61 62 63 64 65 66 67 68 69 70 71 72 73 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 \label{sec:ideref} \subsection{Command-line options} \begin{description} \item[-I] $d$: adds $d$ in the load path, to search for theories. \end{description} \subsection{Left toolbar} \begin{description} \item[Provers] To each detected prover corresponds to a button in this prover framed box. Clicking on this button starts the prover on the selected goal(s). \item Start an editor on the selected task. For automatic provers, this allows to see the file sent to the prover. For interactive provers, this also allows to add or modify the corresponding proof script. The modifications are saved, and can be retrieved later even if the goal was modified. \item[Split] This splits the current goal into subgoals if it is a conjunction of two or more goals. \end{description} \subsection{Menus} \begin{description} \item[File/Detect provers] \end{description} \subsection{Preferences} \subsection{Structure of the database file} TODO  MARCHE Claude committed Sep 06, 2010 100   MARCHE Claude committed Sep 06, 2010 101 102 \section{The \texttt{why.conf} configuration file}  MARCHE Claude committed Sep 08, 2010 103 104 105 106 107 108 109 110 111 \section{Drivers of external provers} \section{Transformations} \subsection{Non-splitting transformations} \begin{description} \item[eliminate\_algebraic] Replaces algebraic data types by first-order definitions~\cite{paskevich09rr}  MARCHE Claude committed Sep 09, 2010 112 113 114 \item[eliminate\_builtin] Suppress definitions of symbols which are declared as builtin in the driver, i.e. with a syntax'' rule.  MARCHE Claude committed Sep 08, 2010 115 116 117 \item[eliminate\_definition] \item[eliminate\_definition\_func] \item[eliminate\_definition\_pred]  MARCHE Claude committed Sep 09, 2010 118 119 120 121 122 \item[eliminate\_if\_fmla] replaces formulas of the form if f1 then f2 else f3 by an equivalent formula using implications and other connectives. (TODO: detail) \item[eliminate\_if\_term] replaces terms of the form if formula then t2 else t3 by lift it at the level of the formula (TODO: detail)  MARCHE Claude committed Sep 08, 2010 123 \item[eliminate\_if]  MARCHE Claude committed Sep 09, 2010 124 125 126 127  apply both two above transformations \item[eliminate\_inductive] replaces inductive predicates by (incomplete) axiomatic definitions, i.e construction axioms and an inversion axiom (TODO: detail)  MARCHE Claude committed Sep 08, 2010 128 129 \item[eliminate\_let\_fmla] \item[eliminate\_let\_term]  MARCHE Claude committed Sep 09, 2010 130 131 \item[eliminate\_let] apply both two above transformations  MARCHE Claude committed Sep 08, 2010 132 133 134 135 136 137 \item[eliminate\_mutual\_recursion] \item[eliminate\_recursion] \item[encoding\_decorate\_mono] \item[encoding\_enumeration] \item[encoding\_simple2] \item[encoding\_smt]  MARCHE Claude committed Sep 08, 2010 138 Should we cite \cite{conchon08smt} here?  MARCHE Claude committed Sep 08, 2010 139 140 141 142 143 144 145 \item[encoding\_tptp] \item[filter\_trigger] \item[filter\_trigger\_builtin] \item[filter\_trigger\_no\_predicate] \item[hypothesis\_selection] \item[inline\_all] \item[inline\_trivial]  MARCHE Claude committed Sep 09, 2010 146 147 148 149  removes definitions of the form \begin{verbatim} logic f x_1 .. x_n = (g e_1 .. e_k) \end{verbatim}  MARCHE Claude committed Sep 10, 2010 150 151 when each $e_i$ is either a constant or one of the $x_j$, and each $x_1$ .. $x_n$ occur at most once in the $e_i$  MARCHE Claude committed Sep 09, 2010 152   MARCHE Claude committed Sep 08, 2010 153 154 \item[remove\_triggers] \item[simplify\_array]  MARCHE Claude committed Sep 09, 2010 155 156 157 \item[simplify\_formula] reduces trivial equalities $t=t$ to True and then simplifies propositional structure: removes True, False, f and f'' to f'', etc.  MARCHE Claude committed Sep 08, 2010 158 \item[simplify\_recursive\_definition]  MARCHE Claude committed Sep 09, 2010 159 160 161 162 163 164 165 166 167 168 169 170 171  reduces mutually recursive definitions if they are not really mutually recursive, e.g.: \begin{verbatim} logic f : ... = .... g ... with g : .. = e \end{verbatim} becomes \begin{verbatim} logic g : .. = e logic f : ... = .... g ... \end{verbatim} if f does not occur in e  MARCHE Claude committed Sep 08, 2010 172 \item[simplify\_trivial\_quantification]  MARCHE Claude committed Sep 09, 2010 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188  simplifies quantifications of the form \begin{verbatim} forall x, x=t -> P(x) \end{verbatim} or \begin{verbatim} forall x, t=x -> P(x) \end{verbatim} when x does not occur in t into \begin{verbatim} P(t) \end{verbatim} More generally, it applies this simplification whenever x=t appear in a negative position.  MARCHE Claude committed Sep 08, 2010 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 \item[simplify\_trivial\_quantification\_in\_goal] \item[split\_premise] \end{description} \subsection{Splitting transformations} \begin{description} \item[right\_split] \item[simplify\_formula\_and\_task] \item[split\_all] \item[split\_goal] \item[split\_goal\_pos\_all] \item[split\_goal\_pos\_axiom] \item[split\_goal\_pos\_goal] \item[split\_goal\_pos\_neg\_all] \item[split\_goal\_pos\_neg\_axiom] \item[split\_goal\_pos\_neg\_goal] \end{description}  MARCHE Claude committed Sep 06, 2010 208   MARCHE Claude committed Sep 06, 2010 209 210 211 212 213 214  %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: