<commit_before>\chapter{Reference manuals for the \why\ tools}
\label{chap:manpages}

\section{Compilation, Installation}
\label{sec:install}

Compilation of \why\ must start with a configuration phase which is run as
\begin{verbatim}
./configure
\end{verbatim}
This analyzes your current configuration and checks 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 site
\url{http://caml.inria.fr/ocaml/}
\end{itemize}

For the IDE, additional OCaml libraries are needed:
\begin{itemize}
\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 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}
\end{itemize}

When configuration is finished, you can compile \why.
\begin{verbatim}
make
\end{verbatim}

\subsection{Local use, without installation}

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/}.

\subsection{Installation of the \why\ library}
\label{sec:installlib}

By default, the \why\ library is not installed. It can be installed using
\begin{verbatim}
make byte opt
make install_lib
\end{verbatim}

\section{Installation of external 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
them. There is no need to install these provers before compiling and
installing Why. 

For installation of external provers, please look at the Why provers
tips page \url{http://why.lri.fr/provers.en.html}.

For configuring \why\ to use the provers, follow instructions given in
Section~\ref{sec:why3config}.

\section{The \texttt{why3config} command-line tool}
\label{sec:why3config}.

\why\ 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 redone each time a new prover is installed.

The provers which \why\ attempts to detect are described in
the readable configuration file \texttt{provers-detection-data.conf}
of the \why\ 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 provers detection is stored in the user's
configuration file (\verb+~/.why.conf+ or, in the case of local
installation, \verb+why.conf+ in Why3 sources top directory). This file 
is also human-readable, and advanced users may modify it in order to
experiment with different ways of calling provers, \eg{} different 
versions of the same prover, or with different options.

The provers which are typically looked for are
\begin{itemize}
\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/}
\end{itemize}

\texttt{why3config} also detects the plugins installed in the \why\
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,
but will not try to detect provers. 
The option \texttt{--detect-provers} should be used to force
\why\ to detect again the available
provers and to replace them in the configuration file. The option
\texttt{--detect-plugins} will do the same for plugins.

\section{The \texttt{why3} command-line tool}
\label{sec:why3ref}

\why\ is primarily used to call provers on goals contained in an
input file. By default, such a file must be written in \why language
and have the extension \texttt{.why}. However, a dynamically loaded
plugin can register a parser for some other format of logical problems,
\eg{} TPTP or SMTlib.

The \texttt{why3} tool executes the following steps:
\begin{enumerate}
\item Parse the command line and report errors if needed.
\item Read the configuration file using the priority defined in
  Section~\ref{sec:whyconffile}.
\item Load the plugins mentioned in the configuration. It will not
  stop if some plugin fails to load.
\item Parse and typecheck the given files using the correct parser in order
  to obtain a set of \why\ theories for each file. It uses
  the filename extension or the \texttt{--format} option to choose
  among the available parsers. The \texttt{--list-format} option gives 
  the list of registered parsers.
\item Extract the selected goals inside each of the selected theories 
  into tasks. The goals and theories are selected using the options
  \texttt{-G/--goal} and \texttt{-T/--theory}. The option
  \texttt{-T/--theory} applies to the last file appearing on the
  command line, the option \texttt{-G/--goal} applies to the last theory
  appearing on the command line. If no theories are selected in a file,
  then every theory is considered as selected. If no goals are selected
  in a theory, then every goal is considered as selected.
\item Apply the transformation requested
  with \texttt{-a/--apply-transform} in their order of appearance 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, i.e.~the ones
  which appear in the configuration file.
\item If the option \texttt{-P/--prover} is given, call the selected prover
  on each generated task and print the results. If the option
  \texttt{-D/--driver} is given, print each generated task using
  the format specified in the selected driver.
\end{enumerate}

%\texttt{why3} calls the provers sequentially, use \texttt{why3bench} if *)
%you want to call the provers concurrently.  *)

The provers can answer the following output:
\begin{itemize}
\item[Valid] the goal is proved in the given context,
\item[Unknown] the prover stop by itself to search,
\item[Timeout] the prover doesn't have enough time,
\item[Failure] an error occured,
\item[Invalid] the prover know the goal can't be proved
\end{itemize}
% \why\ can also be *)
% used to provide other informations : *)
% \begin{itemize} *)
% \item \texttt{print-namespace} print the namespace of the selected *)
%   theories *)
% \item TO BE COMPLETED *)
% \end{itemize} *)

\section{The \texttt{why3ide} GUI}
\label{sec:ideref}

The basic usage of the GUI is described by the tutorial of
Section~\ref{sec:gui}. We describe here the command-line options and
the actions of the various menus and buttons of the interface.

\subsection{Command-line options}
<commit_msg>Doc : -bisect<commit_after>\chapter{Reference manuals for the \why\ tools}
\label{chap:manpages}

\section{Compilation, Installation}
\label{sec:install}

Compilation of \why\ must start with a configuration phase which is run as
\begin{verbatim}
./configure
\end{verbatim}
This analyzes your current configuration and checks 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 site
\url{http://caml.inria.fr/ocaml/}
\end{itemize}

For the IDE, additional OCaml libraries are needed:
\begin{itemize}
\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 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}
\end{itemize}

