Chapter 13 The Coq commands

# Coq Reference Manual

# Chapter 13 The Coq commands

- 13.1 Interactive use (`coqtop`)
- 13.2 Batch compilation (`coqc`)
- 13.3 Resource file
- 13.4 Environment variables
- 13.5 Options
- 13.6 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 `coqtop` and `coqc` for more details.

## 13.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();;`.

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

## 13.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`.

## 13.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 where 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 14.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.

## 13.5 Options

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

`-byte`

  Run the byte-code version of Coq.

`-opt`

  Run the native-code version of Coq.

`-I` directory, `-include` directory

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

`-I` directory `-as` dirpath

  Add physical path directory to the list of directories where to look for a file and bind it to the logical directory dirpath. The subdirectory structure of directory is recursively available from Coq using absolute names extending the dirpath prefix.

  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 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: `Add Rec LoadPath` in Section 6.6.4 and logical paths in Section 2.6.1.

`-top` dirpath

  This sets the toplevel module name to dirpath instead of `Top`. Not valid for `coqc`.

`-notop` dirpath

  This sets the toplevel module name to the empty logical dirpath. Not valid for `coqc`.

`-exclude-dir` subdirectory

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

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

`-outputstate` file

  Cause Coq to dump its state to file file.coq just after finishing parsing and evaluating all the arguments from the command line.

`-nois`

  Cause Coq to begin with an empty state. Mainly useful to build the standard input state.

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

`-l` file, `-load-vernac-source` file

  Load Coq file file`.v`

`-lv` file, `-load-vernac-source-verbose` file

  Load Coq file file`.v` with a copy of the contents of the file on 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

  This compiles file file`.v` into file`.vo`. This option implies options `-batch` and `-silent`. It is only available for `coqtop`.

`-compile-verbose` file

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

`-verbose`

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

`-batch`

  Batch mode : exit just after arguments parsing. This option is only used by `coqc`.

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

`-quality`

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

`-emacs`

  Tells Coq it is executed under Emacs.

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

`-dump-glob` file
  This dumps references for global names in file file (to be used by coqdoc, see 14.4)
`-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.

`-vm`

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

`-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 for `coqc` the directory containing Coq binaries. It is equivalent to do `export COQBIN=`directory before lauching `coqc`.

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

## 13.6 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:

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

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.