Chapter 14  The Coq commands

There are three Coq commands:

The options are (basically) the same for the first two commands, and roughly described below. You can also look at the man pages of coqtop and 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). 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();;.

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 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.

14.3  Customization at launch time

14.3.1  By resource file

When Coq is launched, with either coqtop or coqc, the resource file $XDG_CONFIG_HOME/coq/coqrc.xxx is loaded, where $XDG_CONFIG_HOME is the configuration directory of the user (by default its home directory /.config and 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 -init-file below).

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.

14.4  By environment variables

Load path can be specified to the Coq system by setting up $COQPATH environment variable. It is a list of directories separated by : (; on windows).

Coqwill also honour $XDG_DATA_HOME and $XDG_DATA_DIRS (see http://standards.freedesktop.org/basedir-spec/basedir-spec-latest.html). Coqadds ${XDG_DATA_HOME}/coq and ${XDG_DATA_DIRS}/coq to its search path.

14.4.1  By command line options

The following command-line options are recognized by the commands coqc and coqtop, unless stated otherwise:

-I directory, -include directory[ -as dirpath
]

Add physical path directory to the list of directories where to look for a file and bind it to the empty logical directory/the logical directory dirpath. The sub-directory structure of directory is recursively available from Coq using absolute names (extending the dirpath prefix) (see Section 2.6.2).


See also: Add LoadPath in Section 6.6.3 and logical paths in Section 2.6.1.

-R directory dirpath, -R directory [-as dirpath
] Do as -I directory -as dirpath but make the sub-directory 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: Add Rec LoadPath in Section 6.6.4 and logical paths in Section 2.6.1.

-top dirpath, -notop

This sets the toplevel module name to dirpath/the empty logical path instead of Top. Not valid for coqc.

-exclude-dir subdirectory

This tells to exclude any sub-directory named subdirectory while processing option -R. Without this option only the conventional version control management sub-directories named CVS and _darcs are excluded.

-is file, -inputstate file, -outputstate file

Load at the beginning/Dump at the end a Coq state from the file file.

Incompatible with some not purely functional aspect of the code

-nois

Cause Coq to begin with an empty state.

-init-file file, -q

Take file as the resource file. / Cause Coq not to load the resource file.

-load-ml-source file

Load the Caml source file file.

-load-ml-object file

Load the Caml object file file.

-l[v] file, -load-vernac-source[-verbose] file

Load Coq file file.v optionally with copy it contents on the standard input.

-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,-compile-verbose file, -batch

coqtop options only used internally by coqc.

This compiles file file.v into file.vo without/with a copy of the contents of the file on standard input. This option implies options -batch (exit just after arguments parsing). It is only available for coqtop.

-verbose

This option is only for coqc. It tells to compile the file with a copy of its contents on standard input.

-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.

-with-geoproof (yes|no)

Activate or not special functions for Geoproof within Coqide (default is yes).

-beautify

While compiling file, pretty prints each command just after having parsing it in file.beautified in order to get old-fashion syntax/definitions/notations.

-quality

Improve the legibility of the proof terms produced by some tactics.

-emacs, -ide-slave

Start a special main loop to communicate with ide.

-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

-compat version

Attempt to maintain some of the incompatible changes in their version behavior.

-dump-glob file

This dumps references for global names in file file (to be used by coqdoc, see 15.4)

-dont-load-proofs

Warning: this is an unsafe mode. Instead of loading in memory the proofs of opaque theorems, they are treated as axioms. This results in smaller memory requirement and faster compilation, but the behavior of the system might slightly change (for instance during module subtyping), and some features won’t be available (for example Print Assumptions).

-lazy-load-proofs
This is the default behavior. Proofs of opaque theorems aren’t loaded immediately in memory, but only when necessary, for instance during some module subtyping or Print Assumptions. This should be almost as fast and efficient as -dont-load-proofs, with none of its drawbacks.
-force-load-proofs
Proofs of opaque theorems are loaded in memory as soon as the corresponding Require is done. This used to be Coq’s default behavior.
-no-hash-consing
-vm

This activates the use of the bytecode-based conversion algorithm for the current session (see Section 6.11.5).

-image file

This option sets the binary image to be used by coqc to be file instead of the standard one. Not of general use.

-bindir directory

Set for coqc the directory containing Coq binaries. It is equivalent to do export COQBIN=directory before launching coqc.

-where, -config, -filteropts

Print the Coq’s standard library location or Coq’s binaries, dependencies, libraries locations or the list of command line arguments that coqtop has recognize as options and exit.

-v

Print the Coq’s version and exit.

-h, --help

Print a short usage and exit.

14.5  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 force check of its dependencies.

-admit module
Do not check module and any of its dependencies, unless explicitly required.
-o

At exit, print a summary about the context. List the names of all assumptions and variables (constants without body).

-silent

Do not write progress information in standard output.

Environment variable $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:

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.

1
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.