updated documentation for 0.64

parent 614c6a53
...@@ -3,9 +3,9 @@ ...@@ -3,9 +3,9 @@
| formula "->" formula ; implication | formula "->" formula ; implication
| formula "<->" formula ; equivalence | formula "<->" formula ; equivalence
| formula "and" formula ; conjunction | formula "and" formula ; conjunction
| formula "/\" formula ; asymmetric conjunction | formula "&&" formula ; asymmetric conjunction
| formula "or" formula ; disjunction | formula "or" formula ; disjunction
| formula "\/" formula ; asymmetric disjunction | formula "||" formula ; asymmetric disjunction
| "not" formula ; negation | "not" formula ; negation
| lqualid ; symbol | lqualid ; symbol
| prefix-op term ; | prefix-op term ;
......
...@@ -4,7 +4,8 @@ ...@@ -4,7 +4,8 @@
We provide here a short description of logic symbols defined in the We provide here a short description of logic symbols defined in the
standard library. Only the most general-purpose ones are standard library. Only the most general-purpose ones are
described. For more details, one should directly read the described. For more details, one should directly read the
corresponding file, or alternatively, use the \verb|why3| with option \verb|-T| and a qualified theory name, \eg corresponding file, or alternatively, use the \verb|why3| with option
\verb|-T| and a qualified theory name, for example:
\begin{verbatim} \begin{verbatim}
> why3 -T bool.Ite > why3 -T bool.Ite
theory Ite theory Ite
......
...@@ -99,9 +99,10 @@ file to add support for detection of other provers. (In that case, ...@@ -99,9 +99,10 @@ file to add support for detection of other provers. (In that case,
please consider submitting a new prover configuration on the bug please consider submitting a new prover configuration on the bug
tracking system). tracking system).
The result of the prover detection is stored in the user's The result of provers detection is stored in the user's
configuration file (\eg{} \verb+~/.why.conf+). Again, this file configuration file (\verb+~/.why.conf+ or, in the case of local
is human-readable, and advanced users may modify it in order to 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 experiment with different ways of calling provers, \eg{} different
versions of the same prover, or with different options. versions of the same prover, or with different options.
...@@ -356,14 +357,14 @@ generally a bench configuration file: ...@@ -356,14 +357,14 @@ generally a bench configuration file:
csv = "prgbench.csv" csv = "prgbench.csv"
\end{verbatim} \end{verbatim}
Such a file can defined three families \texttt{tools,probs,bench}. The Such a file can define three families \texttt{tools,probs,bench}. The
sections \texttt{tools} define a set of components to compare, the sections \texttt{tools} define a set of components to compare, the
sections \texttt{probs} define a set of goals on which to compare some sections \texttt{probs} define a set of goals on which to compare some
components and the sections \texttt{bench} define which components to components and the sections \texttt{bench} define which components to
compare using which goals. It refers by name to the sections compare using which goals. It refers by name to the sections
\texttt{tools} and \texttt{probs} defined in the same file. The order \texttt{tools} and \texttt{probs} defined in the same file. The order
of the definitions is irrelevant. Notice that \texttt{loadpath} in a family of the definitions is irrelevant. Notice that \texttt{loadpath} in a family
\texttt{tools} can be used to compare different axiomatisation. \texttt{tools} can be used to compare different axiomatizations.
One can run all the bench given in one bench configuration file with One can run all the bench given in one bench configuration file with
\texttt{why3bench} : \texttt{why3bench} :
...@@ -373,30 +374,27 @@ why3bench -B path_to_my_bench.rc ...@@ -373,30 +374,27 @@ why3bench -B path_to_my_bench.rc
\section{The \texttt{why.conf} configuration file} \section{The \texttt{why.conf} configuration file}
\label{sec:whyconffile} \label{sec:whyconffile}
One can defined more than one configuration file. \texttt{why3config} One can use a custom configuration file. \texttt{why3config}
and all the others \texttt{why3}'s tools use priorities for which and other \texttt{why3} tools use priorities for which
user's configuration file to consider: user's configuration file to consider:
\begin{itemize} \begin{itemize}
\item the file specified by the \texttt{-C} or \texttt{--config} options, \item the file specified by the \texttt{-C} or \texttt{-{}-config} options,
\item the file specified by the environment variable \item the file specified by the environment variable
\texttt{\$WHY\_CONFIG} if set. \texttt{WHY3CONFIG} if set.
\item the file \texttt{why.conf} or \texttt{.why.conf} in the current \item the file \texttt{\$HOME/.why.conf}
directory. (\texttt{\$USERPROFILE/.why.conf} under Windows) or, in the case of
\item the file \texttt{\$HOME/.why.conf} or \texttt{\$USERPROFILE/.why.conf} local installation, \texttt{why.conf} in Why3 sources top directory.
\end{itemize} \end{itemize}
If none of this file exists a built-in default configuration is used If none of these files 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 The configuration file is a human-readable text file, which consists
composed by association pairs arranged by sections. Here an example of of association pairs arranged in sections. Here follows an example of
a configuration file. configuration file.
\begin{verbatim} \begin{verbatim}
[main ] [main ]
datadir = "/usr/local/share/why3"
libdir = "/usr/local/lib/why3"
loadpath = "/usr/local/share/why3/theories" loadpath = "/usr/local/share/why3/theories"
magic = 2
memlimit = 0 memlimit = 0
running_provers_max = 2 running_provers_max = 2
timelimit = 10 timelimit = 10
...@@ -424,19 +422,19 @@ name = "Alt-Ergo" ...@@ -424,19 +422,19 @@ name = "Alt-Ergo"
version = "0.91" version = "0.91"
\end{verbatim} \end{verbatim}
A section begin with an header inside square brackets and end at the A section begins with a header inside square brackets and ends at the
next square brackets. Sections can't be nested. The header of a beginning of the next section. The header of a
section can be only one identifier, \texttt{main} and \texttt{ide} in 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 the example, or it can be composed by a family name and one family
argument, \texttt{prover} is one family name, \texttt{coq} and argument, \texttt{prover} is one family name, \texttt{coq} and
\texttt{alt-ergo} are the family argument. \texttt{alt-ergo} are the family argument.
Inside a section, one key can be associated to an integer (.eg -555), Inside a section, one key can be associated with an integer (.eg -555),
a boolean (true, false) or a string (\eg{} "emacs"). One key can appear 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 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. the keys inside a section matter only for the multi-value key.
\section{Drivers of external provers} \section{Drivers of External Provers}
\label{sec:drivers} \label{sec:drivers}
The drivers of external provers are readable files, in directory The drivers of external provers are readable files, in directory
......
...@@ -128,7 +128,7 @@ Section~\ref{sec:ideref} for details on how to configure this). You get ...@@ -128,7 +128,7 @@ Section~\ref{sec:ideref} for details on how to configure this). You get
now a regular Coq file fo fill in, as shown on Figure~\ref{fig:coqide}. now a regular Coq file fo fill in, as shown on Figure~\ref{fig:coqide}.
Please take care of the comments of this file. Only the part between Please take care of the comments of this file. Only the part between
the two last comments can be modified. Moreover, these comments the two last comments can be modified. Moreover, these comments
themselves should not be modified at all, they are use to mark the themselves should not be modified at all, they are used to mark the
part you modify, in order to regenerate the file if the goal is part you modify, in order to regenerate the file if the goal is
changed. changed.
......
...@@ -98,8 +98,8 @@ associativities, from lowest to greatest priority: ...@@ -98,8 +98,8 @@ associativities, from lowest to greatest priority:
\texttt{if then else} / \texttt{let in} & -- \\ \texttt{if then else} / \texttt{let in} & -- \\
label & -- \\ label & -- \\
\texttt{->} / \texttt{<->} & right \\ \texttt{->} / \texttt{<->} & right \\
\texttt{or} / \verb!\/! & right \\ \texttt{or} / \verb!||! & right \\
\texttt{and} / \verb!/\! & right \\ \texttt{and} / \verb!&&! & right \\
\texttt{not} & -- \\ \texttt{not} & -- \\
infix level 1 & left \\ infix level 1 & left \\
infix level 2 & left \\ infix level 2 & left \\
...@@ -119,11 +119,11 @@ disequality (\texttt{<>}). ...@@ -119,11 +119,11 @@ disequality (\texttt{<>}).
\end{figure} \end{figure}
Notice that there are two symbols for the conjunction: \texttt{and} Notice that there are two symbols for the conjunction: \texttt{and}
and \verb|/\|, and similarly for disjunction. There are logically and \verb|&&|, and similarly for disjunction. There are logically
equivalent, but may be treated slightly differently by some equivalent, but may be treated slightly differently by some
transformation, \eg{} the \texttt{split} transformation transforms transformation, \eg{} the \texttt{split} transformation transforms
$A~\texttt{and}~B$ into subgoals $A$ and $B$, whereas it transforms $A~\texttt{and}~B$ into subgoals $A$ and $B$, whereas it transforms
$A~\verb|/\|~B$ into subgoals $A$ and $A\rightarrow B$. $A~\verb|&&|~B$ into subgoals $A$ and $A\rightarrow B$.
\paragraph{Theories.} \paragraph{Theories.}
The syntax for theories is given Figure~\ref{fig:bnf:theory}. The syntax for theories is given Figure~\ref{fig:bnf:theory}.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment