[Sphinx] Move chapter 14 to new infrastructure

1 files changed, 402 insertions, 0 deletions

diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
new file mode 100644
index 000000000..5b73ac00a
--- /dev/null
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -0,0 +1,402 @@
+\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: