diff options
Diffstat (limited to 'doc/refman/RefMan-com.tex')
-rw-r--r-- | doc/refman/RefMan-com.tex | 280 |
1 files changed, 280 insertions, 0 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex new file mode 100644 index 00000000..f8a7546f --- /dev/null +++ b/doc/refman/RefMan-com.tex @@ -0,0 +1,280 @@ +\chapter{The \Coq~commands}\label{Addoc-coqc} +\ttindex{coqtop} +\ttindex{coqc} + +There are two \Coq~commands: +\begin{itemize} +\item {\tt coqtop}: The \Coq\ toplevel (interactive mode) ; +\item {\tt coqc} : The \Coq\ compiler (batch compilation). +\end{itemize} +The options are (basically) the same for the 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();;!. + +% The command \verb!coqtop -searchisos! runs the search tool {\sf +% Coq\_SearchIsos} (see section~\ref{coqsearchisos}, +% page~\pageref{coqsearchisos}) and, as the \Coq~system, can be combined +% with the option \verb!-opt!. + +\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{Resource file} +\index{Resource file} + +When \Coq\ is launched, with either {\tt coqtop} or {\tt coqc}, the +resource file \verb:$HOME/.coqrc.7.0: is loaded, where \verb:$HOME: is +the home directory of the user. If this file is not found, then the +file \verb:$HOME/.coqrc: is searched. You can also specify an +arbitrary name for the resource file (see option \verb:-init-file: +below), or the name of another user to load the resource file of +someone else (see option \verb:-user:). + +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{Environment variables} +\label{EnvVariables} +\index{Environment variables} + +There are three environment variables used by the \Coq\ system. +\verb:$COQBIN: for the directory where the binaries are, +\verb:$COQLIB: for the directory whrer the standard library is, and +\verb:$COQTOP: for the directory of the sources. The latter is useful +only for developers that are writing their own tactics and are using +\texttt{coq\_makefile} (see \ref{Makefile}). If \verb:$COQBIN: or +\verb:$COQLIB: are not defined, \Coq\ will use the default values +(defined at installation time). So these variables are useful only if +you move the \Coq\ binaries and library after installation. + +\section{Options} +\index{Options of the command line} + +The following command-line options are recognized by the commands {\tt + coqc} and {\tt coqtop}, unless stated otherwise: + +\begin{description} +\item[{\tt -byte}]\ + + Run the byte-code version of \Coq{}. + +\item[{\tt -opt}]\ + + Run the native-code version of \Coq{}. + +\item[{\tt -I} {\em directory}, {\tt -include} {\em directory}]\ + + Add {\em directory} to the searched directories when looking for a + file. + +\item[{\tt -R} {\em directory} {\dirpath}]\ + + This maps the subdirectory structure of physical {\em directory} to + logical {\dirpath} and adds {\em directory} and its subdirectories + to the searched directories when looking for a file. + +\item[{\tt -top} {\dirpath}]\ + + This sets the toplevel module name to {\dirpath} instead of {\tt + Top}. Not valid for {\tt coqc}. + +\item[{\tt -is} {\em file}, {\tt -inputstate} {\em file}]\ + + Cause \Coq~to use the state put in the file {\em file} as its input + state. The default state is {\em initial.coq}. + Mainly useful to build the standard input state. + +\item[{\tt -outputstate} {\em file}]\ + + Cause \Coq~to dump its state to file {\em file}.coq just after finishing + parsing and evaluating all the arguments from the command line. + +\item[{\tt -nois}]\ + + Cause \Coq~to begin with an empty state. Mainly useful to build the + standard input state. + +%Obsolete? +% +%\item[{\tt -notactics}]\ +% +% Forbid the dynamic loading of tactics in the bytecode version of {\Coq}. + +\item[{\tt -init-file} {\em file}]\ + + Take {\em file} as the resource file. + +\item[{\tt -q}]\ + + Cause \Coq~not to load the resource file. + +\item[{\tt -user} {\em username}]\ + + Take resource file of user {\em username} (that is + \verb+~+{\em username}{\tt /.coqrc.7.0}) instead of yours. + +\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} {\em file}, {\tt -load-vernac-source} {\em file}]\ + + Load \Coq~file {\em file}{\tt .v} + +\item[{\tt -lv} {\em file}, {\tt -load-vernac-source-verbose} {\em file}]\ + + Load \Coq~file {\em file}{\tt .v} with + a copy of the contents of the file on standard input. + +\item[{\tt -load-vernac-object} {\em file}]\ + + Load \Coq~compiled file {\em file}{\tt .vo} + +%\item[{\tt -preload} {\em file}]\ \\ +%Add {\em file}{\tt .vo} to the files to be loaded and opened +%before making the initial state. +% +\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}]\ + + This compiles file {\em file}{\tt .v} into {\em file}{\tt .vo}. + This option implies options {\tt -batch} and {\tt -silent}. It is + only available for {\tt coqtop}. + +\item[{\tt -compile-verbose} {\em file}]\ + + This compiles file {\em file}{\tt .v} into {\em file}{\tt .vo} with + a copy of the contents of the file on standard input. + This option implies options {\tt -batch} and {\tt -silent}. 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. + +\item[{\tt -batch}]\ + + Batch mode : exit just after arguments parsing. This option is only + used by {\tt coqc}. + +%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 -quality}] + + Improve the legibility of the proof terms produced by some tactics. + +\item[{\tt -emacs}]\ + + Tells \Coq\ it is executed under Emacs. + +\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 -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}]\ + + This avoids loading in memory the proofs of opaque theorems + resulting in a smaller memory requirement and faster compilation; + warning: this invalidates some features such as the extraction tool. + +\item[{\tt -image} {\em file}]\ + + This option sets the binary image to be used 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 lauching {\tt coqc}. + +\item[{\tt -where}]\ + + Print the \Coq's standard library location 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} + +% {\tt coqtop} has an additional option: + +% \begin{description} +% \item[{\tt -searchisos}]\ \\ +% Launch the {\sf Coq\_SearchIsos} toplevel +% (see section~\ref{coqsearchisos}, page~\pageref{coqsearchisos}). +% \end{description} + +% $Id: RefMan-com.tex 8609 2006-02-24 13:32:57Z notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty $ + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "Reference-Manual" +%%% End: |