When configuration is finished, you can compile \why.
\begin{verbatim}
make
\end{verbatim}

\subsection{Local use, without installation}

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/}.

\subsection{Installation of the \why\ library}
\label{sec:installlib}

By default, the \why\ library is not installed. It can be installed using
\begin{verbatim}
make byte opt
make install_lib
\end{verbatim}

\section{Installation of external 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
them. There is no need to install these provers before compiling and
installing Why. 

For installation of external provers, please look at the Why provers
tips page \url{http://why.lri.fr/provers.en.html}.

For configuring \why\ to use the provers, follow instructions given in
Section~\ref{sec:why3config}.

\section{The \texttt{why3config} command-line tool}
\label{sec:why3config}.

\why\ 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 redone each time a new prover is installed.

The provers which \why\ attempts to detect are described in
the readable configuration file \texttt{provers-detection-data.conf}
of the \why\ 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 provers detection is stored in the user's
configuration file (\verb+~/.why.conf+ or, in the case of local
installation, \verb+why.conf+ in Why3 sources top directory). This file 
is also human-readable, and advanced users may modify it in order to
experiment with different ways of calling provers, \eg{} different 
versions of the same prover, or with different options.

The provers which are typically looked for are
\begin{itemize}
\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/}
\end{itemize}

\texttt{why3config} also detects the plugins installed in the \why\
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,
but will not try to detect provers. 
The option \texttt{--detect-provers} should be used to force
\why\ to detect again the available
provers and to replace them in the configuration file. The option
\texttt{--detect-plugins} will do the same for plugins.

\section{The \texttt{why3} command-line tool}
\label{sec:why3ref}

\why\ is primarily used to call provers on goals contained in an
input file. By default, such a file must be written in \why language
and have the extension \texttt{.why}. However, a dynamically loaded
plugin can register a parser for some other format of logical problems,
\eg{} TPTP or SMTlib.

The \texttt{why3} tool executes the following steps:
\begin{enumerate}
\item Parse the command line and report errors if needed.
\item Read the configuration file using the priority defined in
  Section~\ref{sec:whyconffile}.
\item Load the plugins mentioned in the configuration. It will not
  stop if some plugin fails to load.
\item Parse and typecheck the given files using the correct parser in order
  to obtain a set of \why\ theories for each file. It uses
  the filename extension or the \texttt{--format} option to choose
  among the available parsers. The \texttt{--list-format} option gives 
  the list of registered parsers.
\item Extract the selected goals inside each of the selected theories 
  into tasks. The goals and theories are selected using the options
  \texttt{-G/--goal} and \texttt{-T/--theory}. The option
  \texttt{-T/--theory} applies to the last file appearing on the
  command line, the option \texttt{-G/--goal} applies to the last theory
  appearing on the command line. If no theories are selected in a file,
  then every theory is considered as selected. If no goals are selected
  in a theory, then every goal is considered as selected.
\item Apply the transformation requested
  with \texttt{-a/--apply-transform} in their order of appearance 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, i.e.~the ones
  which appear in the configuration file.
\item If the option \texttt{-P/--prover} is given, call the selected prover
  on each generated task and print the results. If the option
  \texttt{-D/--driver} is given, print each generated task using
  the format specified in the selected driver.
\end{enumerate}

%\texttt{why3} calls the provers sequentially, use \texttt{why3bench} if *)
%you want to call the provers concurrently.  *)

The provers can answer the following output:
\begin{description}
\item[Valid] the goal is proved in the given context,
\item[Unknown] the prover stop by itself to search,
\item[Timeout] the prover doesn't have enough time,
\item[Failure] an error occured,
\item[Invalid] the prover know the goal can't be proved
\end{description}
% \why\ can also be *)
% used to provide other informations : *)
% \begin{itemize} *)
% \item \texttt{print-namespace} print the namespace of the selected *)
%   theories *)
% \item TO BE COMPLETED *)
% \end{itemize} *)

The option \texttt{--bisect} change the behaviors of why3. With this
option, \texttt{-P/--prover} and \texttt{-o/--output} must be given
and a valid goal must be selected. The last step executed by why3 is
replaced by computing a minimal set (in the great majority of the
case) of declarations which still prove the goal. Currently it doesn't
use any information provided by the prover, it call the prover
multiple time with reduced context. The minimal set of declarations is
then written in the prover syntax into a file located in the directory
given to the \texttt{-o/--output} option.

\section{The \texttt{why3ide} GUI}
\label{sec:ideref}

The basic usage of the GUI is described by the tutorial of
Section~\ref{sec:gui}. We describe here the command-line options and
the actions of the various menus and buttons of the interface.

\subsection{Command-line options}

{'fraction_non_alphanumeric': 0.09290530805140915, 'fraction_numerical': 0.00507175378940695, 'mean_word_length': 4.312921004286589, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 8, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3343831', 'n_tokens_mistral': 5248, 'n_tokens_neox': 5102, 'n_words': 2183}