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

\section{Compilation, Installation}

MARCHE Claude's avatar
MARCHE Claude committed
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
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}
\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
\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/}

\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}

\item TODO: sqlite3
\end{itemize}

MARCHE Claude's avatar
MARCHE Claude committed
30
\section{Installation of external provers}
MARCHE Claude's avatar
doc    
MARCHE Claude committed
31
32
33
34
35
36
37

\section{The \texttt{why3} command-line tool}

\section{The \texttt{why3ml} tool}

\section{The \texttt{why3ide} tool}

MARCHE Claude's avatar
MARCHE Claude committed
38
39
40
\section{The \texttt{why.conf} configuration file}


MARCHE Claude's avatar
doc    
MARCHE Claude committed
41
42
43
44
45
46

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