There are two Coq commands:
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.
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();;.
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.
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.
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, unless stated otherwise:
Run the byte-code version of Coq.
Run the native-code version of Coq.
Add directory to the searched directories when looking for a file.
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.
This sets the toplevel module name to dirpath instead of Top. Not valid for coqc.
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.
Cause Coq to dump its state to file file.coq just after finishing parsing and evaluating all the arguments from the command line.
Cause Coq to begin with an empty state. Mainly useful to build the standard input state.
Take file as the resource file.
Cause Coq not to load the resource file.
Take resource file of user username (that is
~username/.coqrc.7.0) instead of yours.
Load the Caml source file file.
Load the Caml object file file.
Load Coq file file.v
Load Coq file file.v with a copy of the contents of the file on standard input.
Load Coq compiled file file.vo
Load Coq compiled file file.vo and import it (Require file).
This compiles file file.v into file.vo. This option implies options -batch and -silent. It is only available for coqtop.
This compiles file file.v into file.vo with a copy of the contents of the file on standard input. This option implies options -batch and -silent. It is only available for coqtop.
This option is only for coqc. It tells to compile the file with a copy of its contents on standard input.
Batch mode : exit just after arguments parsing. This option is only used by coqc.
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.
Improve the legibility of the proof terms produced by some tactics.
Tells Coq it is executed under Emacs.
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
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.
This activates the use of the bytecode-based conversion algorithm for the current session (see Section 6.9.1).
This option sets the binary image to be used to be file instead of the standard one. Not of general use.
Set for coqc the directory containing Coq binaries. It is equivalent to do export COQBIN=directory before lauching coqc.
Print the Coq’s standard library location and exit.
Print the Coq’s version and exit.
Print a short usage and exit.