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
Newer Older
MARCHE Claude's avatar
doc    
MARCHE Claude committed
1
\chapter{Reference manuals for the Why3 tools}
MARCHE Claude's avatar
MARCHE Claude committed
2
\label{chap:manpages}
MARCHE Claude's avatar
doc    
MARCHE Claude committed
3
4
5

\section{Compilation, Installation}

MARCHE Claude's avatar
MARCHE Claude committed
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's avatar
MARCHE Claude committed
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's avatar
MARCHE Claude committed
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's avatar
add    
MARCHE Claude committed
21
\end{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
22

MARCHE Claude's avatar
add    
MARCHE Claude committed
23
24
For the IDE, additional Ocaml libraries are needed:
\begin{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
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's avatar
add    
MARCHE Claude committed
32
\item TODO Claude: sqlite3
MARCHE Claude's avatar
MARCHE Claude committed
33
34
\end{itemize}

MARCHE Claude's avatar
add    
MARCHE Claude committed
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's avatar
MARCHE Claude committed
43
\section{Installation of external provers}
MARCHE Claude's avatar
doc    
MARCHE Claude committed
44

MARCHE Claude's avatar
add    
MARCHE Claude committed
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's avatar
doc    
MARCHE Claude committed
55
56
57
58
59
\section{The \texttt{why3} command-line tool}

\section{The \texttt{why3ml} tool}

\section{The \texttt{why3ide} tool}
MARCHE Claude's avatar
MARCHE Claude committed
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[Edit] 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's avatar
doc    
MARCHE Claude committed
100

MARCHE Claude's avatar
MARCHE Claude committed
101
102
\section{The \texttt{why.conf} configuration file}

MARCHE Claude's avatar
MARCHE Claude committed
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}
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's avatar
MARCHE Claude committed
115
116
117
\item[eliminate\_definition]
\item[eliminate\_definition\_func]
\item[eliminate\_definition\_pred]
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's avatar
MARCHE Claude committed
123
\item[eliminate\_if]
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's avatar
MARCHE Claude committed
128
129
\item[eliminate\_let\_fmla]
\item[eliminate\_let\_term]
130
131
\item[eliminate\_let]
  apply both two above transformations
MARCHE Claude's avatar
MARCHE Claude committed
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's avatar
biblio    
MARCHE Claude committed
138
Should we cite \cite{conchon08smt} here?
MARCHE Claude's avatar
MARCHE Claude committed
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]
146
147
148
149
  removes definitions of the form
\begin{verbatim}
logic f x_1 .. x_n = (g e_1 .. e_k)
\end{verbatim}
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$ 
152

MARCHE Claude's avatar
MARCHE Claude committed
153
154
\item[remove\_triggers]
\item[simplify\_array]
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's avatar
MARCHE Claude committed
158
\item[simplify\_recursive\_definition]
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's avatar
MARCHE Claude committed
172
\item[simplify\_trivial\_quantification]
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's avatar
MARCHE Claude committed
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's avatar
MARCHE Claude committed
208

MARCHE Claude's avatar
doc    
MARCHE Claude committed
209
210
211
212
213
214

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