Commit 62fe72b6 authored by MARCHE Claude's avatar MARCHE Claude

doc: fix makefile, labels, index

parent 5e18f8df
...@@ -1464,9 +1464,9 @@ doc/bnf: doc/bnf.mll ...@@ -1464,9 +1464,9 @@ doc/bnf: doc/bnf.mll
$(OCAMLLEX) $< $(OCAMLLEX) $<
$(OCAMLOPT) -o $@ doc/bnf.ml $(OCAMLOPT) -o $@ doc/bnf.ml
DOC = api glossary ide intro library macros manpages install coq_tactic \ DOC = api glossary ide intro library macros manpages install \
realizations manual starting syntax syntaxref technical version whyml \ manual starting syntax syntaxref technical version whyml \
pvs itp pvs coq coq_tactic isabelle
DOCTEX = $(addprefix doc/, $(addsuffix .tex, $(DOC))) DOCTEX = $(addprefix doc/, $(addsuffix .tex, $(DOC)))
......
\subsection{Coq} \section{Coq}
\label{sec:coq} \label{sec:coq}
\index{Coq proof assistant}
This section describes the content of the Coq files generated by \why for This section describes the content of the Coq files generated by \why for
both proof obligations and theory realizations. When reading a Coq both proof obligations and theory realizations. When reading a Coq
...@@ -40,3 +41,10 @@ Currently, the parser for Coq scripts is rather naive and does not know ...@@ -40,3 +41,10 @@ Currently, the parser for Coq scripts is rather naive and does not know
much about comments. For instance, \why can easily be confused by much about comments. For instance, \why can easily be confused by
some terminating directive like \verb+Qed+ that would be present in a some terminating directive like \verb+Qed+ that would be present in a
comment. comment.
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End:
\chapter{Coq Tactic} \subsection{Coq Tactic}
\label{chap:tactic} \label{sec:coqtactic}
\index{Coq proof assistant}
\why\ provides a Coq tactic to call external theorem provers as oracles. \why\ provides a Coq tactic to call external theorem provers as oracles.
\section{Installation} \subsubsection{Installation}
You need Coq version 8.3 or greater. If this is the case, \why's You need Coq version 8.3 or greater. If this is the case, \why's
configuration detects it, then compiles and installs the Coq tactic. configuration detects it, then compiles and installs the Coq tactic.
...@@ -24,7 +23,7 @@ option \texttt{-I} or by adding ...@@ -24,7 +23,7 @@ option \texttt{-I} or by adding
\end{center} \end{center}
to your \texttt{\~{}/.coqrc} resource file. to your \texttt{\~{}/.coqrc} resource file.
\section{Usage} \subsubsection{Usage}
The Coq tactic is called \texttt{why3} and is used as follows: The Coq tactic is called \texttt{why3} and is used as follows:
\begin{center} \begin{center}
...@@ -41,7 +40,7 @@ limit in seconds as given by \why's configuration file ...@@ -41,7 +40,7 @@ limit in seconds as given by \why's configuration file
(see page~\pageref{sec:whyconffile}). A different value may be given (see page~\pageref{sec:whyconffile}). A different value may be given
using the \texttt{timelimit} keyword. using the \texttt{timelimit} keyword.
\paragraph{Error messages.} The following errors may be reported by \subsubsection{Error messages.} The following errors may be reported by
the Coq tactic. the Coq tactic.
\begin{description} \begin{description}
\item[\texttt{Not a first order goal}]\emptyitem \item[\texttt{Not a first order goal}]\emptyitem
......
...@@ -53,13 +53,14 @@ It is also installable from sources, available from the site ...@@ -53,13 +53,14 @@ It is also installable from sources, available from the site
\end{itemize} \end{itemize}
If you want to use the specific Coq features, \ie the Coq If you want to use the specific Coq features, \ie the Coq tactic
tactic~\ref{chap:tactic} and Coq realizations~\ref{sec:realizations}, (Section~\ref{sec:coqtactic}) and Coq realizations
then Coq has to be installed before \why. Look at the summary printed (Section~\ref{sec:realizations}), then Coq has to be installed before
at the end of the configuration script to check if Coq has been \why. Look at the summary printed at the end of the configuration
detected properly. Similarly, for using PVS or Isabelle to discharge proofs, PVS script to check if Coq has been detected properly. Similarly, for
and Isabelle must be installed before \why. You should check that using PVS (Section~\ref{sec:pvs}) or Isabelle (Section~\ref{sec:isabelle}) to discharge proofs, PVS and Isabelle must be
those proof assistants are correctly detected by the configure script. installed before \why. You should check that those proof assistants
are correctly detected by the configure script.
When configuration is finished, you can compile \why. When configuration is finished, you can compile \why.
\begin{verbatim} \begin{verbatim}
...@@ -71,7 +72,7 @@ make install ...@@ -71,7 +72,7 @@ make install
\end{verbatim} \end{verbatim}
Installation can be tested as follows: Installation can be tested as follows:
\begin{enumerate} \begin{enumerate}
\item install some external provers (see~Section\ref{provers} below) \item install some external provers (see~Section~\ref{provers} below)
\item run \verb|why3config --detect| \item run \verb|why3config --detect|
\item run some examples from the distribution, \eg you should \item run some examples from the distribution, \eg you should
obtain the following: obtain the following:
......
\subsection{Isabelle/HOL} \section{Isabelle/HOL}
\label{sec:isabelle}
\todo{Explain Isabelle/jedit server interaction} \index{Isabelle proof assistant}
\subsection{Installation}
You need version Isabelle2013-2.
\todo{put ... in ... etc/components}
\subsection{Usage}
\todo{Explain Isabelle/jedit server interaction}
When using Isabelle, files generated from Why3 theories are stored in When using Isabelle, files generated from Why3 theories are stored in
a dedicated XML format. Those files should not be edited. Instead, a dedicated XML format. Those files should not be edited. Instead,
realizations must be designed in some \texttt{.thy} as follows. See realizations must be designed in some \texttt{.thy} as follows.
directory \url{lib/isabelle} for examples.
\subsection{Realizations}
The realization file corresponding to some Why3 file \url{f.why} The realization file corresponding to some Why3 file \url{f.why}
should have the following form. should have the following form.
...@@ -29,3 +40,12 @@ why3_vc <some other lemma> by proof ...@@ -29,3 +40,12 @@ why3_vc <some other lemma> by proof
why3_end why3_end
\end{verbatim} \end{verbatim}
See directory \url{lib/isabelle} for examples.
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End:
...@@ -5,6 +5,8 @@ ...@@ -5,6 +5,8 @@
\todo{expliquer les principes} \todo{expliquer les principes}
... We then provide specific information about some ITPs.
\section{Theory Realizations} \section{Theory Realizations}
\label{sec:realizations} \label{sec:realizations}
...@@ -99,11 +101,10 @@ This configuration file can be passed to \why thanks to the ...@@ -99,11 +101,10 @@ This configuration file can be passed to \why thanks to the
\index{driver@\verb+driver+} \index{driver@\verb+driver+}
\section{Specific Information about some ITPs}
\input{./coq.tex} \input{./coq.tex}
\input{./coq_tactic.tex}
\input{./isabelle.tex} \input{./isabelle.tex}
\input{./pvs.tex} \input{./pvs.tex}
......
...@@ -239,7 +239,6 @@ Thi-Minh-Tuyen Nguyen, Asma Tafat, Piotr Trojanek. ...@@ -239,7 +239,6 @@ Thi-Minh-Tuyen Nguyen, Asma Tafat, Piotr Trojanek.
\input{itp.tex} \input{itp.tex}
\input{coq_tactic.tex}
% \chapter{Complete API documentation} *) % \chapter{Complete API documentation} *)
% \label{chap:apidoc} *) % \label{chap:apidoc} *)
......
\subsection{PVS} \section{PVS}
\label{sec:pvs}
\index{PVS proof assistant}
\subsection{Installation}
You need version 6.0.
\subsection{Usage}
When a PVS file is regenerated, the old version is split into chunks, When a PVS file is regenerated, the old version is split into chunks,
according to blank lines. Chunks corresponding to \why declarations according to blank lines. Chunks corresponding to \why declarations
...@@ -13,6 +22,8 @@ otherwise, there will be two ...@@ -13,6 +22,8 @@ otherwise, there will be two
declarations for \texttt{f} in the next version of the file (one being declarations for \texttt{f} in the next version of the file (one being
regenerated and another one considered to be a user-edited chunk). regenerated and another one considered to be a user-edited chunk).
\subsection{Realization}
The user is allowed to perform the following actions on a PVS The user is allowed to perform the following actions on a PVS
realization: realization:
\begin{itemize} \begin{itemize}
...@@ -36,3 +47,10 @@ realization: ...@@ -36,3 +47,10 @@ realization:
\why makes some effort to merge new declarations with old ones \why makes some effort to merge new declarations with old ones
and with user chunks. If it happens that some chunks could not be and with user chunks. If it happens that some chunks could not be
merged, they are appended at the end of the file, in comments. merged, they are appended at the end of the file, in comments.
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End:
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