1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
|
\chapter{The \Coq~commands}\label{Addoc-coqc}
\ttindex{coqtop}
\ttindex{coqc}
There are two \Coq~commands:
\bigskip
\begin{tabular}{l@{\quad:\quad}l}
-- {\tt coqtop} & The \Coq\ toplevel (interactive mode) ; \\[1em]
-- {\tt coqc} & The \Coq\ compiler (batch compilation).
\end{tabular}
\bigskip
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
ran by the command {\tt coqtop}.
\index{byte-code}
\index{native code}
\label{binary-images}
They are three different binary images of \Coq: the byte-code one,
the native-code one and the full native-code one. When invoking
\verb!coqtop!, the byte-code version of the system is used. The
command \verb!coqtop -opt! runs a native-code version of the
\Coq~system, and the command \verb!coqtop -full! a native-code version
with the implementation code of all the tactics (that is with the code
of the tactics \verb!Linear!, \verb!Ring! and \verb!Omega! which then
can be required by \verb=Require=) and tools (\verb!Extraction! and
\verb!Natural! which again become available through the command
\verb=Require=). Those toplevels are significantly faster than the
byte-code one. Notice that it is no longer possible to access the
Caml toplevel, neither to load tactics.
This 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!Coqtoplevel.go();;!.
% 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}).
With the \verb!-i! option, it compiles the specification module {\em
file}{\tt .vi}.
\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 not
\verb+/bar/foo/to-to+ .
Notice that the \verb!-opt! and \verb!-full! options are still
available with \verb!coqc! and allow you to compile \Coq\ files with
an efficient version 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:AddPath: commands to add
directories to the load path of \Coq. You can use the environment
variable \verb:$COQLIB: which refer to the \Coq\
library. Remember that the
default load path already contains the following directories:
\begin{verbatim}
.
$CAMLP4LIB
$COQLIB/tactics/tcc
$COQLIB/tactics/programs/EXAMPLES
$COQLIB/tactics/programs
$COQLIB/tactics/contrib/polynom
$COQLIB/tactics/contrib/omega
$COQLIB/tactics/contrib/natural
$COQLIB/tactics/contrib/linear
$COQLIB/tactics/contrib/extraction
$COQLIB/tactics/contrib/acdsimpl/simplify_rings
$COQLIB/tactics/contrib/acdsimpl/simplify_naturals
$COQLIB/tactics/contrib/acdsimpl/acd_simpl_def
$COQLIB/tactics/contrib/acdsimpl
$COQLIB/tactics/contrib
$COQLIB/theories/ZARITH
$COQLIB/theories/TREES
$COQLIB/theories/TESTS
$COQLIB/theories/SORTING
$COQLIB/theories/SETS
$COQLIB/theories/RELATIONS/WELLFOUNDED
$COQLIB/theories/RELATIONS
$COQLIB/theories/LOGIC
$COQLIB/theories/LISTS
$COQLIB/theories/INIT
$COQLIB/theories/DEMOS/PROGRAMS
$COQLIB/theories/DEMOS/OMEGA
$COQLIB/theories/DEMOS
$COQLIB/theories/BOOL
$COQLIB/theories/REALS
$COQLIB/theories/ARITH
$COQLIB/tactics
$COQLIB/states
\end{verbatim}
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 3 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 developpers that are writing there own tactics using
\texttt{coq\_makefile} (see \ref{Makefile}). If \verb:$COQBIN: or
\verb:$COQLIB: are not defined, \Coq\ will use the default values
(choosen at installation time). So these variables are useful onlt 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}:
\begin{description}
\item[{\tt -opt}]\ \\
Run the native-code version of \Coq{} (or {\sf Coq\_SearchIsos} for {\tt
coqtop}).
\item[{\tt -full}]\ \\
Run a native-code version of {\Coq} with all tactics.
\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}]\ \\
Add recursively {\em directory} to the searched directories when looking for
a file.
\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 tactics.coq}.
Mainly useful to build the standard input state.
\item[{\tt -nois}]\ \\
Cause \Coq~to begin with an empty state. Mainly useful to build the
standard input state.
\item[{\tt -notactics}]\ \\
Forbid the dynamic loading of tactics, and start on the input state
{\em state.coq}.
\item[{\tt -init-file} {\em file}]\ \\
Take {\em file} as resource file, instead of {\tt \$HOME/.coqrc.7.0}.
\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 -load-vernac-source} {\em file}]\ \\
Load \Coq~file {\em file}{\tt .v}
\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 -batch}]\ \\
Batch mode : exit just after arguments parsing. This option is only
used by {\tt coqc}.
\item[{\tt -debug}]\ \\
Switch on the debug flag.
\item[{\tt -emacs}]\ \\
Tells \Coq\ it is executed under Emacs.
\item[{\tt -db}]\ \\
Launch \Coq\ under the Objective Caml debugger (provided that \Coq\
has been compiled for debugging; see next chapter).
\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}]\ \\
It is equivalent to do \texttt{export COQBIN=}{\em directory}
before lauching \Coq.
\item[{\tt -libdir} {\em file}]\ \\
It is equivalent to do \texttt{export COQLIB=}{\em directory}
before lauching \Coq.
\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} owns an additional option:
\begin{description}
\item[{\tt -searchisos}]\ \\
Launch the {\sf Coq\_SearchIsos} toplevel
(see section~\ref{coqsearchisos}, page~\pageref{coqsearchisos}).
\end{description}
See the manual pages for more details.
% $Id$
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End:
|
