diff options
| -rw-r--r-- | doc/refman/RefMan-com.tex | 225 |
1 files changed, 132 insertions, 93 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 8bb1cc331..6f8584988 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -5,9 +5,9 @@ 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) +\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 @@ -39,11 +39,10 @@ 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} must be a regular {\Coq} identifier, as -defined in the Section~\ref{lexical}. It -must only contain letters, digits or underscores -(\_). Thus it can be \verb+/bar/foo/toto.v+ but cannot be -\verb+/bar/foo/to-to.v+. +\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} @@ -64,7 +63,7 @@ directories to the load path of \Coq. It is possible to skip the loading of the resource file with the option \verb:-q:. -\section{By environment variables\label{EnvVariables} +\subsection{By environment variables\label{EnvVariables} \index{Environment variables}\label{envars}} Load path can be specified to the \Coq\ system by setting up @@ -93,13 +92,13 @@ 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}]\ +\item[{\tt -I} {\em directory}, {\tt -include} {\em directory}]\ % -Add physical path {\em directory} to the {\ocaml} loadpath. + Add physical path {\em directory} to the {\ocaml} loadpath. \SeeAlso Section~\ref{Libraries} and the command {\tt Declare ML Module} Section \ref{compiled}. -\item[\texttt{-Q} \emph{directory} {\dirpath}]\ +\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 @@ -109,147 +108,184 @@ Add physical path {\em directory} to the {\ocaml} loadpath. \SeeAlso Section~\ref{Libraries}. -\item[{\tt -R} {\em directory} {\dirpath}]\ +\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}, {\tt -notop}]\ +\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 -notop}]\ % + + Use the empty logical path for the toplevel module name 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}]\ % - This sets the toplevel module name to {\dirpath}/the empty logical path instead - of {\tt Top}. Not valid for {\tt coqc}. + 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 -exclude-dir} {\em subdirectory}]\ +\item[{\tt -nois}]\ % - This tells to exclude any subdirectory named {\em subdirectory} - while processing option {\tt -R}. Without this option only the - conventional version control management subdirectories named {\tt - CVS} and {\tt \_darcs} are excluded. + Start from an empty state instead of loading the {\tt Init.Prelude} + module. -\item[{\tt -nois}]\ +\item[{\tt -init-file} {\em file}]\ % - Cause \Coq~to begin with an empty state. + Load {\em file} as the resource file instead of loading the default + resource file from the standard configuration directories. -\item[{\tt -init-file} {\em file}, {\tt -q}]\ +\item[{\tt -q}]\ % - Take {\em file} as the resource file. / - Cause \Coq~not to load the resource file. + Do not to load the default resource file. -\item[{\tt -load-ml-source} {\em file}]\ +\item[{\tt -load-ml-source} {\em file}]\ % Load the {\ocaml} source file {\em file}. -\item[{\tt -load-ml-object} {\em file}]\ +\item[{\tt -load-ml-object} {\em file}]\ % Load the {\ocaml} object file {\em file}. -\item[{\tt -l[v]} {\em file}, {\tt -load-vernac-source[-verbose]} {\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}. - Load \Coq~file {\em file}{\tt .v} optionally with copy it contents on the - standard input. +\item[{\tt -require} {\dirpath}]\ % -\item[{\tt -load-vernac-object} {\em path}]\ + Load \Coq~compiled library {\dirpath} and import it. This is equivalent + to running {\tt Require Import} {\dirpath}. - Load \Coq~compiled library {\em path} (equivalent to {\tt Require} {\em path}). +\item[{\tt -batch}]\ % -\item[{\tt -require} {\em path}]\ + Exit just after argument parsing. Available for {\tt coqtop} only. - Load \Coq~compiled library {\em path} and import it (equivalent to {\tt - Require Import} {\em path}). +\item[{\tt -compile} {\em file.v}]\ % -\item[{\tt -compile} {\em file.v},{\tt -compile-verbose} {\em file.v}, {\tt -batch}]\ + 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}. - {\tt coqtop} options only used internally by {\tt coqc}. +\item[{\tt -compile-verbose} {\em file.v}]\ % - This compiles file {\em file.v} into {\em file}{\tt .vo} without/with a - copy of the contents of the file on standard input. This option implies options - {\tt -batch} (exit just after arguments parsing). It is only - available for {\tt coqtop}. + Same as {\tt -compile} but also output the content of {\em file.v} as + it is compiled. -\item[{\tt -verbose}]\ +\item[{\tt -verbose}]\ % - This option is only for {\tt coqc}. It tells to compile the file with - a copy of its contents on standard input. + 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}. %Mostly unused in the code -%\item[{\tt -debug}]\ +%\item[{\tt -debug}]\ % % % Switch on the debug flag. -\item[{\tt -with-geoproof} (yes|no)]\ +\item[{\tt -with-geoproof} (yes|no)]\ % - Activate or not special functions for Geoproof within {\CoqIDE} (default is yes). + Enable or not special functions for Geoproof within {\CoqIDE} (default + is yes). -\item[{\tt -color} (on|off|auto)]\ +\item[{\tt -color} (on|off|auto)]\ % - Activate or not the coloring of output of {\tt coqtop}. The default, auto, - means that {\tt coqtop} will dynamically decide whether to activate it - depending if the output channels of {\tt coqtop} can handle ANSI styles. + 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}]\ +\item[{\tt -beautify}]\ % - While compiling {\em file}, pretty prints each command just after having parsing - it in {\em file}{\tt .beautified} in order to get old-fashion - syntax/definitions/notations. + 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}]\ +\item[{\tt -emacs}, {\tt -ide-slave}]\ % - Start a special main loop to communicate with ide. + Start a special toplevel to communicate with a specific IDE. -\item[{\tt -impredicative-set}]\ +\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 + 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 + axiom of choice or the principle of description. -\item[{\tt -type-in-type}]\ +\item[{\tt -type-in-type}]\ % - This collapses the universe hierarchy of {\Coq} making the logic inconsistent. + Collapse the universe hierarchy of {\Coq}. Warning: this makes the + logic inconsistent. -\item[{\tt -compat} {\em version}] \mbox{} +\item[{\tt -compat} {\em version}]\ % - Attempt to maintain some of the incompatible changes in their {\em version} - behavior. + Attempt to maintain some backward-compatibility with a previous version. -\item[{\tt -dump-glob} {\em file}]\ +\item[{\tt -dump-glob} {\em file}]\ % - This dumps references for global names in file {\em file} - (to be used by coqdoc, see~\ref{coqdoc}) + 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-hash-consing}] \mbox{} +\item[{\tt -no-glob}]\ % -\item[{\tt -image} {\em file}]\ + Disable the dumping of references for global names. - This option sets the binary image to be used by {\tt coqc} to be {\em file} +%\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}]\ +\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. - Set for {\tt coqc} the directory containing \Coq\ binaries. - It is equivalent to do \texttt{export COQBIN=}{\em directory} - before launching {\tt coqc}. +\item[{\tt -config}]\ % -\item[{\tt -where}, {\tt -config}, {\tt -filteropts}]\ + Print the locations of \Coq's binaries, dependencies, and libraries, then exit. - Print the \Coq's standard library location or \Coq's binaries, dependencies, - libraries locations or the list of command line arguments that {\tt coqtop} has - recognize as options and exit. +\item[{\tt -filteropts}]\ % -\item[{\tt -v}]\ + Print the list of command line arguments that {\tt coqtop} has + recognized as options and exit. - Print the \Coq's version and exit. +\item[{\tt -v}]\ % -\item[{\tt -list-tags}]\ + Print \Coq's version and exit. - Print the highlight tags known by \Coq as well as their currently associated - color. +\item[{\tt -list-tags}]\ % -\item[{\tt -h}, {\tt --help}]\ + 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. @@ -293,18 +329,21 @@ Command-line options {\tt -I}, {\tt -R}, {\tt -where} and {\tt -impredicative-set} are supported by {\tt coqchk} and have the same meaning as for {\tt coqtop}. Extra options are: \begin{description} -\item[{\tt -norec} $module$]\ +\item[{\tt -norec} {\em module}]\ % + + Check {\em module} but do not check its dependencies. - Check $module$ but do not force check of its dependencies. -\item[{\tt -admit} $module$] \ +\item[{\tt -admit} {\em module}]\ % - Do not check $module$ and any of its dependencies, unless + Do not check {\em module} and any of its dependencies, unless explicitly required. -\item[{\tt -o}]\ + +\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}]\ + +\item[{\tt -silent}]\ % Do not write progress information in standard output. \end{description} |