diff options
Diffstat (limited to 'doc/refman/RefMan-com.tex')
| -rw-r--r-- | doc/refman/RefMan-com.tex | 358 |
1 files changed, 0 insertions, 358 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex deleted file mode 100644 index bcc68c78..00000000 --- a/doc/refman/RefMan-com.tex +++ /dev/null @@ -1,358 +0,0 @@ -\chapter[The \Coq~commands]{The \Coq~commands\label{Addoc-coqc} -\ttindex{coqtop} -\ttindex{coqc}} - -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 Objective Caml provides a native-code compiler -for your platform, which is supposed in the following). When invoking -\verb!coqtop! or \verb!coqc!, the native-code version of the system is -used. The command-line options \verb!-byte! and \verb!-opt! explicitly -select the byte-code and the native-code versions, respectively. - -The byte-code toplevel is based on a Caml -toplevel (to allow the dynamic link of tactics). You can switch to -the Caml toplevel with the command \verb!Drop.!, and come back to the -\Coq~toplevel with the command \verb!Toplevel.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} 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+ . - -Notice that the \verb!-byte! and \verb!-opt! options are still -available with \verb!coqc! and allow you to select the byte-code or -native-code versions of the system. - -\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:. - -\section{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 honour \verb:$XDG_DATA_HOME: and \verb:$XDG_DATA_DIRS: (see -\url{http://standards.freedesktop.org/basedir-spec/basedir-spec-latest.html}). -\Coq adds \verb:${XDG_DATA_HOME}/coq: and \verb:${XDG_DATA_DIRS}/coq: to its -search path. - -\subsection{By command line options\index{Options of the command line} -\label{vmoption} -\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}[ {\tt -as} {\em dirpath}]]\ - -Add physical path {\em directory} to the list of directories where to look for a -file and bind it to the empty logical directory/the logical directory {\em - dirpath}. The sub-directory structure of {\em directory} is recursively available -from {\Coq} using absolute names (extending the {\dirpath} prefix) (see -Section~\ref{LongNames}). - - \SeeAlso {\tt Add LoadPath} in Section~\ref{AddLoadPath} and logical - paths in Section~\ref{Libraries}. - -\item[{\tt -R} {\em directory} {\dirpath}, {\tt -R} {\em directory} [{\tt -as} {\dirpath}]]\ - - Do as {\tt -I} {\em directory} {\tt -as} {\dirpath} but make the - sub-directory structure of {\em directory} recursively visible so - that the recursive contents of physical {\em directory} is available - from {\Coq} using short or partially qualified names. - - \SeeAlso {\tt Add Rec LoadPath} in Section~\ref{AddRecLoadPath} and logical - paths in Section~\ref{Libraries}. - -\item[{\tt -top} {\dirpath}, {\tt -notop}]\ - - This sets the toplevel module name to {\dirpath}/the empty logical path instead - of {\tt Top}. Not valid for {\tt coqc}. - -\item[{\tt -exclude-dir} {\em subdirectory}]\ - - This tells to exclude any sub-directory named {\em subdirectory} - while processing option {\tt -R}. Without this option only the - conventional version control management sub-directories named {\tt - CVS} and {\tt \_darcs} are excluded. - -\item[{\tt -is} {\em file}, {\tt -inputstate} {\em file}, {\tt -outputstate} {\em file}]\ - - Load at the beginning/Dump at the end a \Coq{} state from the file {\em file}. - - Incompatible with some not purely functional aspect of the code - -\item[{\tt -nois}]\ - - Cause \Coq~to begin with an empty state. - -\item[{\tt -init-file} {\em file}, {\tt -q}]\ - - Take {\em file} as the resource file. / - Cause \Coq~not to load the resource file. - -\item[{\tt -load-ml-source} {\em file}]\ - - Load the Caml source file {\em file}. - -\item[{\tt -load-ml-object} {\em file}]\ - - Load the Caml object file {\em file}. - -\item[{\tt -l[v]} {\em file}, {\tt -load-vernac-source[-verbose]} {\em file}]\ - - Load \Coq~file {\em file}{\tt .v} optionally with copy it contents on the - standard input. - -\item[{\tt -load-vernac-object} {\em file}]\ - - Load \Coq~compiled file {\em file}{\tt .vo} - -\item[{\tt -require} {\em file}]\ - - Load \Coq~compiled file {\em file}{\tt .vo} and import it ({\tt - Require} {\em file}). - -\item[{\tt -compile} {\em file},{\tt -compile-verbose} {\em file}, {\tt -batch}]\ - - {\tt coqtop} options only used internally by {\tt coqc}. - - This compiles file {\em file}{\tt .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}. - -\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. - -%Mostly unused in the code -%\item[{\tt -debug}]\ -% -% Switch on the debug flag. - -\item[{\tt -xml}]\ - - This option is for use with {\tt coqc}. It tells \Coq\ to export on - the standard output the content of the compiled file into XML format. - -\item[{\tt -with-geoproof} (yes|no)]\ - - Activate or not special functions for Geoproof within Coqide (default is yes). - -\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. - -\item[{\tt -quality}] - - Improve the legibility of the proof terms produced by some tactics. - -\item[{\tt -emacs}, {\tt -ide-slave}]\ - - Start a special main loop to communicate with 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 -compat} {\em version}] \null - - Attempt to maintain some of the incompatible changes in their {\em version} - behavior. - -\item[{\tt -dump-glob} {\em file}]\ - - This dumps references for global names in file {\em file} - (to be used by coqdoc, see~\ref{coqdoc}) - -\item[{\tt -dont-load-proofs}]\ - - Warning: this is an unsafe mode. - Instead of loading in memory the proofs of opaque theorems, they are - treated as axioms. This results in smaller memory requirement and - faster compilation, but the behavior of the system might slightly change - (for instance during module subtyping), and some features won't be - available (for example {\tt Print Assumptions}). - -\item[{\tt -lazy-load-proofs}]\ - - This is the default behavior. Proofs of opaque theorems aren't - loaded immediately in memory, but only when necessary, for instance - during some module subtyping or {\tt Print Assumptions}. This should be - almost as fast and efficient as {\tt -dont-load-proofs}, with none - of its drawbacks. - -\item[{\tt -force-load-proofs}]\ - - Proofs of opaque theorems are loaded in memory as soon as the - corresponding {\tt Require} is done. This used to be Coq's default behavior. - -\item[{\tt -no-hash-consing}] \null - -\item[{\tt -vm}]\ - - This activates the use of the bytecode-based conversion algorithm - for the current session (see Section~\ref{SetVirtualMachine}). - -\item[{\tt -image} {\em file}]\ - - This option sets 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 for {\tt coqc} the directory containing \Coq\ binaries. - It is equivalent to do \texttt{export COQBIN=}{\em directory} - before launching {\tt coqc}. - -\item[{\tt -where}, {\tt -config}, {\tt -filteropts}]\ - - 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 -v}]\ - - Print the \Coq's version 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. -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 -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$]\ - - Check $module$ but do not force check of its dependencies. -\item[{\tt -admit} $module$] \ - - Do not check $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: |