diff options
-rw-r--r-- | Makefile.doc | 1 | ||||
-rw-r--r-- | doc/refman/RefMan-com.tex | 402 | ||||
-rw-r--r-- | doc/refman/Reference-Manual.tex | 1 | ||||
-rw-r--r-- | doc/sphinx/index.rst | 2 | ||||
-rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 256 |
5 files changed, 258 insertions, 404 deletions
diff --git a/Makefile.doc b/Makefile.doc index 077ae965c..01f4f34b3 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -68,7 +68,6 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ REFMANTEXFILES:=$(addprefix doc/refman/, \ headers.sty Reference-Manual.tex \ - RefMan-com.tex \ RefMan-uti.tex RefMan-ide.tex \ AsyncProofs.tex RefMan-ssr.tex) \ $(REFMANCOQTEXFILES) \ diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex deleted file mode 100644 index 5b73ac00a..000000000 --- a/doc/refman/RefMan-com.tex +++ /dev/null @@ -1,402 +0,0 @@ -\chapter[The \Coq~commands]{The \Coq~commands\label{Addoc-coqc} -\ttindex{coqtop} -\ttindex{coqc} -\ttindex{coqchk}} -%HEVEA\cutname{commands.html} - -There are three \Coq~commands: -\begin{itemize} -\item {\tt coqtop}: the \Coq\ toplevel (interactive mode); -\item {\tt coqc}: the \Coq\ compiler (batch compilation); -\item {\tt coqchk}: the \Coq\ checker (validation of compiled libraries). -\end{itemize} -The options are (basically) the same for the first two commands, and -roughly described below. You can also look at the \verb!man! pages of -\verb!coqtop! and \verb!coqc! for more details. - - -\section{Interactive use ({\tt coqtop})} - -In the interactive mode, also known as the \Coq~toplevel, the user can -develop his theories and proofs step by step. The \Coq~toplevel is -run by the command {\tt coqtop}. - -\index{byte-code} -\index{native code} -\label{binary-images} -They are two different binary images of \Coq: the byte-code one and -the native-code one (if {\ocaml} provides a native-code compiler -for your platform, which is supposed in the following). By default, -\verb!coqtop! executes the native-code version; run \verb!coqtop.byte! to -get the byte-code version. - -The byte-code toplevel is based on an {\ocaml} -toplevel (to allow the dynamic link of tactics). You can switch to -the {\ocaml} toplevel with the command \verb!Drop.!, and come back to the -\Coq~toplevel with the command \verb!Coqloop.loop();;!. - -\section{Batch compilation ({\tt coqc})} -The {\tt coqc} command takes a name {\em file} as argument. Then it -looks for a vernacular file named {\em file}{\tt .v}, and tries to -compile it into a {\em file}{\tt .vo} file (See ~\ref{compiled}). - -\Warning The name {\em file} should be a regular {\Coq} identifier, as -defined in Section~\ref{lexical}. It should contain only letters, digits -or underscores (\_). For instance, \verb+/bar/foo/toto.v+ is valid, but -\verb+/bar/foo/to-to.v+ is invalid. - -\section[Customization]{Customization at launch time} - -\subsection{By resource file\index{Resource file}} - -When \Coq\ is launched, with either {\tt coqtop} or {\tt coqc}, the -resource file \verb:$XDG_CONFIG_HOME/coq/coqrc.xxx: is loaded, where -\verb:$XDG_CONFIG_HOME: is the configuration directory of the user (by -default its home directory \verb!/.config! and \verb:xxx: is the version -number (e.g. 8.3). If this file is not found, then the file -\verb:$XDG_CONFIG_HOME/coqrc: is searched. You can also specify an -arbitrary name for the resource file (see option \verb:-init-file: -below). - - -This file may contain, for instance, \verb:Add LoadPath: commands to add -directories to the load path of \Coq. -It is possible to skip the loading of the resource file with the -option \verb:-q:. - -\subsection{By environment variables\label{EnvVariables} -\index{Environment variables}\label{envars}} - -Load path can be specified to the \Coq\ system by setting up -\verb:$COQPATH: environment variable. It is a list of directories -separated by \verb|:| (\verb|;| on windows). {\Coq} will also honor -\verb:$XDG_DATA_HOME: and \verb:$XDG_DATA_DIRS: (see Section -\ref{loadpath}). - -Some {\Coq} commands call other {\Coq} commands. In this case, they -look for the commands in directory specified by \verb:$COQBIN:. If -this variable is not set, they look for the commands in the executable -path. - -The \verb:$COQ_COLORS: environment variable can be used to specify the set of -colors used by {\tt coqtop} to highlight its output. It uses the same syntax as -the \verb:$LS_COLORS: variable from GNU's {\tt ls}, that is, a colon-separated -list of assignments of the form \verb:name=attr1;...;attrn: where {\tt name} is -the name of the corresponding highlight tag and {\tt attri} is an ANSI escape -code. The list of highlight tags can be retrieved with the {\tt -list-tags} -command-line option of {\tt coqtop}. - -\subsection{By command line options\index{Options of the command line} -\label{coqoptions}} - -The following command-line options are recognized by the commands {\tt - coqc} and {\tt coqtop}, unless stated otherwise: - -\begin{description} -\item[{\tt -I} {\em directory}, {\tt -include} {\em directory}]\ % - - Add physical path {\em directory} to the {\ocaml} loadpath. - - \SeeAlso Section~\ref{Libraries} and the command {\tt Declare ML Module} Section \ref{compiled}. - -\item[{\tt -Q} {\em directory} {\dirpath}]\ % - - Add physical path \emph{directory} to the list of directories where - {\Coq} looks for a file and bind it to the the logical directory - \emph{dirpath}. The subdirectory structure of \emph{directory} is - recursively available from {\Coq} using absolute names (extending - the {\dirpath} prefix) (see Section~\ref{LongNames}). - - Note that only those subdirectories and files which obey the lexical - conventions of what is an {\ident} (see Section~\ref{lexical}) - are taken into account. Conversely, the underlying file systems or - operating systems may be more restrictive than {\Coq}. While Linux's - ext4 file system supports any {\Coq} recursive layout - (within the limit of 255 bytes per file name), the default on NTFS - (Windows) or HFS+ (MacOS X) file systems is on the contrary to - disallow two files differing only in the case in the same directory. - - \SeeAlso Section~\ref{Libraries}. - -\item[{\tt -R} {\em directory} {\dirpath}]\ % - - Do as \texttt{-Q} \emph{directory} {\dirpath} but make the - subdirectory structure of \emph{directory} recursively visible so - that the recursive contents of physical \emph{directory} is available - from {\Coq} using short or partially qualified names. - - \SeeAlso Section~\ref{Libraries}. - -\item[{\tt -top} {\dirpath}]\ % - - Set the toplevel module name to {\dirpath} instead of {\tt Top}. Not - valid for {\tt coqc} as the toplevel module name is inferred from the - name of the output file. - -\item[{\tt -exclude-dir} {\em directory}]\ % - - Exclude any subdirectory named {\em directory} while - processing options such as {\tt -R} and {\tt -Q}. By default, only the - conventional version control management directories named {\tt CVS} and - {\tt \_darcs} are excluded. - -\item[{\tt -nois}]\ % - - Start from an empty state instead of loading the {\tt Init.Prelude} - module. - -\item[{\tt -init-file} {\em file}]\ % - - Load {\em file} as the resource file instead of loading the default - resource file from the standard configuration directories. - -\item[{\tt -q}]\ % - - Do not to load the default resource file. - -\item[{\tt -load-ml-source} {\em file}]\ % - - Load the {\ocaml} source file {\em file}. - -\item[{\tt -load-ml-object} {\em file}]\ % - - Load the {\ocaml} object file {\em file}. - -\item[{\tt -l} {\em file}, {\tt -load-vernac-source} {\em file}]\ % - - Load and execute the {\Coq} script from {\em file.v}. - -\item[{\tt -lv} {\em file}, {\tt -load-vernac-source-verbose} {\em - file}]\ % - - Load and execute the {\Coq} script from {\em file.v}. - Output its content on the standard input as it is executed. - -\item[{\tt -load-vernac-object} {\dirpath}]\ % - - Load \Coq~compiled library {\dirpath}. This is equivalent to running - {\tt Require} {\dirpath}. - -\item[{\tt -require} {\dirpath}]\ % - - Load \Coq~compiled library {\dirpath} and import it. This is equivalent - to running {\tt Require Import} {\dirpath}. - -\item[{\tt -batch}]\ % - - Exit just after argument parsing. Available for {\tt coqtop} only. - -\item[{\tt -compile} {\em file.v}]\ % - - Compile file {\em file.v} into {\em file.vo}. This options imply {\tt - -batch} (exit just after argument parsing). It is available only - for {\tt coqtop}, as this behavior is the purpose of {\tt coqc}. - -\item[{\tt -compile-verbose} {\em file.v}]\ % - - Same as {\tt -compile} but also output the content of {\em file.v} as - it is compiled. - -\item[{\tt -verbose}]\ % - - Output the content of the input file as it is compiled. This option is - available for {\tt coqc} only; it is the counterpart of {\tt - -compile-verbose}. - - \item[{\tt -w} (all|none|w$_1$,\ldots,w$_n$)]\ % - - Configure the display of warnings. This option expects {\tt all}, {\tt none} - or a comma-separated list of warning names or categories (see - Section~\ref{SetWarnings}). - -%Mostly unused in the code -%\item[{\tt -debug}]\ % -% -% Switch on the debug flag. - -\item[{\tt -color} (on|off|auto)]\ % - - Enable or not the coloring of output of {\tt coqtop}. Default is auto, - meaning that {\tt coqtop} dynamically decides, depending on whether the - output channel supports ANSI escape sequences. - -\item[{\tt -beautify}]\ % - - Pretty-print each command to {\em file.beautified} when compiling {\em - file.v}, in order to get old-fashioned syntax/definitions/notations. - -\item[{\tt -emacs}, {\tt -ide-slave}]\ % - - Start a special toplevel to communicate with a specific IDE. - -\item[{\tt -impredicative-set}]\ % - - Change the logical theory of {\Coq} by declaring the sort {\tt Set} - impredicative. Warning: this is known to be inconsistent with - some standard axioms of classical mathematics such as the functional - axiom of choice or the principle of description. - -\item[{\tt -type-in-type}]\ % - - Collapse the universe hierarchy of {\Coq}. Warning: this makes the - logic inconsistent. - -\item[{\tt -mangle-names} {\em ident}]\ % - - Experimental: Do not depend on this option. - - Replace Coq's auto-generated name scheme with names of the form - {\tt ident0}, {\tt ident1}, \ldots etc. - The command {\tt Set Mangle Names}\optindex{Mangle Names} turns - the behavior on in a document, and {\tt Set Mangle Names Prefix "ident"} - \optindex{Mangle Names Prefix} changes the used prefix. - - This feature is intended to be used as a linter for developments that want - to be robust to changes in the auto-generated name scheme. The options are - provided to facilitate tracking down problems. - -\item[{\tt -compat} {\em version}]\ % - - Attempt to maintain some backward-compatibility with a previous version. - -\item[{\tt -dump-glob} {\em file}]\ % - - Dump references for global names in file {\em file} (to be used - by {\tt coqdoc}, see~\ref{coqdoc}). By default, if {\em file.v} is being - compiled, {\em file.glob} is used. - -\item[{\tt -no-glob}]\ % - - Disable the dumping of references for global names. - -%\item[{\tt -no-hash-consing}]\ % - -\item[{\tt -image} {\em file}]\ % - - Set the binary image to be used by {\tt coqc} to be {\em file} - instead of the standard one. Not of general use. - -\item[{\tt -bindir} {\em directory}]\ % - - Set the directory containing {\Coq} binaries to be used by {\tt coqc}. - It is equivalent to doing \texttt{export COQBIN=}{\em directory} before - launching {\tt coqc}. - -\item[{\tt -where}]\ % - - Print the location of \Coq's standard library and exit. - -\item[{\tt -config}]\ % - - Print the locations of \Coq's binaries, dependencies, and libraries, then exit. - -\item[{\tt -filteropts}]\ % - - Print the list of command line arguments that {\tt coqtop} has - recognized as options and exit. - -\item[{\tt -v}]\ % - - Print \Coq's version and exit. - -\item[{\tt -list-tags}]\ % - - Print the highlight tags known by {\Coq} as well as their currently associated - color and exit. - -\item[{\tt -h}, {\tt --help}]\ % - - Print a short usage and exit. - -\end{description} - - -\section{Compiled libraries checker ({\tt coqchk})} - -The {\tt coqchk} command takes a list of library paths as argument, described -either by their logical name or by their physical filename, which must end in -{\tt .vo}. The corresponding compiled libraries (.vo files) are searched in the -path, recursively processing the libraries they depend on. The content -of all these libraries is then type-checked. The effect of {\tt - coqchk} is only to return with normal exit code in case of success, -and with positive exit code if an error has been found. Error messages -are not deemed to help the user understand what is wrong. In the -current version, it does not modify the compiled libraries to mark -them as successfully checked. - -Note that non-logical information is not checked. By logical -information, we mean the type and optional body associated to names. -It excludes for instance anything related to the concrete syntax of -objects (customized syntax rules, association between short and long -names), implicit arguments, etc. - -This tool can be used for several purposes. One is to check that a -compiled library provided by a third-party has not been forged and -that loading it cannot introduce inconsistencies.\footnote{Ill-formed - non-logical information might for instance bind {\tt - Coq.Init.Logic.True} to short name {\tt False}, so apparently {\tt - False} is inhabited, but using fully qualified names, {\tt - Coq.Init.Logic.False} will always refer to the absurd proposition, - what we guarantee is that there is no proof of this latter - constant.} -Another point is to get an even higher level of security. Since {\tt - coqtop} can be extended with custom tactics, possibly ill-typed -code, it cannot be guaranteed that the produced compiled libraries are -correct. {\tt coqchk} is a standalone verifier, and thus it cannot be -tainted by such malicious code. - -Command-line options {\tt -Q}, {\tt -R}, {\tt -where} and -{\tt -impredicative-set} are supported by {\tt coqchk} and have the -same meaning as for {\tt coqtop}. As there is no notion of relative paths in -object files {\tt -Q} and {\tt -R} have exactly the same meaning. - -Extra options are: -\begin{description} -\item[{\tt -norec} {\em module}]\ % - - Check {\em module} but do not check its dependencies. - -\item[{\tt -admit} {\em module}]\ % - - Do not check {\em module} and any of its dependencies, unless - explicitly required. - -\item[{\tt -o}]\ % - - At exit, print a summary about the context. List the names of all - assumptions and variables (constants without body). - -\item[{\tt -silent}]\ % - - Do not write progress information in standard output. -\end{description} - -Environment variable \verb:$COQLIB: can be set to override the -location of the standard library. - -The algorithm for deciding which modules are checked or admitted is -the following: assuming that {\tt coqchk} is called with argument $M$, -option {\tt -norec} $N$, and {\tt -admit} $A$. Let us write -$\overline{S}$ the set of reflexive transitive dependencies of set -$S$. Then: -\begin{itemize} -\item Modules $C=\overline{M}\backslash\overline{A}\cup M\cup N$ are - loaded and type-checked before being added to the context. -\item And $\overline{M}\cup\overline{N}\backslash C$ is the set of - modules that are loaded and added to the context without - type-checking. Basic integrity checks (checksums) are nonetheless - performed. -\end{itemize} - -As a rule of thumb, the {\tt -admit} can be used to tell that some -libraries have already been checked. So {\tt coqchk A B} can be split -in {\tt coqchk A \&\& coqchk B -admit A} without type-checking any -definition twice. Of course, the latter is slightly slower since it -makes more disk access. It is also less secure since an attacker might -have replaced the compiled library $A$ after it has been read by the -first command, but before it has been read by the second command. - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 357272aa4..4ddb5e0f2 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -112,7 +112,6 @@ Options A and B of the licence are {\em not} elected.} %%SUPPRIME \include{RefMan-tus.v}% Writing tactics \part{Practical tools} -\include{RefMan-com}% The coq commands (coqc coqtop) \include{RefMan-uti}% utilities (gallina, do_Makefile, etc) \include{RefMan-ide}% Coq IDE diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst index 443e5c10f..507fb2297 100644 --- a/doc/sphinx/index.rst +++ b/doc/sphinx/index.rst @@ -35,6 +35,8 @@ Table of contents .. toctree:: :caption: Practical tools + practical-tools/coq-commands + .. toctree:: :caption: Addendum diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst new file mode 100644 index 000000000..1ff808894 --- /dev/null +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -0,0 +1,256 @@ +.. include:: ../replaces.rst + +.. _thecoqcommands: + +The |Coq| commands +==================== + +There are three |Coq| commands: + ++ ``coqtop``: the |Coq| toplevel (interactive mode); ++ ``coqc``: the |Coq| compiler (batch compilation); ++ ``coqchk``: the |Coq| checker (validation of compiled libraries). + + +The options are (basically) the same for the first two commands, and +roughly described below. You can also look at the ``man`` pages of +``coqtop`` and ``coqc`` for more details. + +Interactive use (coqtop) +------------------------ + +In the interactive mode, also known as the |Coq| toplevel, the user can +develop his theories and proofs step by step. The |Coq| toplevel is run +by the command ``coqtop``. + +They are two different binary images of |Coq|: the byte-code one and the +native-code one (if OCaml provides a native-code compiler for +your platform, which is supposed in the following). By default, +``coqtop`` executes the native-code version; run ``coqtop.byte`` to get +the byte-code version. + +The byte-code toplevel is based on an OCaml toplevel (to +allow dynamic linking of tactics). You can switch to the OCaml toplevel +with the command ``Drop.``, and come back to the |Coq| +toplevel with the command ``Coqloop.loop();;``. + +Batch compilation (coqc) +------------------------ + +The ``coqc`` command takes a name *file* as argument. Then it looks for a +vernacular file named *file*.v, and tries to compile it into a +*file*.vo file (See :ref:`TODO-6.5`). Warning: The name *file* should be a +regular |Coq| identifier, as defined in Section :ref:'TODO-1.1'. It should contain +only letters, digits or underscores (_). For instance, ``/bar/foo/toto.v`` is valid, but +``/bar/foo/to-to.v`` is invalid. + + +Customization at launch time +--------------------------------- + +By resource file +~~~~~~~~~~~~~~~~~~~~~~~ + +When |Coq| is launched, with either ``coqtop`` or ``coqc``, the resource file +``$XDG_CONFIG_HOME/coq/coqrc.xxx`` is loaded, where ``$XDG_CONFIG_HOME`` +is the configuration directory of the user (by default its home +directory ``/.config`` and ``xxx`` is the version number (e.g. 8.8). If +this file is not found, then the file ``$XDG_CONFIG_HOME/coqrc`` is +searched. You can also specify an arbitrary name for the resource file +(see option ``-init-file`` below). + +This file may contain, for instance, ``Add LoadPath`` commands to add +directories to the load path of |Coq|. It is possible to skip the +loading of the resource file with the option ``-q``. + + +By environment variables +~~~~~~~~~~~~~~~~~~~~~~~~~ + +Load path can be specified to the |Coq| system by setting up ``$COQPATH`` +environment variable. It is a list of directories separated by +``:`` (``;`` on Windows). |Coq| will also honor ``$XDG_DATA_HOME`` and +``$XDG_DATA_DIRS`` (see Section :ref:`TODO-2.6.3`). + +Some |Coq| commands call other |Coq| commands. In this case, they look for +the commands in directory specified by ``$COQBIN``. If this variable is +not set, they look for the commands in the executable path. + +The ``$COQ_COLORS`` environment variable can be used to specify the set +of colors used by ``coqtop`` to highlight its output. It uses the same +syntax as the ``$LS_COLORS`` variable from GNU’s ls, that is, a colon-separated +list of assignments of the form ``name=``:n:``{*; attr}`` where +``name`` is the name of the corresponding highlight tag and each ``attrᵢ`` is an +ANSI escape code. The list of highlight tags can be retrieved with the +``-list-tags`` command-line option of ``coqtop``. + +By command line options +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The following command-line options are recognized by the commands ``coqc`` +and ``coqtop``, unless stated otherwise: + +:-I *directory*, -include *directory*: Add physical path *directory* + to the OCaml loadpath. See also: :ref:`TODO-2.6.1` and the + command Declare ML Module Section :ref:`TODO-6.5`. +:-Q *directory* dirpath: Add physical path *directory* to the list of + directories where |Coq| looks for a file and bind it to the the logical + directory *dirpath*. The subdirectory structure of *directory* is + recursively available from |Coq| using absolute names (extending the + dirpath prefix) (see Section :ref:`TODO-2.6.2`).Note that only those + subdirectories and files which obey the lexical conventions of what is + an ident (see Section :ref:`TODO-1.1`) are taken into account. Conversely, the + underlying file systems or operating systems may be more restrictive + than |Coq|. While Linux’s ext4 file system supports any |Coq| recursive + layout (within the limit of 255 bytes per file name), the default on + NTFS (Windows) or HFS+ (MacOS X) file systems is on the contrary to + disallow two files differing only in the case in the same directory. + See also: Section :ref:`TODO-2.6.1`. +:-R *directory* dirpath: Do as -Q *directory* dirpath but make the + subdirectory structure of *directory* recursively visible so that the + recursive contents of physical *directory* is available from |Coq| using + short or partially qualified names. See also: Section :ref:`TODO-2.6.1`. +:-top dirpath: Set the toplevel module name to dirpath instead of Top. + Not valid for `coqc` as the toplevel module name is inferred from the + name of the output file. +:-exclude-dir *directory*: Exclude any subdirectory named *directory* + while processing options such as -R and -Q. By default, only the + conventional version control management directories named CVS + and_darcs are excluded. +:-nois: Start from an empty state instead of loading the Init.Prelude + module. +:-init-file *file*: Load *file* as the resource file instead of + loading the default resource file from the standard configuration + directories. +:-q: Do not to load the default resource file. +:-load-ml-source *file*: Load the OCaml source file *file*. +:-load-ml-object *file*: Load the OCaml object file *file*. +:-l *file*, -load-vernac-source *file*: Load and execute the |Coq| + script from *file.v*. +:-lv *file*, -load-vernac-source-verbose *file*: Load and execute the + |Coq| script from *file.v*. Output its content on the standard input as + it is executed. +:-load-vernac-object dirpath: Load |Coq| compiled library dirpath. This + is equivalent to runningRequire dirpath. +:-require dirpath: Load |Coq| compiled library dirpath and import it. + This is equivalent to running Require Import dirpath. +:-batch: Exit just after argument parsing. Available for `coqtop` only. +:-compile *file.v*: Compile file *file.v* into *file.vo*. This options + imply -batch (exit just after argument parsing). It is available only + for `coqtop`, as this behavior is the purpose of `coqc`. +:-compile-verbose *file.v*: Same as -compile but also output the + content of *file.v* as it is compiled. +:-verbose: Output the content of the input file as it is compiled. + This option is available for `coqc` only; it is the counterpart of + -compile-verbose. +:-w (all|none|w₁,…,wₙ): Configure the display of warnings. This + option expects all, none or a comma-separated list of warning names or + categories (see Section :ref:`TODO-6.9.3`). +:-color (on|off|auto): Enable or not the coloring of output of `coqtop`. + Default is auto, meaning that `coqtop` dynamically decides, depending on + whether the output channel supports ANSI escape sequences. +:-beautify: Pretty-print each command to *file.beautified* when + compiling *file.v*, in order to get old-fashioned + syntax/definitions/notations. +:-emacs, -ide-slave: Start a special toplevel to communicate with a + specific IDE. +:-impredicative-set: Change the logical theory of |Coq| by declaring the + sort Set impredicative. Warning: This is known to be inconsistent with some + standard axioms of classical mathematics such as the functional + axiom of choice or the principle of description. +:-type-in-type: Collapse the universe hierarchy of |Coq|. Warning: This makes the logic + inconsistent. +:-mangle-names *ident*: Experimental: Do not depend on this option. Replace + Coq's auto-generated name scheme with names of the form *ident0*, *ident1*, + etc. The command ``Set Mangle Names`` turns the behavior on in a document, + and ``Set Mangle Names Prefix "ident"`` changes the used prefix. This feature + s intended to be used as a linter for developments that want to be robust to + changes in the auto-generated name scheme. The options are provided to + facilitate tracking down problems. +:-compat *version*: Attempt to maintain some backward-compatibility + with a previous version. +:-dump-glob *file*: Dump references for global names in file *file* + (to be used by coqdoc, see :ref:`TODO-15.4`). By default, if *file.v* is being + compiled, *file.glob* is used. +:-no-glob: Disable the dumping of references for global names. +:-image *file*: Set the binary image to be used by `coqc` to be *file* + instead of the standard one. Not of general use. +:-bindir *directory*: Set the directory containing |Coq| binaries to be + used by `coqc`. It is equivalent to doing export COQBIN= *directory* + before launching `coqc`. +:-where: Print the location of |Coq|’s standard library and exit. +:-config: Print the locations of |Coq|’s binaries, dependencies, and + libraries, then exit. +:-filteropts: Print the list of command line arguments that `coqtop` has + recognized as options and exit. +:-v: Print |Coq|’s version and exit. +:-list-tags: Print the highlight tags known by |Coq| as well as their + currently associated color and exit. +:-h, --help: Print a short usage and exit. + +Compiled libraries checker (coqchk) +---------------------------------------- + +The ``coqchk`` command takes a list of library paths as argument, described either +by their logical name or by their physical filename, hich must end in ``.vo``. The +corresponding compiled libraries (``.vo`` files) are searched in the path, +recursively processing the libraries they depend on. The content of all these +libraries is then type-checked. The effect of ``coqchk`` is only to return with +normal exit code in case of success, and with positive exit code if an error has +been found. Error messages are not deemed to help the user understand what is +wrong. In the current version, it does not modify the compiled libraries to mark +them as successfully checked. + +Note that non-logical information is not checked. By logical +information, we mean the type and optional body associated to names. +It excludes for instance anything related to the concrete syntax of +objects (customized syntax rules, association between short and long +names), implicit arguments, etc. + +This tool can be used for several purposes. One is to check that a +compiled library provided by a third-party has not been forged and +that loading it cannot introduce inconsistencies [#]_. Another point is +to get an even higher level of security. Since ``coqtop`` can be extended +with custom tactics, possibly ill-typed code, it cannot be guaranteed +that the produced compiled libraries are correct. ``coqchk`` is a +standalone verifier, and thus it cannot be tainted by such malicious +code. + +Command-line options ``-Q``, ``-R``, ``-where`` and ``-impredicative-set`` are supported +by ``coqchk`` and have the same meaning as for ``coqtop``. As there is no notion of +relative paths in object files ``-Q`` and ``-R`` have exactly the same meaning. + +:-norec *module*: Check *module* but do not check its dependencies. +:-admit *module*: Do not check *module* and any of its dependencies, + unless explicitly required. +:-o: At exit, print a summary about the context. List the names of all + assumptions and variables (constants without body). +:-silent: Do not write progress information in standard output. + +Environment variable ``$COQLIB`` can be set to override the location of +the standard library. + +The algorithm for deciding which modules are checked or admitted is +the following: assuming that ``coqchk`` is called with argument ``M``, option +``-norec N``, and ``-admit A``. Let us write :math:`\overline{S}` for the +set of reflexive transitive dependencies of set :math:`S`. Then: + ++ Modules :math:`C = \overline{M} \backslash \overline{A} \cup M \cup N` are loaded and type-checked before being added + to the context. ++ And :math:`M \cup N \backslash C` is the set of modules that are loaded and added to the + context without type-checking. Basic integrity checks (checksums) are + nonetheless performed. + +As a rule of thumb, the -admit can be used to tell that some libraries +have already been checked. So ``coqchk A B`` can be split in ``coqchk A`` && +``coqchk B -admit A`` without type-checking any definition twice. Of +course, the latter is slightly slower since it makes more disk access. +It is also less secure since an attacker might have replaced the +compiled library ``A`` after it has been read by the first command, but +before it has been read by the second command. + +.. [#] Ill-formed non-logical information might for instance bind + Coq.Init.Logic.True to short name False, so apparently False is + inhabited, but using fully qualified names, Coq.Init.Logic.False will + always refer to the absurd proposition, what we guarantee is that + there is no proof of this latter constant. |