- 14.1 Interactive use (coqtop)
- 14.2 Batch compilation (coqc)
- 14.3 Customization
- 14.4 Compiled libraries checker (coqchk)
There are three Coq commands:
- coqtop: the Coq toplevel (interactive mode);
- coqc: the Coq compiler (batch compilation);
- coqchk: the Coq checker (validation of compiled libraries).
The options are (basically) the same for the first two commands, and
roughly described below. You can also look at the
man pages of
coqc for more details.
14.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). By default,
coqtop executes the native-code version; run
get the byte-code version.
The byte-code toplevel is based on an Objective Caml
toplevel (to allow the dynamic link of tactics). You can switch to
the Objective Caml toplevel with the command
Drop., and come back to the
Coq toplevel with the command
14.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.5).
Warning: The name file should be a regular Coq identifier, as defined in Section 1.1. It should contain only letters, digits or underscores (_). For instance,
/bar/foo/toto.v is valid, but
/bar/foo/to-to.v is invalid.
14.3 Customization at launch time
When Coq is launched, with either coqtop or coqc, the
$XDG_CONFIG_HOME/coq/coqrc.xxx is loaded, where
$XDG_CONFIG_HOME is the configuration directory of the user (by
default its home directory
xxx is the version
number (e.g. 8.3). If this file is not found, then the file
$XDG_CONFIG_HOME/coqrc is searched. You can also specify an
arbitrary name for the resource file (see option
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
Load path can be specified to the Coq system by setting up
$COQPATH environment variable. It is a list of directories
; on windows). Coq will also honor
$XDG_DATA_DIRS (see Section
Some Coq commands call other Coq commands. In this case, they
look for the commands in directory specified by
this variable is not set, they look for the commands in the executable
$COQ_COLORS environment variable can be used to specify the set of
colors used by coqtop to highlight its output. It uses the same syntax as
$LS_COLORS variable from GNU’s ls, that is, a colon-separated
list of assignments of the form
name=attr1;...;attrn where name is
the name of the corresponding highlight tag and attri is an ANSI escape
code. The list of highlight tags can be retrieved with the -list-tags
command-line option of coqtop.
The following command-line options are recognized by the commands coqc and coqtop, unless stated otherwise:
- -I directory, -include directory
Add physical path directory to the Objective Caml loadpath.
- -Q directory dirpath
Add physical path directory to the list of directories where Coq looks for a file and bind it to the the logical directory dirpath. The subdirectory structure of directory is recursively available from Coq using absolute names (extending the dirpath prefix) (see Section 2.6.2).
Note that only those subdirectories and files which obey the lexical conventions of what is an ident (see Section 1.1) are taken into account. Conversely, the underlying file systems or operating systems may be more restrictive than Coq. While Linux’s ext4 file system supports any Coq recursive layout (within the limit of 255 bytes per file name), the default on NTFS (Windows) or HFS+ (MacOS X) file systems is on the contrary to disallow two files differing only in the case in the same directory.
See also: Section 2.6.1.
- -R directory dirpath
Do as -Q directory dirpath but make the subdirectory structure of directory recursively visible so that the recursive contents of physical directory is available from Coq using short or partially qualified names.
See also: Section 2.6.1.
- -top dirpath
Set the toplevel module name to dirpath instead of Top. Not valid for coqc as the toplevel module name is inferred from the name of the output file.
- -exclude-dir directory
Exclude any subdirectory named directory while processing options such as -R and -Q. By default, only the conventional version control management directories named CVS and _darcs are excluded.
Start from an empty state instead of loading the Init.Prelude module.
- -init-file file
Load file as the resource file instead of loading the default resource file from the standard configuration directories.
Do not to load the default resource file.
- -load-ml-source file
Load the Objective Caml source file file.
- -load-ml-object file
Load the Objective Caml object file file.
- -l file, -load-vernac-source file
Load and execute the Coq script from file.v.
- -lv file, -load-vernac-source-verbose file
Load and execute the Coq script from file.v. Output its content on the standard input as it is executed.
- -load-vernac-object dirpath
Load Coq compiled library dirpath. This is equivalent to running Require dirpath.
- -require dirpath
Load Coq compiled library dirpath and import it. This is equivalent to running Require Import dirpath.
Exit just after argument parsing. Available for coqtop only.
- -compile file.v
Compile file file.v into file.vo. This options imply -batch (exit just after argument parsing). It is available only for coqtop, as this behavior is the purpose of coqc.
- -compile-verbose file.v
Same as -compile but also output the content of file.v as it is compiled.
Output the content of the input file as it is compiled. This option is available for coqc only; it is the counterpart of -compile-verbose.
- -w (all|none|w1,…,wn)
Configure the display of warnings. This option expects all, none or a comma-separated list of warning names or categories (see Section 6.9.3).
- -with-geoproof (yes|no)
Enable or not special functions for Geoproof within CoqIDE (default is yes).
- -color (on|off|auto)
Enable or not the coloring of output of coqtop. Default is auto, meaning that coqtop dynamically decides, depending on whether the output channel supports ANSI escape sequences.
Pretty-print each command to file.beautified when compiling file.v, in order to get old-fashioned syntax/definitions/notations.
- -emacs, -ide-slave
Start a special toplevel to communicate with a specific IDE.
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.
Collapse the universe hierarchy of Coq. Warning: this makes the logic inconsistent.
- -compat version
Attempt to maintain some backward-compatibility with a previous version.
- -dump-glob file
Dump references for global names in file file (to be used by coqdoc, see 15.4). By default, if file.v is being compiled, file.glob is used.
Disable the dumping of references for global names.
- -image file
Set the binary image to be used by coqc to be file instead of the standard one. Not of general use.
- -bindir directory
Set the directory containing Coq binaries to be used by coqc. It is equivalent to doing export COQBIN=directory before launching coqc.
Print the location of Coq’s standard library and exit.
Print the locations of Coq’s binaries, dependencies, and libraries, then exit.
Print the list of command line arguments that coqtop has recognized as options and exit.
Print Coq’s version and exit.
Print the highlight tags known by Coq as well as their currently associated color and exit.
- -h, --help
Print a short usage and exit.
14.4 Compiled libraries checker (coqchk)
The coqchk command takes a list of library paths as argument. The corresponding compiled libraries (.vo files) are searched in the path, recursively processing the libraries they depend on. The content of all these libraries is then type-checked. The effect of coqchk is only to return with normal exit code in case of success, and with positive exit code if an error has been found. Error messages are not deemed to help the user understand what is wrong. In the current version, it does not modify the compiled libraries to mark them as successfully checked.
Note that non-logical information is not checked. By logical information, we mean the type and optional body associated to names. It excludes for instance anything related to the concrete syntax of objects (customized syntax rules, association between short and long names), implicit arguments, etc.
This tool can be used for several purposes. One is to check that a compiled library provided by a third-party has not been forged and that loading it cannot introduce inconsistencies.1 Another point is to get an even higher level of security. Since coqtop can be extended with custom tactics, possibly ill-typed code, it cannot be guaranteed that the produced compiled libraries are correct. coqchk is a standalone verifier, and thus it cannot be tainted by such malicious code.
Command-line options -I, -R, -where and -impredicative-set are supported by coqchk and have the same meaning as for coqtop. Extra options are:
- -norec module
Check module but do not check its dependencies.
- -admit module
Do not check module and any of its dependencies, unless explicitly required.
At exit, print a summary about the context. List the names of all assumptions and variables (constants without body).
Do not write progress information in standard output.
$COQLIB can be set to override the
location of the standard library.
The algorithm for deciding which modules are checked or admitted is the following: assuming that coqchk is called with argument M, option -norec N, and -admit A. Let us write S the set of reflexive transitive dependencies of set S. Then:
- Modules C=M\A∪ M∪ N are loaded and type-checked before being added to the context.
- And M∪N\ C is the set of modules that are loaded and added to the context without type-checking. Basic integrity checks (checksums) are nonetheless performed.
As a rule of thumb, the -admit can be used to tell that some libraries have already been checked. So coqchk A B can be split in coqchk A && coqchk B -admit A without type-checking any definition twice. Of course, the latter is slightly slower since it makes more disk access. It is also less secure since an attacker might have replaced the compiled library A after it has been read by the first command, but before it has been read by the second command.
- Ill-formed non-logical information might for instance bind Coq.Init.Logic.True to short name False, so apparently False is inhabited, but using fully qualified names, Coq.Init.Logic.False will always refer to the absurd proposition, what we guarantee is that there is no proof of this latter constant.