diff options
author | 2017-07-27 15:17:21 +0200 | |
---|---|---|
committer | 2017-07-27 15:24:47 +0200 | |
commit | ce3ed09acebe048f1a361ed6440a520b166a13b8 (patch) | |
tree | 18f394d16698b8a051dfe9a050de990515d80ede | |
parent | bd1a0abf49fe67e7f02dc562d4b81d27ed6f606c (diff) |
Extraction TestCompile documented + mentionned in CHANGES
Also includes a minor fix of the Extraction doc (a Require was missing).
-rw-r--r-- | CHANGES | 2 | ||||
-rw-r--r-- | doc/refman/Extraction.tex | 28 |
2 files changed, 24 insertions, 6 deletions
@@ -75,6 +75,8 @@ Standard Library Plugins - The mathematical proof language (also known as declarative mode) was removed. +- A new command Extraction TestCompile has been introduced, not meant + for the general user but instead for Coq's test-suite. Dependencies diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index fa3d61b1c..5d7ec66fa 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -21,9 +21,14 @@ be used (abusively) to refer to any of the three. Before using any of the commands or options described in this chapter, the extraction framework should first be loaded explicitly -via {\tt Require Extraction}. Note that in earlier versions of Coq, these -commands and options were directly available without any preliminary -{\tt Require}. +via {\tt Require Extraction}, or via the more robust +{\tt Require Coq.extraction.Extraction}. +Note that in earlier versions of Coq, these commands and options were +directly available without any preliminary {\tt Require}. + +\begin{coq_example} +Require Extraction. +\end{coq_example} \asection{Generating ML code} \comindex{Extraction} @@ -82,9 +87,20 @@ one monolithic file or one file per \Coq\ library. using prefixes \verb!coq_! or \verb!Coq_!. \end{description} -\noindent The list of globals \qualid$_i$ does not need to be -exhaustive: it is automatically completed into a complete and minimal -environment. +\noindent The following command is meant to help automatic testing of + the extraction, see for instance the {\tt test-suite} directory + in the \Coq\ sources. + +\begin{description} +\item {\tt Extraction TestCompile} \qualid$_1$ \dots\ \qualid$_n$. ~\par + All the globals (or modules) \qualid$_1$ \dots\ \qualid$_n$ and all + their dependencies are extracted to a temporary Ocaml file, just as in + {\tt Extraction "{\em file}"}. Then this temporary file and its + signature are compiled with the same Ocaml compiler used to built + \Coq. This command succeeds only if the extraction and the Ocaml + compilation succeed (and it fails if the current target language + of the extraction is not Ocaml). +\end{description} \asection{Extraction options} |