1
\chapter{The \Coq~commands}\label{Addoc-coqc}
5
There are two \Coq~commands:
7
\item {\tt coqtop}: The \Coq\ toplevel (interactive mode) ;
8
\item {\tt coqc} : The \Coq\ compiler (batch compilation).
10
The options are (basically) the same for the two commands, and
11
roughly described below. You can also look at the \verb!man! pages of
12
\verb!coqtop! and \verb!coqc! for more details.
15
\section{Interactive use ({\tt coqtop})}
17
In the interactive mode, also known as the \Coq~toplevel, the user can
18
develop his theories and proofs step by step. The \Coq~toplevel is
19
run by the command {\tt coqtop}.
24
They are two different binary images of \Coq: the byte-code one and
25
the native-code one (if Objective Caml provides a native-code compiler
26
for your platform, which is supposed in the following). When invoking
27
\verb!coqtop! or \verb!coqc!, the native-code version of the system is
28
used. The command-line options \verb!-byte! and \verb!-opt! explicitly
29
select the byte-code and the native-code versions, respectively.
31
The byte-code toplevel is based on a Caml
32
toplevel (to allow the dynamic link of tactics). You can switch to
33
the Caml toplevel with the command \verb!Drop.!, and come back to the
34
\Coq~toplevel with the command \verb!Toplevel.loop();;!.
36
% The command \verb!coqtop -searchisos! runs the search tool {\sf
37
% Coq\_SearchIsos} (see section~\ref{coqsearchisos},
38
% page~\pageref{coqsearchisos}) and, as the \Coq~system, can be combined
39
% with the option \verb!-opt!.
41
\section{Batch compilation ({\tt coqc})}
42
The {\tt coqc} command takes a name {\em file} as argument. Then it
43
looks for a vernacular file named {\em file}{\tt .v}, and tries to
44
compile it into a {\em file}{\tt .vo} file (See ~\ref{compiled}).
46
\Warning The name {\em file} must be a regular {\Coq} identifier, as
47
defined in the section \ref{lexical}. It
48
must only contain letters, digits or underscores
49
(\_). Thus it can be \verb+/bar/foo/toto.v+ but cannot be
50
\verb+/bar/foo/to-to.v+ .
52
Notice that the \verb!-byte! and \verb!-opt! options are still
53
available with \verb!coqc! and allow you to select the byte-code or
54
native-code versions of the system.
57
\section{Resource file}
60
When \Coq\ is launched, with either {\tt coqtop} or {\tt coqc}, the
61
resource file \verb:$HOME/.coqrc.7.0: is loaded, where \verb:$HOME: is
62
the home directory of the user. If this file is not found, then the
63
file \verb:$HOME/.coqrc: is searched. You can also specify an
64
arbitrary name for the resource file (see option \verb:-init-file:
65
below), or the name of another user to load the resource file of
66
someone else (see option \verb:-user:).
68
This file may contain, for instance, \verb:Add LoadPath: commands to add
69
directories to the load path of \Coq.
70
It is possible to skip the loading of the resource file with the
73
\section{Environment variables}
75
\index{Environment variables}
77
There are three environment variables used by the \Coq\ system.
78
\verb:$COQBIN: for the directory where the binaries are,
79
\verb:$COQLIB: for the directory whrer the standard library is, and
80
\verb:$COQTOP: for the directory of the sources. The latter is useful
81
only for developers that are writing their own tactics and are using
82
\texttt{coq\_makefile} (see \ref{Makefile}). If \verb:$COQBIN: or
83
\verb:$COQLIB: are not defined, \Coq\ will use the default values
84
(defined at installation time). So these variables are useful only if
85
you move the \Coq\ binaries and library after installation.
88
\index{Options of the command line}
91
The following command-line options are recognized by the commands {\tt
92
coqc} and {\tt coqtop}, unless stated otherwise:
97
Run the byte-code version of \Coq{}.
101
Run the native-code version of \Coq{}.
103
\item[{\tt -I} {\em directory}, {\tt -include} {\em directory}]\
105
Add {\em directory} to the searched directories when looking for a
108
\item[{\tt -R} {\em directory} {\dirpath}]\
110
This maps the subdirectory structure of physical {\em directory} to
111
logical {\dirpath} and adds {\em directory} and its subdirectories
112
to the searched directories when looking for a file.
114
\item[{\tt -top} {\dirpath}]\
116
This sets the toplevel module name to {\dirpath} instead of {\tt
117
Top}. Not valid for {\tt coqc}.
119
\item[{\tt -is} {\em file}, {\tt -inputstate} {\em file}]\
121
Cause \Coq~to use the state put in the file {\em file} as its input
122
state. The default state is {\em initial.coq}.
123
Mainly useful to build the standard input state.
125
\item[{\tt -outputstate} {\em file}]\
127
Cause \Coq~to dump its state to file {\em file}.coq just after finishing
128
parsing and evaluating all the arguments from the command line.
132
Cause \Coq~to begin with an empty state. Mainly useful to build the
133
standard input state.
137
%\item[{\tt -notactics}]\
139
% Forbid the dynamic loading of tactics in the bytecode version of {\Coq}.
141
\item[{\tt -init-file} {\em file}]\
143
Take {\em file} as the resource file.
147
Cause \Coq~not to load the resource file.
149
\item[{\tt -user} {\em username}]\
151
Take resource file of user {\em username} (that is
152
\verb+~+{\em username}{\tt /.coqrc.7.0}) instead of yours.
154
\item[{\tt -load-ml-source} {\em file}]\
156
Load the Caml source file {\em file}.
158
\item[{\tt -load-ml-object} {\em file}]\
160
Load the Caml object file {\em file}.
162
\item[{\tt -l} {\em file}, {\tt -load-vernac-source} {\em file}]\
164
Load \Coq~file {\em file}{\tt .v}
166
\item[{\tt -lv} {\em file}, {\tt -load-vernac-source-verbose} {\em file}]\
168
Load \Coq~file {\em file}{\tt .v} with
169
a copy of the contents of the file on standard input.
171
\item[{\tt -load-vernac-object} {\em file}]\
173
Load \Coq~compiled file {\em file}{\tt .vo}
175
%\item[{\tt -preload} {\em file}]\ \\
176
%Add {\em file}{\tt .vo} to the files to be loaded and opened
177
%before making the initial state.
179
\item[{\tt -require} {\em file}]\
181
Load \Coq~compiled file {\em file}{\tt .vo} and import it ({\tt
182
Require} {\em file}).
184
\item[{\tt -compile} {\em file}]\
186
This compiles file {\em file}{\tt .v} into {\em file}{\tt .vo}.
187
This option implies options {\tt -batch} and {\tt -silent}. It is
188
only available for {\tt coqtop}.
190
\item[{\tt -compile-verbose} {\em file}]\
192
This compiles file {\em file}{\tt .v} into {\em file}{\tt .vo} with
193
a copy of the contents of the file on standard input.
194
This option implies options {\tt -batch} and {\tt -silent}. It is
195
only available for {\tt coqtop}.
197
\item[{\tt -verbose}]\
199
This option is only for {\tt coqc}. It tells to compile the file with
200
a copy of its contents on standard input.
204
Batch mode : exit just after arguments parsing. This option is only
207
%Mostly unused in the code
208
%\item[{\tt -debug}]\
210
% Switch on the debug flag.
214
This option is for use with {\tt coqc}. It tells \Coq\ to export on
215
the standard output the content of the compiled file into XML format.
217
\item[{\tt -quality}]
219
Improve the legibility of the proof terms produced by some tactics.
223
Tells \Coq\ it is executed under Emacs.
225
\item[{\tt -impredicative-set}]\
227
Change the logical theory of {\Coq} by declaring the sort {\tt Set}
228
impredicative; warning: this is known to be inconsistent with
229
some standard axioms of classical mathematics such as the functional
230
axiom of choice or the principle of description
232
\item[{\tt -dump-glob} {\em file}]\
234
This dumps references for global names in file {\em file}
235
(to be used by coqdoc, see~\ref{coqdoc})
237
\item[{\tt -dont-load-proofs}]\
239
This avoids loading in memory the proofs of opaque theorems
240
resulting in a smaller memory requirement and faster compilation;
241
warning: this invalidates some features such as the extraction tool.
245
This activates the use of the bytecode-based conversion algorithm
246
for the current session (see section~\ref{SetVirtualMachine}).
248
\item[{\tt -image} {\em file}]\
250
This option sets the binary image to be used to be {\em file}
251
instead of the standard one. Not of general use.
253
\item[{\tt -bindir} {\em directory}]\
255
Set for {\tt coqc} the directory containing \Coq\ binaries.
256
It is equivalent to do \texttt{export COQBIN=}{\em directory}
257
before lauching {\tt coqc}.
261
Print the \Coq's standard library location and exit.
265
Print the \Coq's version and exit.
267
\item[{\tt -h}, {\tt --help}]\
269
Print a short usage and exit.
273
% {\tt coqtop} has an additional option:
275
% \begin{description}
276
% \item[{\tt -searchisos}]\ \\
277
% Launch the {\sf Coq\_SearchIsos} toplevel
278
% (see section~\ref{coqsearchisos}, page~\pageref{coqsearchisos}).
281
% $Id: RefMan-com.tex 9044 2006-07-12 13:22:17Z herbelin $
285
%%% TeX-master: "Reference-Manual"
added
removed
refman/RefMan-com.tex
