Commit 5e18f8df authored by MARCHE Claude's avatar MARCHE Claude

reorganized doc concerning ITPs

parent 04667fdc
\subsection{Coq}
\label{sec:coq}
This section describes the content of the Coq files generated by \why for
both proof obligations and theory realizations. When reading a Coq
script, \why is guided by the presence of empty lines to split the
script, so the user should refrain from removing empty lines around
generated parts or adding empty lines inside them.
\begin{enumerate}
\item The header of the file contains all the library inclusions
required by the driver file. Any user-made changes to this part
will be lost when the file is regenerated by \why. This part ends
at the first empty line.
\item Abstract logic symbols are assumed with the vernacular directive
\verb+Paramater+. Axioms are assumed with the \verb+Axiom+
directive. When regenerating a script, \why assumes that all such
symbols have been generated by a previous run. As a consequence,
the user should not introduce new symbols with these two
directives, as they would be lost.
\item Definitions of functions and inductive types in theories are
printed in a block that starts with \verb+(* Why3 assumption *)+.
This comment should not be removed; otherwise \why will assume
that the definition is user-made.
\item Finally, proof obligations and symbols to be realized are
introduced by \verb+(* Why3 goal *)+. The user is supposed to
fill the script after the statement. \why assumes that the
user-made part extends up to \verb+Qed+, \verb+Admitted+,
\verb+Save+, or \verb+Defined+, whichever comes first. In the
case of definitions, the original statement can be replaced by
a \verb+Notation+ directive, in order to ease the usage of
already defined symbols. \why also recognizes \verb+Variable+
and \verb+Hypothesis+ and preserves them; they should be used in
conjunction with Coq's \verb+Section+ mechanism to realize
theories that still need some abstract symbols and axioms.
\end{enumerate}
Currently, the parser for Coq scripts is rather naive and does not know
much about comments. For instance, \why can easily be confused by
some terminating directive like \verb+Qed+ that would be present in a
comment.
......@@ -52,11 +52,14 @@ It is also installable from sources, available from the site
\url{http://ocaml.info/home/ocaml_sources.html#ocaml-sqlite3}
\end{itemize}
If you want to use the specific Coq features, \ie the Coq
tactic~\ref{chap:tactic} and Coq realizations~\ref{chap:realizations},
tactic~\ref{chap:tactic} and Coq realizations~\ref{sec:realizations},
then Coq has to be installed before \why. Look at the summary printed
at the end of the configuration script to check if Coq has been
detected properly.
detected properly. Similarly, for using PVS or Isabelle to discharge proofs, PVS
and Isabelle must be 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.
\begin{verbatim}
......
\subsection{Isabelle/HOL}
\todo{Explain Isabelle/jedit server interaction}
When using Isabelle, files generated from Why3 theories are stored in
a dedicated XML format. Those files should not be edited. Instead,
realizations must be designed in some \texttt{.thy} as follows. See
......
\chapter{Theory Realizations}
\label{chap:realizations}
\chapter{Interactive Proof Assistants}
\section{On using an interactive proof assistant from Why3}
\todo{expliquer les principes}
\section{Theory Realizations}
\label{sec:realizations}
Given a \why theory, one can use a proof assistant to make a
\emph{realization} of this theory, that is to provide definitions for
......@@ -9,7 +16,7 @@ theory and/or make a connection to an existing library (of the proof
assistant) to ease some proofs.
Currently, realizations are supported for the proof assistants Coq and PVS.
\section{Generating a realization}
\subsection{Generating a realization}
Generating the skeleton for a theory is done by passing to \why the
\verb+--realize+ option, a driver suitable for realizations, the names of
......@@ -34,7 +41,7 @@ theory is modified.
It is up to the user to handle such dependencies, for instance using a
\texttt{Makefile}.
\section{Using realizations inside proofs}
\subsection{Using realizations inside proofs}
If a theory has been realized, the \why printer for the corresponding prover
will no longer output declarations for that theory but instead simply put
......@@ -55,55 +62,7 @@ scripts to point to the realization, in case the default name is not
suitable for the interactive prover.
\index{realized_theory@\verb+realized_theory+}
\section{Generated/edited files}
\label{sec:edited-files}
\subsection{Coq}
This section describes the content of the Coq files generated by \why for
both proof obligations and theory realizations. When reading a Coq
script, \why is guided by the presence of empty lines to split the
script, so the user should refrain from removing empty lines around
generated parts or adding empty lines inside them.
\begin{enumerate}
\item The header of the file contains all the library inclusions
required by the driver file. Any user-made changes to this part
will be lost when the file is regenerated by \why. This part ends
at the first empty line.
\item Abstract logic symbols are assumed with the vernacular directive
\verb+Paramater+. Axioms are assumed with the \verb+Axiom+
directive. When regenerating a script, \why assumes that all such
symbols have been generated by a previous run. As a consequence,
the user should not introduce new symbols with these two
directives, as they would be lost.
\item Definitions of functions and inductive types in theories are
printed in a block that starts with \verb+(* Why3 assumption *)+.
This comment should not be removed; otherwise \why will assume
that the definition is user-made.
\item Finally, proof obligations and symbols to be realized are
introduced by \verb+(* Why3 goal *)+. The user is supposed to
fill the script after the statement. \why assumes that the
user-made part extends up to \verb+Qed+, \verb+Admitted+,
\verb+Save+, or \verb+Defined+, whichever comes first. In the
case of definitions, the original statement can be replaced by
a \verb+Notation+ directive, in order to ease the usage of
already defined symbols. \why also recognizes \verb+Variable+
and \verb+Hypothesis+ and preserves them; they should be used in
conjunction with Coq's \verb+Section+ mechanism to realize
theories that still need some abstract symbols and axioms.
\end{enumerate}
Currently, the parser for Coq scripts is rather naive and does not know
much about comments. For instance, \why can easily be confused by
some terminating directive like \verb+Qed+ that would be present in a
comment.
\input{./pvs.tex}
\input{./isabelle.tex}
\section{Shipping libraries of realizations}
\subsection{Shipping libraries of realizations}
While modifying an existing driver file might be sufficient for local
use, it does not scale well when the realizations are to be shipped to
......@@ -140,6 +99,16 @@ This configuration file can be passed to \why thanks to the
\index{driver@\verb+driver+}
\section{Specific Information about some ITPs}
\input{./coq.tex}
\input{./isabelle.tex}
\input{./pvs.tex}
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
......
% \newcommand{\todo}[1]{{\Huge\bfseries TODO: #1}}
\newcommand{\todo}[1]{{\Huge\bfseries TODO: #1}}
\newcommand{\why}{\textsf{Why3}\xspace}
\newcommand{\whyml}{\textsf{WhyML}\xspace}
......
......@@ -237,7 +237,7 @@ Thi-Minh-Tuyen Nguyen, Asma Tafat, Piotr Trojanek.
\input{library.tex}
\input{realizations.tex}
\input{itp.tex}
\input{coq_tactic.tex}
......
......@@ -138,7 +138,7 @@ now a regular Coq file to fill in, as shown on Figure~\ref{fig:coqide}.
Please be mindful of the comments of this file. They indicate where \why
expects you to fill the blanks. Note that the comments themselves should
not be removed, as they are needed to properly regenerate the file when the
goal is changed. See Section~\ref{sec:edited-files} for more details.
goal is changed. See Section~\ref{sec:coq} for more details.
\begin{figure}[tbp]
%HEVEA\centering
......
......@@ -971,7 +971,7 @@ let print_logic_result fmt r =
x.xs_name.Ident.id_string print_value v
| Irred e ->
fprintf fmt "@[Cannot execute expression@ @[%a@]@]"
p_expr e
Mlw_pretty.print_expr (* p_expr *) e
| Fun _ ->
fprintf fmt "@[Result is a function@]"
......
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