Commit b0b70223 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Update documentation on Coq.

parent 3e11712e
......@@ -7,13 +7,13 @@ 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.
generated blocks 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.
required by the driver file. Any user-made changes to this block
will be lost when the file is regenerated by \why. This part
starts with \verb+(* This file is generated by ... *)+.
\item Abstract logic symbols are assumed with the vernacular directive
\verb+Parameter+. Axioms are assumed with the \verb+Axiom+
directive. When regenerating a script, \why assumes that all such
......@@ -23,20 +23,26 @@ generated parts or adding empty lines inside them.
\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
that the definition is a user-defined block.
\item 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+
predefined 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}
\why preserves any block from the script that does not fall into one of
the previous categories. Such blocks can be used to import other
libraries than the ones from the prelude. They can also be used to state
and prove auxiliary lemmas. \why tries to preserve the position of these
user-defined blocks relatively to the generated ones.
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
......
......@@ -2,10 +2,11 @@
\label{sec:coqtactic}
\why provides a Coq tactic to call external theorem provers as oracles.
This tactic is deprecated and might be removed in future versions of \why.
\subsubsection{Installation}
You need Coq version 8.4 or greater. If this is the case, \why's
You need Coq version 8.5 or greater. If this is the case, \why's
configuration detects it, then compiles and installs the Coq tactic.
The Coq tactic is installed in
\begin{center}
......@@ -16,12 +17,8 @@ by \verb+why3 --print-libdir+. This directory
is automatically added to Coq's load path if you are
calling Coq via \why (from \texttt{why3 ide}, \texttt{why3 replay},
etc.). If you are calling Coq by yourself, you need to add
this directory to Coq's load path, either using Coq's command line
option \texttt{-I} or by adding
\begin{center}
\verb+Add LoadPath "+\textit{why3-lib-dir}\verb+/coq-tactic/".+
\end{center}
to your \texttt{\~{}/.coqrc} resource file.
this directory to Coq's load path using Coq's command line
options \texttt{-I} and \texttt{-R}.
\subsubsection{Usage}
......@@ -34,8 +31,8 @@ The string \textit{prover-name} identifies one of the automated theorem provers
supported by \why, as reported by \verb+why3 --list-provers+
(interactive provers excluded).
\index{list-provers@\verb+--list-provers+}
The current goal is then translated to \why's logic and the prover is
called. If it reports the goal to be valid, then Coq's \texttt{admit}
The tactics translates the current goal to \why's logic and then calls the prover.
If it reports the goal to be valid, then Coq's \texttt{admit}
tactic is used to assume the goal. The prover is called with a time
limit in seconds as given by \why's configuration file
(see Section~\ref{sec:whyconffile}). A different value may be given
......
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