Commit a1761713 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Update doc according to new implementation of upgrades policies

parent 68a3301c
...@@ -119,7 +119,7 @@ Section~\ref{sec:why3config}. ...@@ -119,7 +119,7 @@ Section~\ref{sec:why3config}.
\section{Multiple Versions of the Same Prover} \section{Multiple Versions of the Same Prover}
Since version 0.72, \why is able to several versions of the same Since version 0.72, \why is able to use several versions of the same
prover, e.g. it can use both CVC3 2.2 and CVC3 2.4.1 at the same time. prover, e.g. it can use both CVC3 2.2 and CVC3 2.4.1 at the same time.
The automatic detection of provers looks for typical names for their The automatic detection of provers looks for typical names for their
executable command, e.g. \texttt{cvc3} for CVC3. However, if you executable command, e.g. \texttt{cvc3} for CVC3. However, if you
...@@ -129,11 +129,12 @@ use specialized executable names, such as \texttt{cvc3-2.2} or ...@@ -129,11 +129,12 @@ use specialized executable names, such as \texttt{cvc3-2.2} or
these, you can use the option \verb|--add-prover| to these, you can use the option \verb|--add-prover| to
\texttt{why3config}, e.g. \texttt{why3config}, e.g.
\begin{verbatim} \begin{verbatim}
why3config --detect --add-prover cvc3-2.4:/usr/local/bin/cvc3-2.4.1 why3config --detect --add-prover cvc3-2.4 /usr/local/bin/cvc3-2.4.1
\end{verbatim} \end{verbatim}
the first argument (here \verb|cvc3-2.4|) must be one of the class of the first argument (here \verb|cvc3-2.4|) must be one of the class of
provers known in the file \verb|provers-detection-data.conf| typically provers known in the file \verb|provers-detection-data.conf| typically
located in \verb|/usr/local/share/why3| after installation. located in \verb|/usr/local/share/why3| after installation. See
Appendix~\ref{sec:proverdetecttiondata} for details.
\section{Session Update after Prover Upgrade} \section{Session Update after Prover Upgrade}
......
...@@ -232,13 +232,15 @@ are the following. ...@@ -232,13 +232,15 @@ are the following.
\input{coq_tactic.tex} \input{coq_tactic.tex}
\input{technical.tex}
% \chapter{Complete API documentation} *) % \chapter{Complete API documentation} *)
% \label{chap:apidoc} *) % \label{chap:apidoc} *)
% \input{./apidoc.tex} *) % \input{./apidoc.tex} *)
% \appendix
\input{technical.tex}
\bibliographystyle{abbrv} \bibliographystyle{abbrv}
\bibliography{manual} \bibliography{manual}
%\input{biblio-demons} %\input{biblio-demons}
......
...@@ -10,7 +10,15 @@ The XML file follows the DTD given in \texttt{share/why3session.dtd} and reprodu ...@@ -10,7 +10,15 @@ The XML file follows the DTD given in \texttt{share/why3session.dtd} and reprodu
\verbatiminput{../share/why3session.dtd} \verbatiminput{../share/why3session.dtd}
\section{Provers detection data}
\label{sec:proverdetecttiondata}
All the necessary data configuration for the autoamtic detection of
installed provers is stored in the file
\texttt{provers-detection-data.conf} typically located in directory
\verb|/usr/local/share/why3| after installation. The contents of this
file is reproduced below.
\verbatiminput{../share/provers-detection-data.conf}
\section{The \texttt{why3.conf} configuration file} \section{The \texttt{why3.conf} configuration file}
\label{sec:whyconffile} \label{sec:whyconffile}
......
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