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 14.3 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

\section{Compilation, Installation}
MARCHE Claude's avatar
MARCHE Claude committed
5
\label{sec:install}
MARCHE Claude's avatar
doc    
MARCHE Claude committed
6

MARCHE Claude's avatar
MARCHE Claude committed
7
8
9
10
11
12
13
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
14
15
16
\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
17
18
19
20
21
\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
22
\end{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
23

MARCHE Claude's avatar
add    
MARCHE Claude committed
24
25
For the IDE, additional Ocaml libraries are needed:
\begin{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
26
27
28
29
30
31
32
\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
MARCHE Claude committed
33
34
35
36
37
38
39
\item 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}
MARCHE Claude's avatar
MARCHE Claude committed
40
41
\end{itemize}

MARCHE Claude's avatar
add    
MARCHE Claude committed
42
43
\subsection{Local use, without installation}

MARCHE Claude's avatar
MARCHE Claude committed
44
It is not mandatory to install Why3 to use it. Local use is obtained via
MARCHE Claude's avatar
add    
MARCHE Claude committed
45
46
47
48
\begin{verbatim}
./configure --enable-local
make
\end{verbatim}
MARCHE Claude's avatar
MARCHE Claude committed
49
The Why3 executables are then available in subdirectory \texttt{bin/}.
MARCHE Claude's avatar
add    
MARCHE Claude committed
50

MARCHE Claude's avatar
MARCHE Claude committed
51
52
53
54
55
\subsection{Installation of the Why3 library}
\label{sec:installlib}

TODO

MARCHE Claude's avatar
MARCHE Claude committed
56
\section{Installation of external provers}
MARCHE Claude's avatar
doc    
MARCHE Claude committed
57

MARCHE Claude's avatar
MARCHE Claude committed
58
59
60
61
Why3 can use a wide range of external theorem provers. These need to
be installed separately, and then Why3 needs to be configured to use
them. There is no need to install these provers before compiling and
installing Why. 
MARCHE Claude's avatar
add    
MARCHE Claude committed
62

MARCHE Claude's avatar
MARCHE Claude committed
63
64
For installation of external provers, please look at the Why provers
tips page \url{http://why.lri.fr/provers.en.html}.
MARCHE Claude's avatar
add    
MARCHE Claude committed
65

MARCHE Claude's avatar
MARCHE Claude committed
66
67
For configuring Why3 to use the provers, follow intructions given in
Section~\ref{sec:why3config}.
MARCHE Claude's avatar
add    
MARCHE Claude committed
68

MARCHE Claude's avatar
MARCHE Claude committed
69
70
\section{The \texttt{why3config} command-line tool}
\label{sec:why3config}.
MARCHE Claude's avatar
add    
MARCHE Claude committed
71

MARCHE Claude's avatar
MARCHE Claude committed
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
Why3 must be configured to access external provers. Typically, this is done
by running either the command line tool
\begin{verbatim}
why3config
\end{verbatim}
or using the menu
\begin{verbatim}
File/Detect provers
\end{verbatim}
of the IDE. This must be done again each time a new prover is installed.

The set of all provers which are attempted to detect is described in
the readable configuration file \texttt{provers-detection-data.conf}
of the Why3 data directory (\eg{}
\texttt{/usr/local/share/why3}). Advanced users may try to modify this
file to add support for detection of other provers. (In that case,
please consider submitting a new prover configuration on the bug
tracking system).

The result of the prover detection is stored in the user's
configuration file (\eg{} \texttt{~/.why.conf}). Again, this file is
human readable, and advanced users may modify it in order to
experiment different ways of calling provers, \eg{} different versions
of the same prover, or with different options.

The provers which are typically attemped for detection are
\begin{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
99
100
101
102
103
104
105
106
107
108
\item Alt-Ergo~\cite{conchon08smt,ergo}: \url{http://alt-ergo.lri.fr}
\item CVC3~\cite{BarTin-CAV-07}: \url{http://cs.nyu.edu/acsys/cvc3/}
\item Coq~\cite{CoqArt}: \url{http://coq.inria.fr}
\item Eprover~\cite{schulz04ijcar}: \url{http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html}
\item Gappa~\cite{melquiond08rnc}: \url{http://gappa.gforge.inria.fr/}
\item Simplify~\cite{simplify05}: \url{http://secure.ucd.ie/products/opensource/Simplify/}
\item Spass~: \url{http://www.spass-prover.org/}
\item veriT~: \url{http://www.verit-solver.org/}
\item Yices~\cite{DM06}: \url{http://yices.csl.sri.com/}
\item Z3~\cite{z3}: \url{http://research.microsoft.com/en-us/um/redmond/projects/z3/}
MARCHE Claude's avatar
MARCHE Claude committed
109
\end{itemize}
MARCHE Claude's avatar
add    
MARCHE Claude committed
110

MARCHE Claude's avatar
MARCHE Claude committed
111
\texttt{why3config} also detects the plugins installed in the Why3
112
113
114
115
116
117
plugins directory (\eg{} \texttt{/usr/local/lib/why3/plugins}). A
plugin must register itself as a parser, a transformation or a
printer, as explained in the corresponding section.

If the user's configuration file is already present,
\texttt{why3config} will only reset unset variables to default value.
MARCHE Claude's avatar
MARCHE Claude committed
118
The option \texttt{--autodetect-provers} will detect again the available
119
provers and will replace them in the file configuration.
MARCHE Claude's avatar
MARCHE Claude committed
120
\texttt{--autodetect-plugins} will do the same for plugins.
121

MARCHE Claude's avatar
doc    
MARCHE Claude committed
122
\section{The \texttt{why3} command-line tool}
MARCHE Claude's avatar
MARCHE Claude committed
123
\label{sec:why3ref}
MARCHE Claude's avatar
doc    
MARCHE Claude committed
124

125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
Why3 is primarily used to call provers on goals contains by file in
why3 format \texttt{.why} extension. However plugins can register
parser which can extend the known format. \texttt{why3ml} apply the
following steps :
\begin{enumerate}
\item Parse the command line and report error if needed
\item Read the configuration file using the priority defined in
  section\ref{sec:whyconffile}
\item Load the plugins mentionned in the configuration. It will not
  stop if a plugin fail to load.
\item Parse and type the given files using the correct parser in order
  to obtain a set of why theory for each files. It uses
  the filename extension or the \texttt{--format} options to choose
  among the available parsers. \texttt{--list-format} gives the list
  of them.
\item Extract the selected goals inside each selected theories into
  tasks. The goals and theories are selected using the options
  \texttt{-G/--goal} and \texttt{-T/--theory}. One
  \texttt{-T/--theory} applies to the last file appearing on the
  commandline, one \texttt{-G/--goal} applies to the last theory
  appearing on the commandline. If none theories are selected in one
  file, they are all selected. If none goals are selected inside one
  selected theory, they are all selected.
\item Apply the transformation requested
  with \texttt{-a/--apply-transform} in the order they appear on the
  command line. \texttt{--list-transforms} list the known
  transformations, plugins can add more of them.
\item Apply the driver selected with the \texttt{-D/--driver} option,
  or the driver of the prover selected with \texttt{-P/--prover}
  option. \texttt{--list-provers} lists the known provers, ie the one
  which appear in the configuration file.
\item Print the result of the standard output if \texttt{-D/--driver}
  is used or call the prover and print the result if
  \texttt{-P/--prover} is used.
\end{enumerate}

\texttt{why3} call the prover sequentially, use \texttt{why3bench} if
you want to call the provers concurrently. \texttt{Why3} can also be
used to provide other informations :
\begin{itemize}
\item \texttt{print-namespace} print the namespace of the selected
  theories
\item TODO
\end{itemize}

MARCHE Claude's avatar
doc    
MARCHE Claude committed
170
171
172
\section{The \texttt{why3ml} tool}

\section{The \texttt{why3ide} tool}
MARCHE Claude's avatar
MARCHE Claude committed
173
174
175
176
177
178
179
180
\label{sec:ideref}

\subsection{Command-line options}

\begin{description}
\item[-I] $d$: adds $d$ in the load path, to search for theories.
\end{description}

MARCHE Claude's avatar
MARCHE Claude committed
181
\subsection{Left toolbar actions}
MARCHE Claude's avatar
MARCHE Claude committed
182
183

\begin{description}
MARCHE Claude's avatar
MARCHE Claude committed
184
185
186
187
188
189
\item[Context] The context in which the other tools below will
  apply. If ``only unproved goals'' is selected, no action will ever
  be applied to an already proved goal.  If ``all goals'', then
  actions are performed even if the goal is already proved. The second
  choice allows to compare provers on the same goal.

MARCHE Claude's avatar
MARCHE Claude committed
190
191
192
193
\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).

MARCHE Claude's avatar
MARCHE Claude committed
194
195
196
197
198
199
\item[Split] This splits the current goal into subgoals if it is a
  conjunction of two or more goals.

\item[Inline] If the goal is headed by a defined predicate symbol,
  expands it with this definition. [NOT YET AVAILABLE]

MARCHE Claude's avatar
MARCHE Claude committed
200
201
202
203
204
205
206
207
208
\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.

MARCHE Claude's avatar
MARCHE Claude committed
209
210
211
\item[Replay] replay all obsolete proofs [NOT YET AVAILABLE]

\item[Remove] Remove a proof attempt or a transformation. [NOT YET AVAILABLE]
MARCHE Claude's avatar
MARCHE Claude committed
212
213
214
215
216
217

\end{description}

\subsection{Menus}

\begin{description}
MARCHE Claude's avatar
MARCHE Claude committed
218
219
\item[File/Detect provers] runs provers auto-detection
\item[File/Preferences] opens a window for modifying preferred configuration
MARCHE Claude's avatar
MARCHE Claude committed
220
\end{description}
MARCHE Claude's avatar
MARCHE Claude committed
221

MARCHE Claude's avatar
MARCHE Claude committed
222
223
\subsection{Preferences}

MARCHE Claude's avatar
MARCHE Claude committed
224
225
226
227
228
229
230
231
232
233
The preferences window allows you customize
\begin{itemize}
\item the default editor to use when the \textsf{Edit} button is
  pressed. This might be overidden for a specific prover (the only way
  to do that for the moment is to manually edit the config file)
\item the time limit given to provers, in seconds
\item the maximal number of simultaneous provers allowed to run in parallel. 
\end{itemize}


MARCHE Claude's avatar
MARCHE Claude committed
234
235
\subsection{Structure of the database file}

MARCHE Claude's avatar
MARCHE Claude committed
236
[TO BE COMPLETED]
MARCHE Claude's avatar
doc    
MARCHE Claude committed
237

238
239
\section{The \texttt{why3bench} tool}

MARCHE Claude's avatar
MARCHE Claude committed
240
\section{The \texttt{why.conf} configuration file}
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
\label{sec:whyconffile}
One can defined more than one configuration file. \texttt{why3config}
and all the others \texttt{why3}'s tools use priorities for which
user's configuration file to consider:
\begin{itemize}
\item the file specified by the \texttt{-C} or \texttt{--config} options,
\item the file specified by the environment variable
  \texttt{\$WHY\_CONFIG} if set.
\item the file \texttt{why.conf} or \texttt{.why.conf} in the current
  directory.
\item the file \texttt{\$HOME/.why.conf} or \texttt{\$USERPROFILE/.why.conf}
\end{itemize}
If none of this file exists a built-in default configuration is used
which is saved in a default configuration filename, which is usually
\texttt{\$HOME/.why.conf}.

The configuration file is a human-readable text file, which is
composed by association pairs arranged by sections. Here an example of
a configuration file.

\begin{verbatim}
[main ]
datadir = "/usr/local/share/why3"
libdir = "/usr/local/lib/why3"
loadpath = "/usr/local/share/why3/theories"
memlimit = 0
running_provers_max = 2
timelimit = 10

[ide ]
default_editor = "emacs"
task_height = 384
tree_width = 438
verbose = 0
window_height = 779
window_width = 638

[prover coq]
command = "coqc %f"
driver = "/usr/local/share/why3/drivers/coq.drv"
editor = "coqide"
name = "Coq"
version = "8.2pl2"

[prover alt-ergo]
command = "why3-cpulimit %t %m alt-ergo %f"
driver = "/usr/local/share/why3/drivers/alt_ergo.drv"
editor = ""
name = "Alt-Ergo"
version = "0.91"
\end{verbatim}

A section begin with an header inside square brackets and end at the
next square brackets. Sections can't be nested. The header of a
section can be only one identifier, \texttt{main} and \texttt{ide} in
the example, or it can be composed by a family name and one family
argument, \texttt{prover} is one family name, \texttt{coq} and
\texttt{alt-ergo} are the family argument.


Inside a section, one key can be associated to an integer (.eg -555),
a boolean (true, false) or a string (.eg "emacs"). One key can appear
only once except if its a multi-value key. The order of apparition of
the keys inside a section matter only for the multi-value key.
MARCHE Claude's avatar
MARCHE Claude committed
305

MARCHE Claude's avatar
MARCHE Claude committed
306
\section{Drivers of external provers}
307
The drivers of external provers are 
MARCHE Claude's avatar
MARCHE Claude committed
308
309

\section{Transformations}
MARCHE Claude's avatar
MARCHE Claude committed
310
\label{sec:transformations}
MARCHE Claude's avatar
MARCHE Claude committed
311
312
313
314
315
316

\subsection{Non-splitting transformations}

\begin{description}
\item[eliminate\_algebraic] Replaces algebraic data types by first-order
definitions~\cite{paskevich09rr}
317
318
319
\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
320
321
322
\item[eliminate\_definition]
\item[eliminate\_definition\_func]
\item[eliminate\_definition\_pred]
323
324
325
326
327
\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
328
\item[eliminate\_if]
329
330
331
332
  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
333
334
\item[eliminate\_let\_fmla]
\item[eliminate\_let\_term]
335
336
\item[eliminate\_let]
  apply both two above transformations
MARCHE Claude's avatar
MARCHE Claude committed
337
338
339
340
341
342
\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
343
Should we cite \cite{conchon08smt} here?
MARCHE Claude's avatar
MARCHE Claude committed
344
345
346
347
348
349
350
\item[encoding\_tptp]
\item[filter\_trigger]
\item[filter\_trigger\_builtin]
\item[filter\_trigger\_no\_predicate]
\item[hypothesis\_selection]
\item[inline\_all]
\item[inline\_trivial]
351
352
353
354
  removes definitions of the form
\begin{verbatim}
logic f x_1 .. x_n = (g e_1 .. e_k)
\end{verbatim}
355
356
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$ 
357

MARCHE Claude's avatar
MARCHE Claude committed
358
359
\item[remove\_triggers]
\item[simplify\_array]
360
361
362
\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
363
\item[simplify\_recursive\_definition]
364
365
366
367
368
369
370
371
372
373
374
375
376
  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
377
\item[simplify\_trivial\_quantification]
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
  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
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
\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
413

MARCHE Claude's avatar
doc    
MARCHE Claude committed
414
415
416
417
418
419

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