Commit 494c9bd7 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add some more index entries.

parent 2c68c0f4
......@@ -21,6 +21,8 @@ others.
Notice there is an alternative way to explore the contents of a
library, using the \verb|why3| command with option
\verb|-T| and a qualified theory name, for example:
> why3 -T bool.Ite
theory Ite
......@@ -45,6 +47,9 @@ defined in it.
\item[Bool] provides the Boolean data type \verb|bool| with
constructors \verb|True| and \verb|False|; and operations \verb|andb|, \verb|orb|, \verb|xorb|, \verb|notb|.
\item[Ite] provides the polymorphic if-then-else operator written as \verb|ite|.
......@@ -132,6 +137,8 @@ such as the sorted predicate, permutation, etc.
This library provides the classical ML option type with constructors
\verb|None| and \verb|Some|.
\subsection{Library \texttt{list}}
......@@ -156,6 +163,9 @@ and the one providing arrays.
\item[Refint] provides additional functions \texttt{incr},
\texttt{decr} and a few others, over integer references.
\subsection{Library \texttt{array}}
......@@ -23,22 +23,31 @@ particular the option \verb|-help| which displays the usage and options.
\item[\texttt{-L} $d$]
adds $d$ in the load path, to search for theories.
\item[\texttt{-{}-library} $d$]
same as \verb|-L|
\item[\texttt{-I} $d$]
same as \verb|-L| (deprecated)
\item[\texttt{-C} $file$]
reads configuration from $file$
\item[\texttt{-{}-config} $file$]
same as \verb|-C|
\item[\texttt{-{}-extra-config} $file$]
reads additional configuration from $file$
lists known debug flags
sets all debug flags (except flags which change the behavior)
\item[\texttt{-{}-debug} $flag$]
set a debug flag
print version information
......@@ -58,6 +67,8 @@ the command line tool \texttt{why3config}.
%%of the IDE.
This must be redone each time a new prover is installed.
\index{configuration file}
The provers which \why attempts to detect are described in
the readable configuration file \texttt{provers-detection-data.conf}
......@@ -78,6 +89,7 @@ versions of the same prover, or with different options.
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,
......@@ -86,6 +98,8 @@ The option \verb|--detect-provers| should be used to force
\why to detect again the available
provers and to replace them in the configuration file. The option
\verb|--detect-plugins| will do the same for plugins.
If a supported prover is installed under a name
that is not automatically recognized by \texttt{why3config},
......@@ -98,6 +112,8 @@ why3config --add-prover alt-ergo /home/me/bin/alt-ergo-trunc
As the first argument, one should put a prover
identification string. The list of known prover identifiers
can be obtained by the option \verb|--list-prover-ids|.
\section{The \texttt{why3} command-line tool}
......@@ -108,6 +124,7 @@ input file. By default, such a file must be written either in \why language
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:
......@@ -131,14 +148,25 @@ The \texttt{why3} tool executes the following steps:
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 \verb|-a/--apply-transform| in their order of appearance on the
command line. \verb|--list-transforms| list the known
transformations, plugins can add more of them.
\item Apply the driver selected with the \verb|-D/--driver| option,
or the driver of the prover selected with \verb|-P/--prover|
option. \verb|--list-provers| lists the known provers, \ie the ones
that appear in the configuration file.
\item If the option \verb|-P/--prover| is given, call the selected prover
on each generated task and print the results. If the option
\verb|-D/--driver| is given, print each generated task using
......@@ -183,6 +211,7 @@ Section~\ref{sec:gui}. There are no specific command-line options,
apart from the common options detailed in introduction to this chapter.
We describe the actions of the various menus and buttons of the
......@@ -461,6 +490,7 @@ stored in a \why session file, as the one produced by the IDE. Its
main goal is to play non-regression tests, \eg you can find in
\texttt{examples/} a script that runs regression tests on
all the examples.
The tool is invoked in a terminal or a script using
......@@ -14,12 +14,14 @@ Currently, realizations are supported for the proof assistants Coq and PVS.
Generating the skeleton for a theory is done by passing to \why the
\verb+--realize+ option, a driver suitable for realizations, the names of
the theories to realize, and a target directory.
why3 --realize -D path/to/drivers/prover-realize.drv
-T env_path.theory_name -o path/to/target/dir/
The name of the generated file is inferred from the theory name. If the
target directory already contains a file with the same name, \why
......@@ -128,7 +130,7 @@ option="--eval \"(setq coq-load-path (cons '(\\\"path/to/vo/files\\\" \
This configuration file can be passed to \why thanks to the
\verb+--extra-config+ option.
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment