Commit 3070b01d authored by Andrei Paskevich's avatar Andrei Paskevich

update the documentation for the last two commits

parent df714242
......@@ -21,7 +21,7 @@ module \texttt{Term} gives a few functions for building these. Here is
a piece of OCaml code for building the formula $true \lor false$.
\begin{verbatim}
(* opening the Why3 library *)
open Why
open Why3
(* a ground propositional goal: true or false *)
let fmla_true : Term.term = Term.t_true
......@@ -150,7 +150,7 @@ end
\section{Calling External Provers}
To call an external prover, we need to access the Why configuration
file \texttt{why.conf}, as it was build using the \texttt{why3config}
file \texttt{why3.conf}, as it was built using the \texttt{why3config}
command line tool or the \textsf{Detect Provers} menu of the graphical
IDE. The following API calls allow to access the content of this
configuration file.
......@@ -217,7 +217,7 @@ is the maximum allowed memory in megabytes. The type
\item \texttt{pr\_answer}: the prover answer, explained below;
\item \texttt{pr\_output}: the output of the prover, i.e. both
standard output and the standard error of the process
(a redirection in \texttt{why.conf} is required);
(a redirection in \texttt{why3.conf} is required);
\item \texttt{pr\_time} : the time taken by the prover, in seconds.
\end{itemize}
A \texttt{pr\_answer} is a sum of several kind of answers:
......
......@@ -101,8 +101,8 @@ 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
configuration file (\verb+~/.why3.conf+ or, in the case of local
installation, \verb+why3.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.
......@@ -353,7 +353,7 @@ generally a bench configuration file:
driver = "..."
command = "..."
loadpath = "..." #added to the one in why.conf
loadpath = "..." #added to the one in why3.conf
loadpath = "..."
timelimit = 30
......@@ -388,7 +388,7 @@ One can run all the bench given in one bench configuration file with
why3bench -B path_to_my_bench.rc
\end{verbatim}
\section{The \texttt{why.conf} configuration file}
\section{The \texttt{why3.conf} configuration file}
\label{sec:whyconffile}
One can use a custom configuration file. \texttt{why3config}
and other \texttt{why3} tools use priorities for which
......@@ -397,9 +397,9 @@ user's configuration file to consider:
\item the file specified by the \texttt{-C} or \texttt{-{}-config} options,
\item the file specified by the environment variable
\texttt{WHY3CONFIG} if set.
\item the file \texttt{\$HOME/.why.conf}
(\texttt{\$USERPROFILE/.why.conf} under Windows) or, in the case of
local installation, \texttt{why.conf} in Why3 sources top directory.
\item the file \texttt{\$HOME/.why3.conf}
(\texttt{\$USERPROFILE/.why3.conf} under Windows) or, in the case of
local installation, \texttt{why3.conf} in Why3 sources top directory.
\end{itemize}
If none of these files exists, a built-in default configuration is used.
......
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