There are two Coq commands:
-
coqtop: The Coq toplevel (interactive mode) ;
- coqc : The Coq compiler (batch compilation).
The options are (basically) the same for the two commands, and
roughly described below. You can also look at the man pages of
coqtop and coqc for more details.
12.1 Interactive use (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 coqtop.
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
coqtop or coqc, the native-code version of the system is
used. The command-line options -byte and -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 Drop., and come back to the
Coq toplevel with the command Toplevel.loop();;.
12.2 Batch compilation (coqc)
The coqc command takes a name file as argument. Then it
looks for a vernacular file named file.v, and tries to
compile it into a file.vo file (See 6.4).
Warning: The name file must be a regular Coq identifier, as
defined in the section 1.1. It
must only contain letters, digits or underscores
(_). Thus it can be /bar/foo/toto.v but cannot be
/bar/foo/to-to.v .
Notice that the -byte and -opt options are still
available with coqc and allow you to select the byte-code or
native-code versions of the system.
12.3 Resource file
When Coq is launched, with either coqtop or coqc, the
resource file $HOME/.coqrc.7.0 is loaded, where $HOME is
the home directory of the user. If this file is not found, then the
file $HOME/.coqrc is searched. You can also specify an
arbitrary name for the resource file (see option -init-file
below), or the name of another user to load the resource file of
someone else (see option -user).
This file may contain, for instance, 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 -q.
12.4 Environment variables
There are three environment variables used by the Coq system.
$COQBIN for the directory where the binaries are,
$COQLIB for the directory whrer the standard library is, and
$COQTOP for the directory of the sources. The latter is useful
only for developers that are writing their own tactics and are using
coq_makefile (see 13.3). If $COQBIN or
$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.
The following command-line options are recognized by the commands coqc and coqtop:
-
-byte
-
Run the byte-code version of Coq.
- -opt
-
Run the native-code version of Coq.
- -I directory, -include directory
-
Add directory to the searched directories when looking for a
file.
- -R directory dirpath
-
This maps the subdirectory structure of physical directory to
logical dirpath and adds directory and its subdirectories
to the searched directories when looking for a file.
- -is file, -inputstate file
-
Cause Coq to use the state put in the file file as its input
state. The default state is initial.coq.
Mainly useful to build the standard input state.
- -nois
-
Cause Coq to begin with an empty state. Mainly useful to build the
standard input state.
- -notactics
-
Forbid the dynamic loading of tactics.
- -init-file file
-
Take file as the resource file.
- -q
-
Cause Coq not to load the resource file.
- -user username
-
Take resource file of user username (that is
~username/.coqrc.7.0) instead of yours.
- -load-ml-source file
-
Load the Caml source file file.
- -load-ml-object file
-
Load the Caml object file file.
- -load-vernac-source file
-
Load Coq file file.v
- -load-vernac-object file
-
Load Coq compiled file file.vo
- -require file
-
Load Coq compiled file file.vo and import it (Require file).
- -compile file
-
This compiles file file.v into file.vo.
This option implies options -batch and -silent. It is
only available for coqtop.
- -batch
-
Batch mode : exit just after arguments parsing. This option is only
used by coqc.
- -debug
-
Switch on the debug flag.
- -xml
-
This option is for use with coqc. It tells Coq to export on
the standard output the content of the compiled file into XML format.
- -emacs
-
Tells Coq it is executed under Emacs.
- -db
-
Launch Coq under the Objective Caml debugger (provided that Coq
has been compiled for debugging; see next chapter).
- -impredicative-set
-
Change the logical theory of Coq by declaring the sort 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
- -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.
- -image file
-
This option sets the binary image to be used to be file
instead of the standard one. Not of general use.
- -bindir directory
-
Set the directory containing Coq binaries.
It is equivalent to do export COQBIN=directory
before lauching Coq.
- -libdir file
-
Set the directory containing Coq libraries.
It is equivalent to do export COQLIB=directory
before lauching Coq.
- -where
-
Print the Coq's standard library location and exit.
- -v
-
Print the Coq's version and exit.
- -h, --help
-
Print a short usage and exit.