diff options
| -rw-r--r-- | Makefile.doc | 3 | ||||
| -rw-r--r-- | doc/refman/RefMan-uti.tex | 482 | ||||
| -rw-r--r-- | doc/refman/Reference-Manual.tex | 6 | ||||
| -rw-r--r-- | doc/refman/coqdoc.tex | 573 | ||||
| -rw-r--r-- | doc/sphinx/index.rst | 1 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 999 |
6 files changed, 1001 insertions, 1063 deletions
diff --git a/Makefile.doc b/Makefile.doc index a8b5376a6..c2471462c 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -62,8 +62,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ Universes.v.tex) REFMANTEXFILES:=$(addprefix doc/refman/, \ - headers.sty Reference-Manual.tex \ - RefMan-uti.tex) \ + headers.sty Reference-Manual.tex) \ $(REFMANCOQTEXFILES) \ REFMANEPSFILES:=doc/refman/coqide.eps doc/refman/coqide-queries.eps diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex deleted file mode 100644 index 962aa98b6..000000000 --- a/doc/refman/RefMan-uti.tex +++ /dev/null @@ -1,482 +0,0 @@ -\chapter[Utilities]{Utilities\label{Utilities}} -%HEVEA\cutname{tools.html} - -The distribution provides utilities to simplify some tedious works -beside proof development, tactics writing or documentation. - -\section[Using Coq as a library]{Using Coq as a library} - -In previous versions, \texttt{coqmktop} was used to build custom -toplevels --- for example for better debugging or custom static -linking. Nowadays, the preferred method is to use \texttt{ocamlfind}. - -The most basic custom toplevel is built using: -\begin{quotation} -\texttt{\% ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg - -package coq.toplevel toplevel/coqtop\_bin.ml -o my\_toplevel.native} -\end{quotation} - -For example, to statically link LTAC, you can just do: -\begin{quotation} -\texttt{\% ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg - -package coq.toplevel -package coq.ltac toplevel/coqtop\_bin.ml -o my\_toplevel.native} -\end{quotation} -and similarly for other plugins. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\section[Building a \Coq\ project with {\tt coq\_makefile}] -{Building a \Coq\ project with {\tt coq\_makefile} -\label{Makefile} -\ttindex{Makefile} -\ttindex{coq\_Makefile} -\ttindex{\_CoqProject}} - -The majority of \Coq\ projects are very similar: a collection of {\tt .v} -files and eventually some {\tt .ml} ones (a \Coq\ plugin). The main piece -of metadata needed in order to build the project are the command -line options to {\tt coqc} (e.g. {\tt -R, -I}, -\SeeAlso Section~\ref{coqoptions}). Collecting the list of files and -options is the job of the {\tt \_CoqProject} file. - -A simple example of a {\tt \_CoqProject} file follows: - -\begin{verbatim} --R theories/ MyCode -theories/foo.v -theories/bar.v --I src/ -src/baz.ml4 -src/bazaux.ml -src/qux_plugin.mlpack -\end{verbatim} - -Currently, both \CoqIDE{} and Proof General (version $\geq$ 4.3pre) understand -{\tt \_CoqProject} files and invoke \Coq\ with the desired options. - -The {\tt coq\_makefile} utility can be used to set up a build infrastructure -for the \Coq\ project based on makefiles. The recommended way of -invoking {\tt coq\_makefile} is the following one: - -\begin{verbatim} -coq_makefile -f _CoqProject -o CoqMakefile -\end{verbatim} - -Such command generates the following files: -\begin{description} - \item[{\tt CoqMakefile}] is a generic makefile for GNU Make that provides targets to build the project (both {\tt .v} and {\tt .ml*} files), to install it system-wide in the {\tt coq-contrib} directory (i.e. where \Coq\ is installed) as well as to invoke {\tt coqdoc} to generate html documentation. - - \item[{\tt CoqMakefile.conf}] contains make variables assignments that reflect the contents of the {\tt \_CoqProject} file as well as the path relevant to \Coq{}. -\end{description} - -An optional file {\bf {\tt CoqMakefile.local}} can be provided by the user in order to extend {\tt CoqMakefile}. In particular one can declare custom actions to be performed before or after the build process. Similarly one can customize the install target or even provide new targets. Extension points are documented in paragraph \ref{coqmakefile:local}. - -The extensions of the files listed in {\tt \_CoqProject} is -used in order to decide how to build them. In particular: - -\begin{itemize} -\item {\Coq} files must use the \texttt{.v} extension -\item {\ocaml} files must use the \texttt{.ml} or \texttt{.mli} extension -\item {\ocaml} files that require pre processing for syntax extensions (like {\tt VERNAC EXTEND}) must use the \texttt{.ml4} extension -\item In order to generate a plugin one has to list all {\ocaml} modules (i.e. ``Baz'' for ``baz.ml'') in a \texttt{.mlpack} file (or \texttt{.mllib} file). -\end{itemize} - -The use of \texttt{.mlpack} files has to be preferred over \texttt{.mllib} -files, since it results in a ``packed'' plugin: All auxiliary -modules (as {\tt Baz} and {\tt Bazaux}) are hidden inside -the plugin's ``name space'' ({\tt Qux\_plugin}). -This reduces the chances of begin unable to load two distinct plugins -because of a clash in their auxiliary module names. - -\paragraph{CoqMakefile.local} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\label{coqmakefile:local} - -The optional file {\tt CoqMakefile.local} is included by the generated file -{\tt CoqMakefile}. Such can contain two kinds of directives. - -\begin{description} - \item[Variable assignment] to the variables listed in the {\tt Parameters} - section of the generated makefile. Here we describe only few of them. - \begin{description} - \item[CAMLPKGS] can be used to specify third party findlib packages, and is - passed to the OCaml compiler on building or linking of modules. - Eg: {\tt -package yojson}. - \item[CAMLFLAGS] can be used to specify additional flags to the OCaml - compiler, like {\tt -bin-annot} or {\tt -w...}. - \item[COQC, COQDEP, COQDOC] can be set in order to use alternative - binaries (e.g. wrappers) - \item[COQ\_SRC\_SUBDIRS] can be extended by including other paths in which {\tt *.cm*} files are searched. For example {\tt COQ\_SRC\_SUBDIRS+=user-contrib/Unicoq} lets you build a plugin containing OCaml code that depends on the OCaml code of {\tt Unicoq}. - \end{description} -\item[Rule extension] - The following makefile rules can be extended. For example -\begin{verbatim} -pre-all:: - echo "This line is print before making the all target" -install-extra:: - cp ThisExtraFile /there/it/goes -\end{verbatim} - \begin{description} - \item[pre-all::] run before the {\tt all} target. One can use this - to configure the project, or initialize sub modules or check - dependencies are met. - \item[post-all::] run after the {\tt all} target. One can use this - to run a test suite, or compile extracted code. - \item[install-extra::] run after {\tt install}. One can use this - to install extra files. - \item[install-doc::] One can use this to install extra doc. - \item[uninstall::] - \item[uninstall-doc::] - \item[clean::] - \item[cleanall::] - \item[archclean::] - \item[merlin-hook::] One can append lines to the generated {\tt .merlin} - file extending this target. - \end{description} -\end{description} - -\paragraph{Timing targets and performance testing} %%%%%%%%%%%%%%%%%%%%%%%%%%% -The generated \texttt{Makefile} supports the generation of two kinds -of timing data: per-file build-times, and per-line times for an -individual file. - -The following targets and \texttt{Makefile} variables allow collection -of per-file timing data: -\begin{itemize} -\item \texttt{TIMED=1} --- passing this variable will cause - \texttt{make} to emit a line describing the user-space build-time - and peak memory usage for each file built. - - \texttt{Note}: On Mac OS, this works best if you've installed - \texttt{gnu-time}. - - \texttt{Example}: For example, the output of \texttt{make TIMED=1} - may look like this: -\begin{verbatim} -COQDEP Fast.v -COQDEP Slow.v -COQC Slow.v -Slow (user: 0.34 mem: 395448 ko) -COQC Fast.v -Fast (user: 0.01 mem: 45184 ko) -\end{verbatim} -\item \texttt{pretty-timed} --- this target stores the output of - \texttt{make TIMED=1} into \texttt{time-of-build.log}, and displays - a table of the times, sorted from slowest to fastest, which is also - stored in \texttt{time-of-build-pretty.log}. If you want to - construct the log for targets other than the default one, you can - pass them via the variable \texttt{TGTS}, e.g., \texttt{make - pretty-timed TGTS="a.vo b.vo"}. - - \texttt{Note}: This target requires \texttt{python} to build the table. - - \texttt{Note}: This target will \emph{append} to the timing log; if - you want a fresh start, you must remove the file - \texttt{time-of-build.log} or run \texttt{make cleanall}. - - \texttt{Example}: For example, the output of \texttt{make - pretty-timed} may look like this: -\begin{verbatim} -COQDEP Fast.v -COQDEP Slow.v -COQC Slow.v -Slow (user: 0.36 mem: 393912 ko) -COQC Fast.v -Fast (user: 0.05 mem: 45992 ko) -Time | File Name --------------------- -0m00.41s | Total --------------------- -0m00.36s | Slow -0m00.05s | Fast -\end{verbatim} -\item \texttt{print-pretty-timed-diff} --- this target builds a table - of timing changes between two compilations; run \texttt{make - make-pretty-timed-before} to build the log of the ``before'' - times, and run \texttt{make make-pretty-timed-after} to build the - log of the ``after'' times. The table is printed on the command - line, and stored in \texttt{time-of-build-both.log}. This target is - most useful for profiling the difference between two commits to a - repo. - - \texttt{Note}: This target requires \texttt{python} to build the table. - - \texttt{Note}: The \texttt{make-pretty-timed-before} and - \texttt{make-pretty-timed-after} targets will \emph{append} to the - timing log; if you want a fresh start, you must remove the files - \texttt{time-of-build-before.log} and - \texttt{time-of-build-after.log} or run \texttt{make cleanall} - \emph{before} building either the ``before'' or ``after'' targets. - - \texttt{Note}: The table will be sorted first by absolute time - differences rounded towards zero to a whole-number of seconds, then - by times in the ``after'' column, and finally lexicographically by - file name. This will put the biggest changes in either direction - first, and will prefer sorting by build-time over subsecond changes - in build time (which are frequently noise); lexicographic sorting - forces an order on files which take effectively no time to compile. - - \texttt{Example}: For example, the output table from \texttt{make - print-pretty-timed-diff} may look like this: -\begin{verbatim} -After | File Name | Before || Change | % Change --------------------------------------------------------- -0m00.39s | Total | 0m00.35s || +0m00.03s | +11.42% --------------------------------------------------------- -0m00.37s | Slow | 0m00.01s || +0m00.36s | +3600.00% -0m00.02s | Fast | 0m00.34s || -0m00.32s | -94.11% -\end{verbatim} -\end{itemize} - -The following targets and \texttt{Makefile} variables allow collection -of per-line timing data: -\begin{itemize} -\item \texttt{TIMING=1} --- passing this variable will cause - \texttt{make} to use \texttt{coqc -time} to write to a - \texttt{.v.timing} file for each \texttt{.v} file compiled, which - contains line-by-line timing information. - - \texttt{Example}: For example, running \texttt{make all TIMING=1} may - result in a file like this: -\begin{verbatim} -Chars 0 - 26 [Require~Coq.ZArith.BinInt.] 0.157 secs (0.128u,0.028s) -Chars 27 - 68 [Declare~Reduction~comp~:=~vm_c...] 0. secs (0.u,0.s) -Chars 69 - 162 [Definition~foo0~:=~Eval~comp~i...] 0.153 secs (0.136u,0.019s) -Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] 0.239 secs (0.236u,0.s) -\end{verbatim} - -\item \texttt{print-pretty-single-time-diff - BEFORE=path/to/file.v.before-timing - AFTER=path/to/file.v.after-timing} --- this target will make a - sorted table of the per-line timing differences between the timing - logs in the \texttt{BEFORE} and \texttt{AFTER} files, display it, - and save it to the file specified by the - \texttt{TIME\_OF\_PRETTY\_BUILD\_FILE} variable, which defaults to - \texttt{time-of-build-pretty.log}. - - To generate the \texttt{.v.before-timing} or - \texttt{.v.after-timing} files, you should pass - \texttt{TIMING=before} or \texttt{TIMING=after} rather than - \texttt{TIMING=1}. - - \texttt{Note}: The sorting used here is the same as in the - \texttt{print-pretty-timed-diff} target. - - \texttt{Note}: This target requires \texttt{python} to build the table. - - \texttt{Example}: For example, running - \texttt{print-pretty-single-time-diff} might give a table like this: -\begin{verbatim} -After | Code | Before || Change | % Change ---------------------------------------------------------------------------------------------------- -0m00.50s | Total | 0m04.17s || -0m03.66s | -87.96% ---------------------------------------------------------------------------------------------------- -0m00.145s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.192s || -0m00.04s | -24.47% -0m00.126s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.143s || -0m00.01s | -11.88% - N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | 0m00.s || +0m00.00s | N/A -0m00.s | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | N/A || +0m00.00s | N/A -0m00.231s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m03.836s || -0m03.60s | -93.97% -\end{verbatim} - -\item \texttt{all.timing.diff}, \texttt{path/to/file.v.timing.diff} - --- The \texttt{path/to/file.v.timing.diff} target will make a - \texttt{.v.timing.diff} file for the corresponding \texttt{.v} file, - with a table as would be generated by the - \texttt{print-pretty-single-time-diff} target; it depends on having - already made the corresponding \texttt{.v.before-timing} and - \texttt{.v.after-timing} files, which can be made by passing - \texttt{TIMING=before} and \texttt{TIMING=after}. The - \texttt{all.timing.diff} target will make such timing difference - files for all of the \texttt{.v} files that the \texttt{Makefile} - knows about. It will fail if some \texttt{.v.before-timing} or - \texttt{.v.after-timing} files don't exist. - - \texttt{Note}: This target requires \texttt{python} to build the table. -\end{itemize} - -\paragraph{Reusing/extending the generated Makefile} %%%%%%%%%%%%%%%%%%%%%%%%% - -Including the generated makefile with an {\tt include} directive is discouraged. -The contents of this file, including variable names -and status of rules shall change in the future. Users are advised to -include {\tt Makefile.conf} or call a target of the generated Makefile -as in {\tt make -f Makefile target} from another Makefile. - -One way to get access to all targets of the generated -\texttt{CoqMakefile} is to have a generic target for invoking unknown -targets. For example: -\begin{verbatim} -# KNOWNTARGETS will not be passed along to CoqMakefile -KNOWNTARGETS := CoqMakefile extra-stuff extra-stuff2 -# KNOWNFILES will not get implicit targets from the final rule, and so -# depending on them won't invoke the submake -# Warning: These files get declared as PHONY, so any targets depending -# on them always get rebuilt -KNOWNFILES := Makefile _CoqProject - -.DEFAULT_GOAL := invoke-coqmakefile - -CoqMakefile: Makefile _CoqProject - $(COQBIN)coq_makefile -f _CoqProject -o CoqMakefile - -invoke-coqmakefile: CoqMakefile - $(MAKE) --no-print-directory -f CoqMakefile $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS)) - -.PHONY: invoke-coqmakefile $(KNOWNFILES) - -#################################################################### -## Your targets here ## -#################################################################### - -# This should be the last rule, to handle any targets not declared above -%: invoke-coqmakefile - @true -\end{verbatim} - -\paragraph{Building a subset of the targets with -j} %%%%%%%%%%%%%%%%%%%%%%%%% - -To build, say, two targets \texttt{foo.vo} and \texttt{bar.vo} -in parallel one can use \texttt{make only TGTS="foo.vo bar.vo" -j}. - -Note that \texttt{make foo.vo bar.vo -j} has a different meaning for -the make utility, in particular it may build a shared prerequisite twice. - -\paragraph{Notes for users of {\tt coq\_makefile} with version $<$ 8.7} %%%%%% - -\begin{itemize} -\item Support for ``sub-directory'' is deprecated. To perform actions before - or after the build (like invoking make on a subdirectory) one can - hook in {\tt pre-all} and {\tt post-all} extension points -\item \texttt{-extra-phony} and \texttt{-extra} are deprecated. To provide - additional target ({\tt .PHONY} or not) please use - {\tt CoqMakefile.local} -\end{itemize} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\section[Modules dependencies]{Modules dependencies\label{Dependencies}\index{Dependencies} - \ttindex{coqdep}} - -In order to compute modules dependencies (so to use {\tt make}), -\Coq\ comes with an appropriate tool, {\tt coqdep}. - -{\tt coqdep} computes inter-module dependencies for \Coq\ and -\ocaml\ programs, and prints the dependencies on the standard -output in a format readable by make. When a directory is given as -argument, it is recursively looked at. - -Dependencies of \Coq\ modules are computed by looking at {\tt Require} -commands ({\tt Require}, {\tt Requi\-re Export}, {\tt Require Import}, -but also at the command {\tt Declare ML Module}. - -Dependencies of \ocaml\ modules are computed by looking at -\verb!open! commands and the dot notation {\em module.value}. However, -this is done approximately and you are advised to use {\tt ocamldep} -instead for the \ocaml\ modules dependencies. - -See the man page of {\tt coqdep} for more details and options. - -The build infrastructure generated by {\tt coq\_makefile} -uses {\tt coqdep} to automatically compute the dependencies -among the files part of the project. - -\section[Documenting \Coq\ files with coqdoc]{Documenting \Coq\ files with coqdoc\label{coqdoc} -\ttindex{coqdoc}} - -\input{./coqdoc} - -\section[Embedded \Coq\ phrases inside \LaTeX\ documents]{Embedded \Coq\ phrases inside \LaTeX\ documents\label{Latex} - \ttindex{coq-tex}\index{Latex@{\LaTeX}}} - -When writing a documentation about a proof development, one may want -to insert \Coq\ phrases inside a \LaTeX\ document, possibly together with -the corresponding answers of the system. We provide a -mechanical way to process such \Coq\ phrases embedded in \LaTeX\ files: the -{\tt coq-tex} filter. This filter extracts Coq phrases embedded in -LaTeX files, evaluates them, and insert the outcome of the evaluation -after each phrase. - -Starting with a file {\em file}{\tt.tex} containing \Coq\ phrases, -the {\tt coq-tex} filter produces a file named {\em file}{\tt.v.tex} with -the \Coq\ outcome. - -There are options to produce the \Coq\ parts in smaller font, italic, -between horizontal rules, etc. -See the man page of {\tt coq-tex} for more details. - -\medskip\noindent {\bf Remark.} This Reference Manual and the Tutorial -have been completely produced with {\tt coq-tex}. - - -\section[\Coq\ and \emacs]{\Coq\ and \emacs\label{Emacs}\index{Emacs}} - -\subsection{The \Coq\ Emacs mode} - -\Coq\ comes with a Major mode for \emacs, {\tt gallina.el}. This mode provides -syntax highlighting -and also a rudimentary indentation facility -in the style of the Caml \emacs\ mode. - -Add the following lines to your \verb!.emacs! file: - -\begin{verbatim} - (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) - (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t) -\end{verbatim} - -The \Coq\ major mode is triggered by visiting a file with extension {\tt .v}, -or manually with the command \verb!M-x coq-mode!. -It gives you the correct syntax table for -the \Coq\ language, and also a rudimentary indentation facility: -\begin{itemize} - \item pressing {\sc Tab} at the beginning of a line indents the line like - the line above; - - \item extra {\sc Tab}s increase the indentation level - (by 2 spaces by default); - - \item M-{\sc Tab} decreases the indentation level. -\end{itemize} - -An inferior mode to run \Coq\ under Emacs, by Marco Maggesi, is also -included in the distribution, in file \texttt{inferior-coq.el}. -Instructions to use it are contained in this file. - -\subsection[{\ProofGeneral}]{{\ProofGeneral}\index{Proof General@{\ProofGeneral}}} - -{\ProofGeneral} is a generic interface for proof assistants based on -Emacs. The main idea is that the \Coq\ commands you are -editing are sent to a \Coq\ toplevel running behind Emacs and the -answers of the system automatically inserted into other Emacs buffers. -Thus you don't need to copy-paste the \Coq\ material from your files -to the \Coq\ toplevel or conversely from the \Coq\ toplevel to some -files. - -{\ProofGeneral} is developed and distributed independently of the -system \Coq. It is freely available at \verb!https://proofgeneral.github.io/!. - - -\section[Module specification]{Module specification\label{gallina}\ttindex{gallina}} - -Given a \Coq\ vernacular file, the {\tt gallina} filter extracts its -specification (inductive types declarations, definitions, type of -lemmas and theorems), removing the proofs parts of the file. The \Coq\ -file {\em file}{\tt.v} gives birth to the specification file -{\em file}{\tt.g} (where the suffix {\tt.g} stands for \gallina). - -See the man page of {\tt gallina} for more details and options. - - -\section[Man pages]{Man pages\label{ManPages}\index{Man pages}} - -There are man pages for the commands {\tt coqdep}, {\tt gallina} and -{\tt coq-tex}. Man pages are installed at installation time -(see installation instructions in file {\tt INSTALL}, step 6). - -%BEGIN LATEX -\RefManCutCommand{ENDREFMAN=\thepage} -%END LATEX - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: t -%%% End: diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 8909c0fef..d61c70d64 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -105,12 +105,6 @@ Options A and B of the licence are {\em not} elected.} \lstset{moredelim=[is][]{|*}{*|}} \lstset{moredelim=*[is][\itshape\rmfamily]{/*}{*/}} -\part{User extensions} -%%SUPPRIME \include{RefMan-tus.v}% Writing tactics - -\part{Practical tools} -\include{RefMan-uti}% utilities (gallina, do_Makefile, etc) - %BEGIN LATEX \RefManCutCommand{BEGINADDENDUM=\thepage} %END LATEX diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex deleted file mode 100644 index 26dbd59e7..000000000 --- a/doc/refman/coqdoc.tex +++ /dev/null @@ -1,573 +0,0 @@ - -%\newcommand{\Coq}{\textsf{Coq}} -\newcommand{\javadoc}{\textsf{javadoc}} -\newcommand{\ocamldoc}{\textsf{ocamldoc}} -\newcommand{\coqdoc}{\textsf{coqdoc}} -\newcommand{\texmacs}{\TeX{}macs} -\newcommand{\monurl}[1]{#1} -%HEVEA\renewcommand{\monurl}[1]{\ahref{#1}{#1}} -%\newcommand{\lnot}{not} % Hevea handles these symbols nicely -%\newcommand{\lor}{or} -%\newcommand{\land}{\&} -%%% Beware : in a \texttt, -- is displayed as a unique - hence -%%% the following macro: -\newcommand{\mm}{\symbol{45}\symbol{45}} - - -\coqdoc\ is a documentation tool for the proof assistant -\Coq, similar to \javadoc\ or \ocamldoc. -The task of \coqdoc\ is -\begin{enumerate} -\item to produce a nice \LaTeX\ and/or HTML document from the \Coq\ - sources, readable for a human and not only for the proof assistant; -\item to help the user navigating in his own (or third-party) sources. -\end{enumerate} - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\subsection{Principles} - -Documentation is inserted into \Coq\ files as \emph{special comments}. -Thus your files will compile as usual, whether you use \coqdoc\ or not. -\coqdoc\ presupposes that the given \Coq\ files are well-formed (at -least lexically). Documentation starts with -\texttt{(**}, followed by a space, and ends with the pending \texttt{*)}. -The documentation format is inspired - by Todd~A.~Coram's \emph{Almost Free Text (AFT)} tool: it is mainly -ASCII text with some syntax-light controls, described below. -\coqdoc\ is robust: it shouldn't fail, whatever the input is. But -remember: ``garbage in, garbage out''. - -\paragraph{\Coq\ material inside documentation.} -\Coq\ material is quoted between the -delimiters \texttt{[} and \texttt{]}. Square brackets may be nested, -the inner ones being understood as being part of the quoted code (thus -you can quote a term like \texttt{fun x => u} by writing -\texttt{[fun x => u]}). Inside quotations, the code is pretty-printed in -the same way as it is in code parts. - -Pre-formatted vernacular is enclosed by \texttt{[[} and -\texttt{]]}. The former must be followed by a newline and the latter -must follow a newline. - -\paragraph{Pretty-printing.} -\coqdoc\ uses different faces for identifiers and keywords. -The pretty-printing of \Coq\ tokens (identifiers or symbols) can be -controlled using one of the following commands: -\begin{alltt} -(** printing \emph{token} %...\LaTeX...% #...HTML...# *) -\end{alltt} -or -\begin{alltt} -(** printing \emph{token} $...\LaTeX\ math...$ #...HTML...# *) -\end{alltt} -It gives the \LaTeX\ and HTML texts to be produced for the given \Coq\ -token. One of the \LaTeX\ or HTML text may be omitted, causing the -default pretty-printing to be used for this token. - -The printing for one token can be removed with -\begin{alltt} -(** remove printing \emph{token} *) -\end{alltt} - -Initially, the pretty-printing table contains the following mapping: -\begin{center} - \begin{tabular}{ll@{\qquad\qquad}ll@{\qquad\qquad}ll@{\qquad\qquad}} - \verb!->! & $\rightarrow$ & - \verb!<-! & $\leftarrow$ & - \verb|*| & $\times$ \\ - \verb|<=| & $\le$ & - \verb|>=| & $\ge$ & - \verb|=>| & $\Rightarrow$ \\ - \verb|<>| & $\not=$ & - \verb|<->| & $\leftrightarrow$ & - \verb!|-! & $\vdash$ \\ - \verb|\/| & $\lor$ & - \verb|/\| & $\land$ & - \verb|~| & $\lnot$ - \end{tabular} -\end{center} -Any of these can be overwritten or suppressed using the -\texttt{printing} commands. - -Important note: the recognition of tokens is done by a (ocaml)lex -automaton and thus applies the longest-match rule. For instance, -\verb!->~! is recognized as a single token, where \Coq\ sees two -tokens. It is the responsibility of the user to insert space between -tokens \emph{or} to give pretty-printing rules for the possible -combinations, e.g. -\begin{verbatim} -(** printing ->~ %\ensuremath{\rightarrow\lnot}% *) -\end{verbatim} - - -\paragraph{Sections.} -Sections are introduced by 1 to 4 leading stars (i.e. at the beginning of the -line) followed by a space. One star is a section, two stars a sub-section, etc. -The section title is given on the remaining of the line. -Example: -\begin{verbatim} - (** * Well-founded relations - - In this section, we introduce... *) -\end{verbatim} - - -%TODO \paragraph{Fonts.} - - -\paragraph{Lists.} -List items are introduced by a leading dash. \coqdoc\ uses whitespace -to determine the depth of a new list item and which text belongs in -which list items. A list ends when a line of text starts at or before -the level of indenting of the list's dash. A list item's dash must -always be the first non-space character on its line (so, in -particular, a list can not begin on the first line of a comment - -start it on the second line instead). - -Example: -\begin{verbatim} - We go by induction on [n]: - - If [n] is 0... - - If [n] is [S n'] we require... - - two paragraphs of reasoning, and two subcases: - - - In the first case... - - In the second case... - - So the theorem holds. -\end{verbatim} - -\paragraph{Rules.} -More than 4 leading dashes produce a horizontal rule. - -\paragraph{Emphasis.} -Text can be italicized by placing it in underscores. A non-identifier -character must precede the leading underscore and follow the trailing -underscore, so that uses of underscores in names aren't mistaken for -emphasis. Usually, these are spaces or punctuation. - -\begin{verbatim} - This sentence contains some _emphasized text_. -\end{verbatim} - -\paragraph{Escaping to \LaTeX\ and HTML.} -Pure \LaTeX\ or HTML material can be inserted using the following -escape sequences: -\begin{itemize} -\item \verb+$...LaTeX stuff...$+ inserts some \LaTeX\ material in math mode. - Simply discarded in HTML output. - -\item \verb+%...LaTeX stuff...%+ inserts some \LaTeX\ material. - Simply discarded in HTML output. - -\item \verb+#...HTML stuff...#+ inserts some HTML material. Simply - discarded in \LaTeX\ output. -\end{itemize} - -Note: to simply output the characters \verb+$+, \verb+%+ and \verb+#+ -and escaping their escaping role, these characters must be doubled. - -\paragraph{Verbatim.} -Verbatim material is introduced by a leading \verb+<<+ and closed by -\verb+>>+ at the beginning of a line. Example: -\begin{verbatim} -Here is the corresponding caml code: -<< - let rec fact n = - if n <= 1 then 1 else n * fact (n-1) ->> -\end{verbatim} - - -\paragraph{Hyperlinks.} -Hyperlinks can be inserted into the HTML output, so that any -identifier is linked to the place of its definition. - -\texttt{coqc \emph{file}.v} automatically dumps localization information -in \texttt{\emph{file}.glob} or appends it to a file specified using option -\texttt{\mm{}dump-glob \emph{file}}. Take care of erasing this global file, if -any, when starting the whole compilation process. - -Then invoke \texttt{coqdoc} or \texttt{coqdoc \mm{}glob-from \emph{file}} to tell -\coqdoc\ to look for name resolutions into the file \texttt{\emph{file}} -(it will look in \texttt{\emph{file}.glob} by default). - -Identifiers from the \Coq\ standard library are linked to the \Coq\ -web site at \url{http://coq.inria.fr/library/}. This behavior can be -changed using command line options \texttt{\mm{}no-externals} and -\texttt{\mm{}coqlib}; see below. - - -\paragraph{Hiding / Showing parts of the source.} -Some parts of the source can be hidden using command line options -\texttt{-g} and \texttt{-l} (see below), or using such comments: -\begin{alltt} -(* begin hide *) -\emph{some Coq material} -(* end hide *) -\end{alltt} -Conversely, some parts of the source which would be hidden can be -shown using such comments: -\begin{alltt} -(* begin show *) -\emph{some Coq material} -(* end show *) -\end{alltt} -The latter cannot be used around some inner parts of a proof, but can -be used around a whole proof. - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\subsection{Usage} - -\coqdoc\ is invoked on a shell command line as follows: -\begin{displaymath} - \texttt{coqdoc }<\textit{options and files}> -\end{displaymath} -Any command line argument which is not an option is considered to be a -file (even if it starts with a \verb!-!). \Coq\ files are identified -by the suffixes \verb!.v! and \verb!.g! and \LaTeX\ files by the -suffix \verb!.tex!. - -\begin{description} -\item[HTML output] ~\par - This is the default output. - One HTML file is created for each \Coq\ file given on the command line, - together with a file \texttt{index.html} (unless option - \texttt{-no-index} is passed). The HTML pages use a style sheet - named \texttt{style.css}. Such a file is distributed with \coqdoc. - -\item[\LaTeX\ output] ~\par - A single \LaTeX\ file is created, on standard output. It can be - redirected to a file with option \texttt{-o}. - The order of files on the command line is kept in the final - document. \LaTeX\ files given on the command line are copied `as is' - in the final document . - DVI and PostScript can be produced directly with the options - \texttt{-dvi} and \texttt{-ps} respectively. - -\item[\texmacs\ output] ~\par - To translate the input files to \texmacs\ format, to be used by - the \texmacs\ Coq interface. - %broken link: - %(see \url{http://www-sop.inria.fr/lemme/Philippe.Audebaud/tmcoq/}). -\end{description} - - -\subsubsection*{Command line options} - - -\paragraph{Overall options} - -\begin{description} - -\item[\texttt{\mm{}html}] ~\par - - Select a HTML output. - -\item[\texttt{\mm{}latex}] ~\par - - Select a \LaTeX\ output. - -\item[\texttt{\mm{}dvi}] ~\par - - Select a DVI output. - -\item[\texttt{\mm{}ps}] ~\par - - Select a PostScript output. - -\item[\texttt{\mm{}texmacs}] ~\par - - Select a \texmacs\ output. - -\item[\texttt{\mm{}stdout}] ~\par - - Write output to stdout. - -\item[\texttt{-o }\textit{file}, \texttt{\mm{}output }\textit{file}] ~\par - - Redirect the output into the file `\textit{file}' (meaningless with - \texttt{-html}). - -\item[\texttt{-d }\textit{dir}, \texttt{\mm{}directory }\textit{dir}] ~\par - - Output files into directory `\textit{dir}' instead of current - directory (option \texttt{-d} does not change the filename specified - with option \texttt{-o}, if any). - -\item[\texttt{\mm{}body-only}] ~\par - - Suppress the header and trailer of the final document. Thus, you can - insert the resulting document into a larger one. - -\item[\texttt{-p} \textit{string}, \texttt{\mm{}preamble} \textit{string}]~\par - - Insert some material in the \LaTeX\ preamble, right before - \verb!\begin{document}! (meaningless with \texttt{-html}). - -\item[\texttt{\mm{}vernac-file }\textit{file}, - \texttt{\mm{}tex-file }\textit{file}] ~\par - - Considers the file `\textit{file}' respectively as a \verb!.v! - (or \verb!.g!) file or a \verb!.tex! file. - -\item[\texttt{\mm{}files-from }\textit{file}] ~\par - - Read file names to process in file `\textit{file}' as if they were - given on the command line. Useful for program sources split up into - several directories. - -\item[\texttt{-q}, \texttt{\mm{}quiet}] ~\par - - Be quiet. Do not print anything except errors. - -\item[\texttt{-h}, \texttt{\mm{}help}] ~\par - - Give a short summary of the options and exit. - -\item[\texttt{-v}, \texttt{\mm{}version}] ~\par - - Print the version and exit. - -\end{description} - -\paragraph{Index options} - -Default behavior is to build an index, for the HTML output only, into -\texttt{index.html}. - -\begin{description} - -\item[\texttt{\mm{}no-index}] ~\par - - Do not output the index. - -\item[\texttt{\mm{}multi-index}] ~\par - - Generate one page for each category and each letter in the index, - together with a top page \texttt{index.html}. - -\item[\texttt{\mm{}index }\textit{string}] ~\par - - Make the filename of the index \textit{string} instead of ``index''. - Useful since ``index.html'' is special. - -\end{description} - -\paragraph{Table of contents option} - -\begin{description} - -\item[\texttt{-toc}, \texttt{\mm{}table-of-contents}] ~\par - - Insert a table of contents. - For a \LaTeX\ output, it inserts a \verb!\tableofcontents! at the - beginning of the document. For a HTML output, it builds a table of - contents into \texttt{toc.html}. - -\item[\texttt{\mm{}toc-depth }\textit{int}] ~\par - - Only include headers up to depth \textit{int} in the table of - contents. - -\end{description} - -\paragraph{Hyperlinks options} -\begin{description} - -\item[\texttt{\mm{}glob-from }\textit{file}] ~\par - - Make references using \Coq\ globalizations from file \textit{file}. - (Such globalizations are obtained with \Coq\ option \texttt{-dump-glob}). - -\item[\texttt{\mm{}no-externals}] ~\par - - Do not insert links to the \Coq\ standard library. - -\item[\texttt{\mm{}external }\textit{url}~\textit{coqdir}] ~\par - - Use given URL for linking references whose name starts with prefix - \textit{coqdir}. - -\item[\texttt{\mm{}coqlib }\textit{url}] ~\par - - Set base URL for the \Coq\ standard library (default is - \url{http://coq.inria.fr/library/}). This is equivalent to - \texttt{\mm{}external }\textit{url}~\texttt{Coq}. - -\item[\texttt{-R }\textit{dir }\textit{coqdir}] ~\par - - Map physical directory \textit{dir} to \Coq\ logical directory - \textit{coqdir} (similarly to \Coq\ option \texttt{-R}). - - Note: option \texttt{-R} only has effect on the files - \emph{following} it on the command line, so you will probably need - to put this option first. - -\end{description} - -\paragraph{Title options} -\begin{description} -\item[\texttt{-s }, \texttt{\mm{}short}] ~\par - - Do not insert titles for the files. The default behavior is to - insert a title like ``Library Foo'' for each file. - -\item[\texttt{\mm{}lib-name }\textit{string}] ~\par - - Print ``\textit{string} Foo'' instead of ``Library Foo'' in titles. - For example ``Chapter'' and ``Module'' are reasonable choices. - -\item[\texttt{\mm{}no-lib-name}] ~\par - - Print just ``Foo'' instead of ``Library Foo'' in titles. - -\item[\texttt{\mm{}lib-subtitles}] ~\par - - Look for library subtitles. When enabled, the beginning of each - file is checked for a comment of the form: -\begin{alltt} -(** * ModuleName : text *) -\end{alltt} - where \texttt{ModuleName} must be the name of the file. If it is - present, the \texttt{text} is used as a subtitle for the module in - appropriate places. - -\item[\texttt{-t }\textit{string}, - \texttt{\mm{}title }\textit{string}] ~\par - - Set the document title. - -\end{description} - -\paragraph{Contents options} -\begin{description} - -\item[\texttt{-g}, \texttt{\mm{}gallina}] ~\par - - Do not print proofs. - -\item[\texttt{-l}, \texttt{\mm{}light}] ~\par - - Light mode. Suppress proofs (as with \texttt{-g}) and the following commands: - \begin{itemize} - \item {}[\texttt{Recursive}] \texttt{Tactic Definition} - \item \texttt{Hint / Hints} - \item \texttt{Require} - \item \texttt{Transparent / Opaque} - \item \texttt{Implicit Argument / Implicits} - \item \texttt{Section / Variable / Hypothesis / End} - \end{itemize} - -\end{description} -The behavior of options \texttt{-g} and \texttt{-l} can be locally -overridden using the \texttt{(* begin show *)} \dots\ \texttt{(* end - show *)} environment (see above). - -There are a few options to drive the parsing of comments: -\begin{description} -\item[\texttt{\mm{}parse-comments}] ~\par - - Parses regular comments delimited by \texttt{(*} and \texttt{*)} as - well. They are typeset inline. - -\item[\texttt{\mm{}plain-comments}] ~\par - - Do not interpret comments, simply copy them as plain-text. - -\item[\texttt{\mm{}interpolate}] ~\par - - Use the globalization information to typeset identifiers appearing in - \Coq{} escapings inside comments. -\end{description} - - -\paragraph{Language options} - -Default behavior is to assume ASCII 7 bits input files. - -\begin{description} - -\item[\texttt{-latin1}, \texttt{\mm{}latin1}] ~\par - - Select ISO-8859-1 input files. It is equivalent to - \texttt{\mm{}inputenc latin1 \mm{}charset iso-8859-1}. - -\item[\texttt{-utf8}, \texttt{\mm{}utf8}] ~\par - - Set \texttt{\mm{}inputenc utf8x} for \LaTeX\ output and - \texttt{\mm{}charset utf-8} for HTML output. Also use Unicode - replacements for a couple of standard plain ASCII notations such - as $\rightarrow$ for \texttt{->} and $\forall$ for - \texttt{forall}. \LaTeX\ UTF-8 support can be found at - \url{http://www.ctan.org/pkg/unicode}. - - For the interpretation of Unicode characters by \LaTeX, extra - packages which {\coqdoc} does not provide by default might be - required, such as \texttt{textgreek} for some Greek letters or - \texttt{stmaryrd} for some mathematical symbols. If a Unicode - character is missing an interpretation in the \texttt{utf8x} input - encoding, add - \verb=\DeclareUnicodeCharacter{=\textit{code}\verb=}{=\textit{latex-interpretation}\verb=}=. Packages - and declarations can be added with option \texttt{-p}. - -\item[\texttt{\mm{}inputenc} \textit{string}] ~\par - - Give a \LaTeX\ input encoding, as an option to \LaTeX\ package - \texttt{inputenc}. - -\item[\texttt{\mm{}charset} \textit{string}] ~\par - - Specify the HTML character set, to be inserted in the HTML header. - -\end{description} - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\subsection[The coqdoc \LaTeX{} style file]{The coqdoc \LaTeX{} style file\label{section:coqdoc.sty}} - -In case you choose to produce a document without the default \LaTeX{} -preamble (by using option \verb|--no-preamble|), then you must insert -into your own preamble the command -\begin{quote} - \verb|\usepackage{coqdoc}| -\end{quote} - -The package optionally takes the argument \verb|[color]| to typeset -identifiers with colors (this requires the \verb|xcolor| package). - -Then you may alter the rendering of the document by -redefining some macros: -\begin{description} - -\item[\texttt{coqdockw}, \texttt{coqdocid}, \ldots] ~ - - The one-argument macros for typesetting keywords and identifiers. - Defaults are sans-serif for keywords and italic for identifiers. - - For example, if you would like a slanted font for keywords, you - may insert -\begin{verbatim} - \renewcommand{\coqdockw}[1]{\textsl{#1}} -\end{verbatim} - anywhere between \verb|\usepackage{coqdoc}| and - \verb|\begin{document}|. - -\item[\texttt{coqdocmodule}] ~ - - One-argument macro for typesetting the title of a \verb|.v| file. - Default is -\begin{verbatim} -\newcommand{\coqdocmodule}[1]{\section*{Module #1}} -\end{verbatim} - and you may redefine it using \verb|\renewcommand|. - -\end{description} - - diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst index e2824d7ca..e24e6a4ec 100644 --- a/doc/sphinx/index.rst +++ b/doc/sphinx/index.rst @@ -39,6 +39,7 @@ Table of contents :caption: Practical tools practical-tools/coq-commands + practical-tools/utilities practical-tools/coqide .. toctree:: diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst new file mode 100644 index 000000000..620c002ff --- /dev/null +++ b/doc/sphinx/practical-tools/utilities.rst @@ -0,0 +1,999 @@ +.. include:: ../replaces.rst + +.. _utilities: + +--------------------- + Utilities +--------------------- + +The distribution provides utilities to simplify some tedious works +beside proof development, tactics writing or documentation. + + +Using Coq as a library +---------------------- + +In previous versions, ``coqmktop`` was used to build custom +toplevels - for example for better debugging or custom static +linking. Nowadays, the preferred method is to use ``ocamlfind``. + +The most basic custom toplevel is built using: + +:: + + % ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg \ + -package coq.toplevel \ + toplevel/coqtop\_bin.ml -o my\_toplevel.native + + +For example, to statically link |L_tac|, you can just do: + +:: + + % ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg \ + -package coq.toplevel -package coq.ltac \ + toplevel/coqtop\_bin.ml -o my\_toplevel.native +and similarly for other plugins. + + +Building a |Coq| project with coq_makefile +------------------------------------------ + +The majority of |Coq| projects are very similar: a collection of ``.v`` +files and eventually some ``.ml`` ones (a |Coq| plugin). The main piece of +metadata needed in order to build the project are the command line +options to ``coqc`` (e.g. ``-R``, ``-I``, see also: Section +:ref:`bycommandline`). Collecting the list of files and options is the job +of the ``_CoqProject`` file. + +A simple example of a ``_CoqProject`` file follows: + +:: + + -R theories/ MyCode + theories/foo.v + theories/bar.v + -I src/ + src/baz.ml4 + src/bazaux.ml + src/qux_plugin.mlpack + + +Currently, both |CoqIDE| and |ProofGeneral| (version ≥ ``4.3pre``) +understand ``_CoqProject`` files and invoke |Coq| with the desired options. + +The ``coq_makefile`` utility can be used to set up a build infrastructure +for the |Coq| project based on makefiles. The recommended way of +invoking ``coq_makefile`` is the following one: + +:: + + coq_makefile -f _CoqProject -o CoqMakefile + + +Such command generates the following files: + +CoqMakefile + is a generic makefile for ``GNU Make`` that provides + targets to build the project (both ``.v`` and ``.ml*`` files), to install it + system-wide in the ``coq-contrib`` directory (i.e. where |Coq| is installed) + as well as to invoke |coqdoc| to generate |HTML| documentation. + +CoqMakefile.conf + contains make variables assignments that reflect + the contents of the ``_CoqProject`` file as well as the path relevant to + |Coq|. + + +An optional file ``CoqMakefile.local`` can be provided by the user in order to +extend ``CoqMakefile``. In particular one can declare custom actions to be +performed before or after the build process. Similarly one can customize the +install target or even provide new targets. Extension points are documented in +paragraph :ref:`coqmakefile:local`. + +The extensions of the files listed in ``_CoqProject`` is used in order to +decide how to build them. In particular: + + ++ |Coq| files must use the ``.v`` extension ++ |OCaml| files must use the ``.ml`` or ``.mli`` extension ++ |OCaml| files that require pre processing for syntax + extensions (like ``VERNAC EXTEND``) must use the ``.ml4`` extension ++ In order to generate a plugin one has to list all |OCaml| + modules (i.e. ``Baz`` for ``baz.ml``) in a ``.mlpack`` file (or ``.mllib`` + file). + + +The use of ``.mlpack`` files has to be preferred over ``.mllib`` files, +since it results in a “packed” plugin: All auxiliary modules (as +``Baz`` and ``Bazaux``) are hidden inside the plugin’s “name space” +(``Qux_plugin``). This reduces the chances of begin unable to load two +distinct plugins because of a clash in their auxiliary module names. + +.. _coqmakefilelocal: + +CoqMakefile.local ++++++++++++++++++ + + + +The optional file ``CoqMakefile.local`` is included by the generated +file ``CoqMakefile``. It can contain two kinds of directives. + +Variable assignment + The variable must belong to the variables listed in the ``Parameters`` section of the generated makefile. + Here we describe only few of them. + :CAMLPKGS: + can be used to specify third party findlib packages, and is + passed to the OCaml compiler on building or linking of modules. Eg: + ``-package yojson``. + :CAMLFLAGS: + can be used to specify additional flags to the |OCaml| + compiler, like ``-bin-annot`` or ``-w``.... + :COQC, COQDEP, COQDOC: + can be set in order to use alternative binaries + (e.g. wrappers) + :COQ_SRC_SUBDIRS: can be extended by including other paths in which ``*.cm*`` files are searched. For example ``COQ\_SRC\_SUBDIRS+=user-contrib/Unicoq`` lets you build a plugin containing OCaml code that depends on the OCaml code of ``Unicoq``. + +Rule extension + The following makefile rules can be extended. + + .. example :: + + :: + + pre-all:: + echo "This line is print before making the all target" + install-extra:: + cp ThisExtraFile /there/it/goes + + ``pre-all::`` + run before the all target. One can use this to configure + the project, or initialize sub modules or check dependencies are met. + + ``post-all::`` + run after the all target. One can use this to run a test + suite, or compile extracted code. + + + ``install-extra::`` + run after install. One can use this to install extra files. + + ``install-doc::`` + One can use this to install extra doc. + + ``uninstall::`` + \ + + ``uninstall-doc::`` + \ + + ``clean::`` + \ + + ``cleanall::`` + \ + + ``archclean::`` + \ + + ``merlin-hook::`` + One can append lines to the generated .merlin file extending this + target. + +Timing targets and performance testing +++++++++++++++++++++++++++++++++++++++ + +The generated ``Makefile`` supports the generation of two kinds of timing +data: per-file build-times, and per-line times for an individual file. + +The following targets and Makefile variables allow collection of per- +file timing data: + + ++ ``TIMED=1`` + passing this variable will cause ``make`` to emit a line + describing the user-space build-time and peak memory usage for each + file built. + + .. note:: + On ``Mac OS``, this works best if you’ve installed ``gnu-time``. + + .. example:: + For example, the output of ``make TIMED=1`` may look like + this: + + :: + + COQDEP Fast.v + COQDEP Slow.v + COQC Slow.v + Slow (user: 0.34 mem: 395448 ko) + COQC Fast.v + Fast (user: 0.01 mem: 45184 ko) + ++ ``pretty-timed`` + this target stores the output of ``make TIMED=1`` into + ``time-of-build.log``, and displays a table of the times, sorted from + slowest to fastest, which is also stored in ``time-of-build-pretty.log``. + If you want to construct the ``log`` for targets other than the default + one, you can pass them via the variable ``TGTS``, e.g., ``make pretty-timed + TGTS="a.vo b.vo"``. + + .. :: + This target requires ``python`` to build the table. + + .. note:: + This target will *append* to the timing log; if you want a + fresh start, you must remove the ``filetime-of-build.log`` or + ``run make cleanall``. + + .. example:: + + For example, the output of ``make pretty-timed`` may look like this: + + :: + + COQDEP Fast.v + COQDEP Slow.v + COQC Slow.v + Slow (user: 0.36 mem: 393912 ko) + COQC Fast.v + Fast (user: 0.05 mem: 45992 ko) + Time | File Name + -------------------- + 0m00.41s | Total + -------------------- + 0m00.36s | Slow + 0m00.05s | Fast + + ++ ``print-pretty-timed-diff`` + this target builds a table of timing + changes between two compilations; run ``make make-pretty-timed-before`` to + build the log of the “before” times, and run ``make make-pretty-timed- + after`` to build the log of the “after” times. The table is printed on + the command line, and stored in ``time-of-build-both.log``. This target is + most useful for profiling the difference between two commits to a + repo. + + .. note:: + This target requires ``python`` to build the table. + + .. note:: + The ``make-pretty-timed-before`` and ``make-pretty-timed-after`` targets will + *append* to the timing log; if you want a fresh start, you must remove + the files ``time-of-build-before.log`` and ``time-of-build-after.log`` or run + ``make cleanall`` *before* building either the “before” or “after” + targets. + + .. note:: + The table will be sorted first by absolute time + differences rounded towards zero to a whole-number of seconds, then by + times in the “after” column, and finally lexicographically by file + name. This will put the biggest changes in either direction first, and + will prefer sorting by build-time over subsecond changes in build time + (which are frequently noise); lexicographic sorting forces an order on + files which take effectively no time to compile. + + .. example:: + For example, the output table from + ``make print-pretty-timed-diff`` may look like this: + + :: + + After | File Name | Before || Change | % Change + -------------------------------------------------------- + 0m00.39s | Total | 0m00.35s || +0m00.03s | +11.42% + -------------------------------------------------------- + 0m00.37s | Slow | 0m00.01s || +0m00.36s | +3600.00% + 0m00.02s | Fast | 0m00.34s || -0m00.32s | -94.11% + + +The following targets and ``Makefile`` variables allow collection of per- +line timing data: + + ++ ``TIMING=1`` + passing this variable will cause ``make`` to use ``coqc -time`` to + write to a ``.v.timing`` file for each ``.v`` file compiled, which contains + line-by-line timing information. + + .. example:: + For example, running ``make all TIMING=1`` may result in a file like this: + + :: + + Chars 0 - 26 [Require~Coq.ZArith.BinInt.] 0.157 secs (0.128u,0.028s) + Chars 27 - 68 [Declare~Reduction~comp~:=~vm_c...] 0. secs (0.u,0.s) + Chars 69 - 162 [Definition~foo0~:=~Eval~comp~i...] 0.153 secs (0.136u,0.019s) + Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] 0.239 secs (0.236u,0.s) + ++ ``print-pretty-single-time-diff`` + :: + + print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing + this target will make a sorted table of the per-line timing differences + between the timing logs in the ``BEFORE`` and ``AFTER`` files, display it, and + save it to the file specified by the ``TIME_OF_PRETTY_BUILD_FILE`` variable, + which defaults to ``time-of-build-pretty.log``. + To generate the ``.v.before-timing`` or ``.v.after-timing`` files, you should + pass ``TIMING=before`` or ``TIMING=after`` rather than ``TIMING=1``. + + .. note:: + The sorting used here is the same as in the ``print-pretty-timed -diff`` target. + + .. note:: + This target requires python to build the table. + + .. example:: + For example, running ``print-pretty-single-time-diff`` might give a table like this: + + :: + + After | Code | Before || Change | % Change + --------------------------------------------------------------------------------------------------- + 0m00.50s | Total | 0m04.17s || -0m03.66s | -87.96% + --------------------------------------------------------------------------------------------------- + 0m00.145s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.192s || -0m00.04s | -24.47% + 0m00.126s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.143s || -0m00.01s | -11.88% + N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | 0m00.s || +0m00.00s | N/A + 0m00.s | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | N/A || +0m00.00s | N/A + 0m00.231s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m03.836s || -0m03.60s | -93.97% + + ++ ``all.timing.diff``, ``path/to/file.v.timing.diff`` + The ``path/to/file.v.timing.diff`` target will make a ``.v.timing.diff`` file for + the corresponding ``.v`` file, with a table as would be generated by + the ``print-pretty-single-time-diff`` target; it depends on having already + made the corresponding ``.v.before-timing`` and ``.v.after-timing`` files, + which can be made by passing ``TIMING=before`` and ``TIMING=after``. + The ``all.timing.diff`` target will make such timing difference files for + all of the ``.v`` files that the ``Makefile`` knows about. It will fail if + some ``.v.before-timing`` or ``.v.after-timing`` files don’t exist. + + .. note:: + This target requires python to build the table. + + +Reusing/extending the generated Makefile +++++++++++++++++++++++++++++++++++++++++ + +Including the generated makefile with an include directive is +discouraged. The contents of this file, including variable names and +status of rules shall change in the future. Users are advised to +include ``Makefile.conf`` or call a target of the generated Makefile as in +``make -f Makefile target`` from another Makefile. + +One way to get access to all targets of the generated ``CoqMakefile`` is to +have a generic target for invoking unknown targets. + +.. example:: + + :: + + # KNOWNTARGETS will not be passed along to CoqMakefile + KNOWNTARGETS := CoqMakefile extra-stuff extra-stuff2 + # KNOWNFILES will not get implicit targets from the final rule, and so + # depending on them won't invoke the submake + # Warning: These files get declared as PHONY, so any targets depending + # on them always get rebuilt + KNOWNFILES := Makefile _CoqProject + + .DEFAULT_GOAL := invoke-coqmakefile + + CoqMakefile: Makefile _CoqProject + $(COQBIN)coq_makefile -f _CoqProject -o CoqMakefile + + invoke-coqmakefile: CoqMakefile + $(MAKE) --no-print-directory -f CoqMakefile $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS)) + + .PHONY: invoke-coqmakefile $(KNOWNFILES) + + #################################################################### + ## Your targets here ## + #################################################################### + + # This should be the last rule, to handle any targets not declared above + %: invoke-coqmakefile + @true + + + +Building a subset of the targets with -j +++++++++++++++++++++++++++++++++++++++++ + +To build, say, two targets foo.vo and bar.vo in parallel one can use +``make only TGTS="foo.vo bar.vo" -j``. + +.. note:: + + ``make foo.vo bar.vo -j`` has a different meaning for the make + utility, in particular it may build a shared prerequisite twice. + + +.. note:: + + For users of coq_makefile with version < 8.7 + + + Support for “sub-directory” is deprecated. To perform actions before + or after the build (like invoking ``make`` on a subdirectory) one can hook + in pre-all and post-all extension points. + + ``-extra-phony`` and ``-extra`` are deprecated. To provide additional target + (``.PHONY`` or not) please use ``CoqMakefile.local``. + + + +Modules dependencies +-------------------- + +In order to compute modules dependencies (so to use ``make``), |Coq| comes +with an appropriate tool, ``coqdep``. + +``coqdep`` computes inter-module dependencies for |Coq| and |OCaml| +programs, and prints the dependencies on the standard output in a +format readable by make. When a directory is given as argument, it is +recursively looked at. + +Dependencies of |Coq| modules are computed by looking at ``Require`` +commands (``Require``, ``Require Export``, ``Require Import``), but also at the +command ``Declare ML Module``. + +Dependencies of |OCaml| modules are computed by looking at +`open` commands and the dot notation *module.value*. However, this is +done approximately and you are advised to use ``ocamldep`` instead for the +|OCaml| modules dependencies. + +See the man page of ``coqdep`` for more details and options. + +The build infrastructure generated by ``coq_makefile`` uses ``coqdep`` to +automatically compute the dependencies among the files part of the +project. + + +Documenting |Coq| files with coqdoc +----------------------------------- + +|coqdoc| is a documentation tool for the proof assistant |Coq|, similar to +``javadoc`` or ``ocamldoc``. The task of |coqdoc| is + + +#. to produce a nice |Latex| and/or |HTML| document from the |Coq| + sources, readable for a human and not only for the proof assistant; +#. to help the user navigating in his own (or third-party) sources. + + + +Principles +~~~~~~~~~~ + +Documentation is inserted into |Coq| files as *special comments*. Thus +your files will compile as usual, whether you use |coqdoc| or not. |coqdoc| +presupposes that the given |Coq| files are well-formed (at least +lexically). Documentation starts with ``(**``, followed by a space, and +ends with the pending ``*)``. The documentation format is inspired by Todd +A. Coram’s *Almost Free Text (AFT)* tool: it is mainly ``ASCII`` text with +some syntax-light controls, described below. |coqdoc| is robust: it +shouldn’t fail, whatever the input is. But remember: “garbage in, +garbage out”. + + +|Coq| material inside documentation. +++++++++++++++++++++++++++++++++++ + +|Coq| material is quoted between the delimiters ``[`` and ``]``. Square brackets +may be nested, the inner ones being understood as being part of the +quoted code (thus you can quote a term like ``fun x => u`` by writing ``[fun +x => u]``). Inside quotations, the code is pretty-printed in the same +way as it is in code parts. + +Pre-formatted vernacular is enclosed by ``[[`` and ``]]``. The former must be +followed by a newline and the latter must follow a newline. + + +Pretty-printing. +++++++++++++++++ + +|coqdoc| uses different faces for identifiers and keywords. The pretty- +printing of |Coq| tokens (identifiers or symbols) can be controlled +using one of the following commands: + +:: + + + (** printing *token* %...LATEX...% #...html...# *) + + +or + +:: + + + (** printing *token* $...LATEX math...$ #...html...# *) + + +It gives the |Latex| and |HTML| texts to be produced for the given |Coq| +token. One of the |Latex| or |HTML| text may be omitted, causing the +default pretty-printing to be used for this token. + +The printing for one token can be removed with + +:: + + + (** remove printing *token* *) + + +Initially, the pretty-printing table contains the following mapping: + +==== === ==== ===== === ==== ==== === +`->` → `<-` ← `*` × +`<=` ≤ `>=` ≥ `=>` ⇒ +`<>` ≠ `<->` ↔ `|-` ⊢ +`\/` ∨ `/\` ∧ `~` ¬ +==== === ==== ===== === ==== ==== === + +Any of these can be overwritten or suppressed using the printing +commands. + +.. note :: + The recognition of tokens is done by a (``ocaml``) lex + automaton and thus applies the longest-match rule. For instance, `->~` + is recognized as a single token, where |Coq| sees two tokens. It is the + responsibility of the user to insert space between tokens *or* to give + pretty-printing rules for the possible combinations, e.g. + + :: + + (** printing ->~ %\ensuremath{\rightarrow\lnot}% *) + + + +Sections. ++++++++++ + +Sections are introduced by 1 to 4 leading stars (i.e. at the beginning +of the line) followed by a space. One star is a section, two stars a +sub-section, etc. The section title is given on the remaining of the +line. + +.. example:: + + :: + + (** * Well-founded relations + + In this section, we introduce... *) + + +Lists. +++++++ + +List items are introduced by a leading dash. coqdoc uses whitespace to +determine the depth of a new list item and which text belongs in which +list items. A list ends when a line of text starts at or before the +level of indenting of the list’s dash. A list item’s dash must always +be the first non-space character on its line (so, in particular, a +list can not begin on the first line of a comment - start it on the +second line instead). + +.. example:: + + :: + + We go by induction on [n]: + - If [n] is 0... + - If [n] is [S n'] we require... + + two paragraphs of reasoning, and two subcases: + + - In the first case... + - In the second case... + + So the theorem holds. + + + +Rules. +++++++ + +More than 4 leading dashes produce a horizontal rule. + + +Emphasis. ++++++++++ + +Text can be italicized by placing it in underscores. A non-identifier +character must precede the leading underscore and follow the trailing +underscore, so that uses of underscores in names aren’t mistaken for +emphasis. Usually, these are spaces or punctuation. + +:: + + This sentence contains some _emphasized text_. + + + +Escaping to |Latex| and |HTML|. ++++++++++++++++++++++++++++++++ + +Pure |Latex| or |HTML| material can be inserted using the following +escape sequences: + + ++ ``$...LATEX stuff...$`` inserts some |Latex| material in math mode. + Simply discarded in |HTML| output. ++ ``%...LATEX stuff...%`` inserts some |Latex| material. Simply + discarded in |HTML| output. ++ ``#...HTML stuff...#`` inserts some |HTML| material. Simply discarded in + |Latex| output. + +.. note:: + to simply output the characters ``$``, ``%`` and ``#`` and escaping + their escaping role, these characters must be doubled. + + +Verbatim +++++++++ + +Verbatim material is introduced by a leading ``<<`` and closed by ``>>`` +at the beginning of a line. + +.. example:: + + :: + + Here is the corresponding caml code: + << + let rec fact n = + if n <= 1 then 1 else n * fact (n-1) + >> + + + +Hyperlinks +++++++++++ + +Hyperlinks can be inserted into the |HTML| output, so that any +identifier is linked to the place of its definition. + +``coqc file.v`` automatically dumps localization information in +``file.glob`` or appends it to a file specified using option ``--dump-glob +file``. Take care of erasing this global file, if any, when starting +the whole compilation process. + +Then invoke |coqdoc| or ``coqdoc --glob-from file`` to tell |coqdoc| to look +for name resolutions into the file ``file`` (it will look in ``file.glob`` +by default). + +Identifiers from the |Coq| standard library are linked to the Coq web +site at `<http://coq.inria.fr/library/>`_. This behavior can be changed +using command line options ``--no-externals`` and ``--coqlib``; see below. + + +Hiding / Showing parts of the source. ++++++++++++++++++++++++++++++++++++++ + +Some parts of the source can be hidden using command line options ``-g`` +and ``-l`` (see below), or using such comments: + +:: + + + (* begin hide *) + *some Coq material* + (* end hide *) + + +Conversely, some parts of the source which would be hidden can be +shown using such comments: + +:: + + + (* begin show *) + *some Coq material* + (* end show *) + + +The latter cannot be used around some inner parts of a proof, but can +be used around a whole proof. + + +Usage +~~~~~ + +|coqdoc| is invoked on a shell command line as follows: +``coqdoc <options and files>``. +Any command line argument which is not an option is considered to be a +file (even if it starts with a ``-``). |Coq| files are identified by the +suffixes ``.v`` and ``.g`` and |Latex| files by the suffix ``.tex``. + + +:|HTML| output: This is the default output. One |HTML| file is created for + each |Coq| file given on the command line, together with a file + ``index.html`` (unless ``option-no-index is passed``). The |HTML| pages use a + style sheet named ``style.css``. Such a file is distributed with |coqdoc|. +:|Latex| output: A single |Latex| file is created, on standard + output. It can be redirected to a file with option ``-o``. The order of + files on the command line is kept in the final document. |Latex| + files given on the command line are copied ‘as is’ in the final + document . DVI and PostScript can be produced directly with the + options ``-dvi`` and ``-ps`` respectively. +:TEXmacs output: To translate the input files to TEXmacs format, + to be used by the TEXmacs |Coq| interface. + + + +Command line options +++++++++++++++++++++ + + +**Overall options** + + + :--|HTML|: Select a |HTML| output. + :--|Latex|: Select a |Latex| output. + :--dvi: Select a DVI output. + :--ps: Select a PostScript output. + :--texmacs: Select a TEXmacs output. + :--stdout: Write output to stdout. + :-o file, --output file: Redirect the output into the file ‘file’ + (meaningless with ``-html``). + :-d dir, --directory dir: Output files into directory ‘dir’ instead of + current directory (option ``-d`` does not change the filename specified + with option ``-o``, if any). + :--body-only: Suppress the header and trailer of the final document. + Thus, you can insert the resulting document into a larger one. + :-p string, --preamble string: Insert some material in the |Latex| + preamble, right before ``\begin{document}`` (meaningless with ``-html``). + :--vernac-file file,--tex-file file: Considers the file ‘file’ + respectively as a ``.v`` (or ``.g``) file or a ``.tex`` file. + :--files-from file: Read file names to process in file ‘file’ as if + they were given on the command line. Useful for program sources split + up into several directories. + :-q, --quiet: Be quiet. Do not print anything except errors. + :-h, --help: Give a short summary of the options and exit. + :-v, --version: Print the version and exit. + + + +**Index options** + + Default behavior is to build an index, for the |HTML| output only, + into ``index.html``. + + :--no-index: Do not output the index. + :--multi-index: Generate one page for each category and each letter in + the index, together with a top page ``index.html``. + :--index string: Make the filename of the index string instead of + “index”. Useful since “index.html” is special. + + + +**Table of contents option** + + :-toc, --table-of-contents: Insert a table of contents. For a |Latex| + output, it inserts a ``\tableofcontents`` at the beginning of the + document. For a |HTML| output, it builds a table of contents into + ``toc.html``. + :--toc-depth int: Only include headers up to depth ``int`` in the table of + contents. + + +**Hyperlinks options** + + :--glob-from file: Make references using |Coq| globalizations from file + file. (Such globalizations are obtained with Coq option ``-dump-glob``). + :--no-externals: Do not insert links to the |Coq| standard library. + :--external url coqdir: Use given URL for linking references whose + name starts with prefix ``coqdir``. + :--coqlib url: Set base URL for the Coq standard library (default is + `<http://coq.inria.fr/library/>`_). This is equivalent to ``--external url + Coq``. + :-R dir coqdir: Map physical directory dir to |Coq| logical + directory ``coqdir`` (similarly to |Coq| option ``-R``). + + .. note:: + option ``-R`` only has + effect on the files *following* it on the command line, so you will + probably need to put this option first. + + +**Title options** + + :-s , --short: Do not insert titles for the files. The default + behavior is to insert a title like “Library Foo” for each file. + :--lib-name string: Print “string Foo” instead of “Library Foo” in + titles. For example “Chapter” and “Module” are reasonable choices. + :--no-lib-name: Print just “Foo” instead of “Library Foo” in titles. + :--lib-subtitles: Look for library subtitles. When enabled, the + beginning of each file is checked for a comment of the form: + + :: + + + (** * ModuleName : text *) + + where ``ModuleName`` must be the name of the file. If it is present, the + text is used as a subtitle for the module in appropriate places. + :-t string, --title string: Set the document title. + + +**Contents options** + + :-g, --gallina: Do not print proofs. + :-l, --light: Light mode. Suppress proofs (as with ``-g``) and the following commands: + + + [Recursive] Tactic Definition + + Hint / Hints + + Require + + Transparent / Opaque + + Implicit Argument / Implicits + + Section / Variable / Hypothesis / End + + + + The behavior of options ``-g`` and ``-l`` can be locally overridden using the + ``(* begin show *) … (* end show *)`` environment (see above). + + There are a few options to drive the parsing of comments: + + :--parse-comments: Parses regular comments delimited by ``(*`` and ``*)`` as + well. They are typeset inline. + :--plain-comments: Do not interpret comments, simply copy them as + plain-text. + :--interpolate: Use the globalization information to typeset + identifiers appearing in |Coq| escapings inside comments. + +**Language options** + + + Default behavior is to assume ASCII 7 bits input files. + + :-latin1, --latin1: Select ISO-8859-1 input files. It is equivalent to + --inputenc latin1 --charset iso-8859-1. + :-utf8, --utf8: Set --inputenc utf8x for |Latex| output and--charset + utf-8 for |HTML| output. Also use Unicode replacements for a couple of + standard plain ASCII notations such as → for ``->`` and ∀ for ``forall``. |Latex| + UTF-8 support can be found + at `<http://www.ctan.org/pkg/unicode>`_. For the interpretation of Unicode + characters by |Latex|, extra packages which |coqdoc| does not provide + by default might be required, such as textgreek for some Greek letters + or ``stmaryrd`` for some mathematical symbols. If a Unicode character is + missing an interpretation in the utf8x input encoding, add + ``\DeclareUnicodeCharacter{code}{LATEX-interpretation}``. Packages + and declarations can be added with option ``-p``. + :--inputenc string: Give a |Latex| input encoding, as an option to |Latex| + package ``inputenc``. + :--charset string: Specify the |HTML| character set, to be inserted in + the |HTML| header. + + + +The coqdoc |Latex| style file +~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +In case you choose to produce a document without the default |Latex| +preamble (by using option ``--no-preamble``), then you must insert into +your own preamble the command + +:: + + \usepackage{coqdoc} + +The package optionally takes the argument ``[color]`` to typeset +identifiers with colors (this requires the ``xcolor`` package). + +Then you may alter the rendering of the document by redefining some +macros: + +:coqdockw, coqdocid, …: The one-argument macros for typesetting + keywords and identifiers. Defaults are sans-serif for keywords and + italic for identifiers.For example, if you would like a slanted font + for keywords, you may insert + + :: + + \renewcommand{\coqdockw}[1]{\textsl{#1}} + + + anywhere between ``\usepackage{coqdoc}`` and ``\begin{document}``. + + +:coqdocmodule: + One-argument macro for typesetting the title of a ``.v`` + file. Default is + + :: + + \newcommand{\coqdocmodule}[1]{\section*{Module #1}} + + and you may redefine it using ``\renewcommand``. + +Embedded Coq phrases inside |Latex| documents +--------------------------------------------- + +When writing a documentation about a proof development, one may want +to insert |Coq| phrases inside a |Latex| document, possibly together +with the corresponding answers of the system. We provide a mechanical +way to process such |Coq| phrases embedded in |Latex| files: the ``coq-tex`` +filter. This filter extracts |Coq| phrases embedded in |Latex| files, +evaluates them, and insert the outcome of the evaluation after each +phrase. + +Starting with a file ``file.tex`` containing |Coq| phrases, the ``coq-tex`` +filter produces a file named ``file.v.tex`` with the Coq outcome. + +There are options to produce the |Coq| parts in smaller font, italic, +between horizontal rules, etc. See the man page of ``coq-tex`` for more +details. + +|Coq| and |GNU| |Emacs| +----------------------- + + +The |Coq| |Emacs| mode +~~~~~~~~~~~~~~~~~~~~~~~~~ + +|Coq| comes with a Major mode for |GNU| |Emacs|, ``gallina.el``. This mode +provides syntax highlighting and also a rudimentary indentation +facility in the style of the ``Caml`` |GNU| |Emacs| mode. + +Add the following lines to your ``.emacs`` file: + +:: + + (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) + (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t) + + +The |Coq| major mode is triggered by visiting a file with extension ``.v``, +or manually with the command ``M-x coq-mode``. It gives you the correct +syntax table for the |Coq| language, and also a rudimentary indentation +facility: + + ++ pressing ``Tab`` at the beginning of a line indents the line like the + line above; ++ extra ``Tab``s increase the indentation level (by 2 spaces by default); ++ ``M-Tab`` decreases the indentation level. + + +An inferior mode to run |Coq| under |Emacs|, by Marco Maggesi, is also +included in the distribution, in file ``inferior-coq.el``. Instructions to +use it are contained in this file. + + +Proof General +~~~~~~~~~~~~~ + +|ProofGeneral| is a generic interface for proof assistants based on +|Emacs|. The main idea is that the |Coq| commands you are editing are sent +to a |Coq| toplevel running behind |Emacs| and the answers of the system +automatically inserted into other |Emacs| buffers. Thus you don’t need +to copy-paste the |Coq| material from your files to the |Coq| toplevel or +conversely from the |Coq| toplevel to some files. + +|ProofGeneral| is developed and distributed independently of the system +|Coq|. It is freely available at `<https://proofgeneral.github.io/>`_. + + +Module specification +-------------------- + +Given a |Coq| vernacular file, the gallina filter extracts its +specification (inductive types declarations, definitions, type of +lemmas and theorems), removing the proofs parts of the file. The |Coq| +file ``file.v`` gives birth to the specification file ``file.g`` (where +the suffix ``.g`` stands for |Gallina|). + +See the man page of ``gallina`` for more details and options. + + +Man pages +--------- + +There are man pages for the commands ``coqdep``, ``gallina`` and ``coq-tex``. Man +pages are installed at installation time (see installation +instructions in file ``INSTALL``, step 6). |