The Coq commands¶
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.
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
.
There are two different binary images of Coq: the byte-code one and the
native-code one (if OCaml provides a native-code compiler for
your platform, which is supposed in the following). By default,
coqtop
executes the native-code version; run coqtop.byte
to get
the byte-code version.
The byte-code toplevel is based on an OCaml toplevel (to
allow dynamic linking of tactics). You can switch to the OCaml toplevel
with the command Drop.
, and come back to the Coq
toplevel with the command Coqloop.loop();;
.
Batch compilation (coqc)¶
The coqc
command compiles a Coq proof script file with a ".v" suffix
to create a compiled file with a ".vo" suffix. (See Compiled files.)
The last component of the filename must be a valid Coq identifier as described in
Lexical conventions; it should contain only letters, digits or
underscores (_) with a ".v" suffix on the final component.
For example /bar/foo/toto.v
is valid, but /bar/foo/to-to.v
is not.
We recommend specifying a logical directory name (which is also the module name)
with the -R
or the -Q
options.
Generally we recommend using utilities such as make
(using coq_makefile
to generate the Makefile
) or dune
to build Coq projects.
See Building a Coq project.
Example: Compiling and loading a single file
If foo.v
is in Coq's current directory, you can use coqc foo.v
to compile it and then Require foo.
in your script. But this
doesn't scale well for larger projects.
Generally it's' better to define a new module:
To compile foo.v
as part of a module Mod1
that is rooted
at .
(i.e. the directory containing foo.v
), run coqc -Q . Mod1 foo.v
.
To make the module available in CoqIDE
, include the following line in the
_CoqProject
file (see Building a Coq project with coq_makefile) in the directory from which you
start CoqIDE
. <PATH> is the pathname of the directory containing the module,
which can be an absolute path or relative to Coq's current directory. For now,
you must close and reload a named script file for CoqIDE
to pick up the change,
or restart CoqIDE
.
The project file name is configurable in Edit / Preferences / Project
.
-R <PATH> Mod1
It's also possible to load a module within coqtop
or coqide
with
commands like these. The drawback of this is that it adds
environment-specific information (the PATH) to your script, making
it non-portable, so we discourage using this approach.
Add LoadPath "PATH" as Mod1. Require Mod1.foo.
in which PATH
is the pathname of the directory containing foo.v
, which
can be absolute or relative to Coq's current directory. The
Add LoadPath
is not needed if you provide the mapping from the
logical directory (module name) to the physical directory by including the
-Q . Mod1
as command-line arguments to coqtop
or coqide
.
Customization at launch time¶
By resource file¶
When Coq is launched, with either coqtop
or coqc
, the
resource file $XDG_CONFIG_HOME/coq/coqrc.xxx
, if it exists, will
be implicitly prepended to any document read by Coq, whether it is an
interactive session or a file to compile. Here, $XDG_CONFIG_HOME
is the configuration directory of the user (by default it's ~/.config
)
and xxx
is the version number (e.g. 8.8). If
this file is not found, then the file $XDG_CONFIG_HOME/coqrc
is
searched. If not found, it is the file ~/.coqrc.xxx
which is searched,
and, if still not found, the file ~/.coqrc
. If the latter is also
absent, no resource file is loaded.
You can also specify an arbitrary name for the resource file
(see option -init-file
below).
The resource 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
.
By environment variables¶
$COQPATH
can be used to specify the load path. It is a list of directories separated by
:
(;
on Windows). Coq will also honor $XDG_DATA_HOME
and
$XDG_DATA_DIRS
(see Section Libraries and filesystem).
Some Coq commands call other Coq commands. In this case, they look for
the commands in directory specified by $COQBIN
. If this variable is
not set, they look for the commands in the executable path.
$COQ_COLORS
can be used to specify the set
of colors used by coqtop
to highlight its output. It uses the same
syntax as the $LS_COLORS
variable from GNU’s ls, that is, a colon-separated
list of assignments of the form name=attr*;
where
name
is the name of the corresponding highlight tag and each attr
is an
ANSI escape code. The list of highlight tags can be retrieved with the
-list-tags
command-line option of coqtop
.
The string uses ANSI escape codes to represent attributes. For example:
export COQ_COLORS=”diff.added=4;48;2;0;0;240:diff.removed=41”
sets the highlights for added text in diffs to underlined (the 4) with a background RGB
color (0, 0, 240) and for removed text in diffs to a red background.
Note that if you specify COQ_COLORS
, the predefined attributes are ignored.
$OCAMLRUNPARAM
, described
here,
can be used to specify certain runtime and memory usage parameters. In most cases,
experimenting with these settings will likely not cause a significant performance difference
and should be harmless.
If the variable is not set, Coq uses the
default values,
except that space_overhead
is set to 120 and minor_heap_size
is set to 32Mwords
(256MB with 64-bit executables or 128MB with 32-bit executables).
By command line options¶
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 OCaml loadpath.
See also
Names of libraries and the command Declare ML Module Section Compiled files.
- -Q directory dirpath
Add physical path directory to the list of directories where Coq looks 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 Section Qualified identifiers). Note that only those subdirectories and files which obey the lexical conventions of what is anident
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 filename), 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 Names of libraries.
- -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 Names of libraries.
- -top dirpath
Set the logical module name to
dirpath
for thecoqtop
interactive session. If no module name is specified,coqtop
will default toTop
.coqc
does not accept this option because the logical module name is inferred from the name of the input file and the corresponding-R
/-Q
options.- -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.
- -nois, -noinit
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.
- -q
Do not to load the default resource 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. Write its contents to the standard output as it is executed.
- -load-vernac-object qualid
Load Coq compiled library
qualid
. This is equivalent to runningRequire
qualid
.Note
Note that the relative order of this command-line option and its variants (
-rfrom
,-ri
,-re
, etc.) and of the-set
and-unset
options matters since the variousRequire
,Require Import
,Require Export
,Set
andUnset
commands will be executed in the order specified on the command-line.- -rfrom dirpath qualid
Load Coq compiled library
qualid
. This is equivalent to runningFrom
dirpath
Require
qualid
. See the note above regarding the order of command-line options.- -ri qualid, -require-import qualid
Load Coq compiled library
qualid
and import it. This is equivalent to runningRequire Import
qualid
. See the note above regarding the order of command-line options.- -re qualid, -require-export qualid
Load Coq compiled library
qualid
and transitively import it. This is equivalent to runningRequire Export
qualid
. See the note above regarding the order of command-line options.- -rifrom dirpath qualid, -require-import-from dirpath qualid
Load Coq compiled library
qualid
and import it. This is equivalent to runningFrom
dirpath
Require Import
qualid
. See the note above regarding the order of command-line options.- -refrom dirpath qualid, -require-export-from dirpath qualid
Load Coq compiled library
qualid
and transitively import it. This is equivalent to runningFrom
dirpath
Require Export
qualid
. See the note above regarding the order of command-line options.- -batch
Exit just after argument parsing. Available for
coqtop
only.- -verbose
Output the content of the input file as it is compiled. This option is available for
coqc
only.- -native-compiler (yes|no|ondemand)
Enable the
native_compute
reduction machine and precompilation to.cmxs
files for future use bynative_compute
. Settingyes
enablesnative_compute
; it also causes Coq to precompile the native code for future use; all dependencies need to have been precompiled beforehand. Settingno
disablesnative_compute
which defaults back tovm_compute
; no files are precompiled. Settingondemand
enablesnative_compute
but disables precompilation; all missing dependencies will be recompiled every timenative_compute
is called.Deprecated since version 8.14: This flag has been deprecated in favor of the Split compilation of native computation files binary. The toolchain has been adapted to transparently rely on the latter, so if you use Building a Coq project with coq_makefile there is nothing to do. Otherwise you should substitute calls to
coqc -native-compiler yes
to calls tocoqc
followed bycoqnative
on the resultingvo
file.Changed in version 8.13: The default value is set at configure time,
-config
can be used to retrieve it. All this can be summarized in the following table:configure
coqc
native_compute
outcome
requirements
yes
yes (default)
native_compute
.cmxs
.cmxs
of depsyes
no
vm_compute
none
none
yes
ondemand
native_compute
none
none
no
yes, no, ondemand
vm_compute
none
none
ondemand
yes
native_compute
.cmxs
.cmxs
of depsondemand
no
vm_compute
none
none
ondemand
ondemand (default)
native_compute
none
none
- -native-output-dir
Set the directory in which to put the aforementioned
.cmxs
fornative_compute
. Defaults to.coq-native
.- -vos
Indicate Coq to skip the processing of opaque proofs (i.e., proofs ending with
Qed
orAdmitted
), output a.vos
files instead of a.vo
file, and to load.vos
files instead of.vo
files when interpretingRequire
commands.- -vok
Indicate Coq to check a file completely, to load
.vos
files instead of.vo
files when interpretingRequire
commands, and to output an empty.vok
files upon success instead of writing a.vo
file.- -w (all|none|w₁,…,wₙ)
Configure the display of warnings. This option expects all, none or a comma-separated list of warning names or categories (see Section Controlling display).
- -color (on|off|auto)
Coqtop only. Enable or disable color output. Default is auto, meaning color is shown only if the output channel supports ANSI escape sequences.
- -diffs (on|off|removed)
Coqtop only. Controls highlighting of differences between proof steps.
on
highlights added tokens,removed
highlights both added and removed tokens. Requires that-color
is enabled. (see Section Showing differences between proof steps).- -beautify
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.
- -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.
- -type-in-type
Collapse the universe hierarchy of Coq.
Warning
This makes the logic inconsistent.
- -mangle-names ident
Experimental. Do not depend on this option. Replace Coq's auto-generated name scheme with names of the form ident0, ident1, etc. Within Coq, the
Mangle Names
flag turns this behavior on, and theMangle Names Prefix
option sets the prefix to use. This feature is intended to be used as a linter for developments that want to be robust to changes in the auto-generated name scheme. The options are provided to facilitate tracking down problems.- -set string
Enable flags and set options. string should be
setting_name=value
, the value is interpreted according to the type of the option. For flagssetting_name
is equivalent tosetting_name=true
. For instance-set "Universe Polymorphism"
will enableUniverse Polymorphism
. Note that the quotes are shell syntax, Coq does not see them. See the note above regarding the order of command-line options.- -unset string
As
-set
but used to disable options and flags. string must be"setting_name"
. See the note above regarding the order of command-line options.- -compat version
Load a file that sets a few options to maintain partial backward-compatibility with a previous version. This is equivalent to
Require Import
Coq.Compat.CoqXXX
withXXX
one of the last three released versions (including the current version). Note that the explanations above regarding the order of command-line options apply, and this could be relevant if you are resetting some of the compatibility options.- -dump-glob file
Dump references for global names in file file (to be used by coqdoc, see Documenting Coq files with coqdoc). By default, if file.v is being compiled, file.glob is used.
- -no-glob
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 launchingcoqc
.- -where
Print the location of Coq’s standard library and exit.
- -config
Print the locations of Coq’s binaries, dependencies, and libraries, then exit.
- -filteropts
Print the list of command line arguments that
coqtop
has recognized as options and exit.- -v
Print Coq’s version and exit.
- -list-tags
Print the highlight tags known by Coq as well as their currently associated color and exit.
- -h, --help
Print a short usage and exit.
Compiled interfaces (produced using -vos
)¶
Compiled interfaces help saving time while developing Coq formalizations, by compiling the formal statements exported by a library independently of the proofs that it contains.
Warning
Compiled interfaces should only be used for development purposes. At the end of the day, one still needs to proof check all files by producing standard
.vo
files. (Technically, when using-vos
, fewer universe constraints are collected.) Moreover, this feature is still experimental, it may be subject to change without prior notice.
Principle.
The compilation using coqc -vos foo.v
produces a file called foo.vos
,
which is similar to foo.vo
except that all opaque proofs are skipped in
the compilation process.
The compilation using coqc -vok foo.v
checks that the file foo.v
correctly compiles, including all its opaque proofs. If the compilation
succeeds, then the output is a file called foo.vok
, with empty contents.
This file is only a placeholder indicating that foo.v
has been successfully
compiled. (This placeholder is useful for build systems such as make
.)
When compiling a file bar.v
that depends on foo.v
(for example via
a Require Foo.
command), if the compilation command is coqc -vos bar.v
or coqc -vok bar.v
, then the file foo.vos
gets loaded (instead of
foo.vo
). A special case is if file foo.vos
exists and has empty
contents, and foo.vo
exists, then foo.vo
is loaded.
Appart from the aforementioned case where foo.vo
can be loaded in place
of foo.vos
, in general the .vos
and .vok
files live totally
independently from the .vo
files.
Dependencies generated by ``coq_makefile``.
The files foo.vos
and foo.vok
both depend on foo.v
.
Furthermore, if a file foo.v
requires bar.v
, then foo.vos
and foo.vok
also depend on bar.vos
.
Note, however, that foo.vok
does not depend on bar.vok
.
Hence, as detailed further, parallel compilation of proofs is possible.
In addition, coq_makefile
generates for a file foo.v
a target
foo.required_vos
which depends on the list of .vos
files that
foo.vos
depends upon (excluding foo.vos
itself). As explained
next, the purpose of this target is to be able to request the minimal
working state for editing interactively the file foo.v
.
Warning
When writing a custom build system, be aware that coqdep
only
produces dependencies related to .vos
and .vok
if the
-vos
command line flag is passed. This is to maintain
compatibility with dune (see ocaml/dune#2642 on github).
Typical compilation of a set of file using a build system.
Assume a file foo.v
that depends on two files f1.v
and f2.v
. The
command make foo.required_vos
will compile f1.v
and f2.v
using
the option -vos
to skip the proofs, producing f1.vos
and f2.vos
.
At this point, one is ready to work interactively on the file foo.v
, even
though it was never needed to compile the proofs involved in the files f1.v
and f2.v
.
Assume a set of files f1.v ... fn.v
with linear dependencies. The command
make vos
enables compiling the statements (i.e. excluding the proofs) in all
the files. Next, make -j vok
enables compiling all the proofs in parallel.
Thus, calling make -j vok
directly enables taking advantage of a maximal
amount of parallelism during the compilation of the set of files.
Note that this comes at the cost of parsing and typechecking all definitions
twice, once for the .vos
file and once for the .vok
file. However, if
files contain nontrivial proofs, or if the files have many linear chains of
dependencies, or if one has many cores available, compilation should be faster
overall.
Need for ``Proof using``
When a theorem is part of a section, typechecking the statement of this theorem might be insufficient for deducing the type of this statement as of at the end of the section. Indeed, the proof of the theorem could make use of section variables or section hypotheses that are not mentioned in the statement of the theorem.
For this reason, proofs inside section should begin with Proof using
instead of Proof
, where after the using
clause one should provide
the list of the names of the section variables that are required for the proof
but are not involved in the typechecking of the statement. Note that it is safe
to write Proof using.
instead of Proof.
also for proofs that are not
within a section.
-
Warning
You should use the “Proof using [...].” syntax instead of “Proof.” to enable skipping this proof which is located inside a section. Give as argument to “Proof using” the list of section variables that are not needed to typecheck the statement but that are required by the proof.
¶ If Coq is invoked using the
-vos
option, whenever it finds the commandProof.
inside a section, it will compile the proof, that is, refuse to skip it, and it will raise a warning. To disable the warning, one may pass the flag-w -proof-without-using-in-section
.
Interaction with standard compilation
When compiling a file foo.v
using coqc
in the standard way (i.e., without
-vos
nor -vok
), an empty file foo.vos
and an empty file foo.vok
are created in addition to the regular output file foo.vo
.
If coqc
is subsequently invoked on some other file bar.v
using option
-vos
or -vok
, and that bar.v
requires foo.v
, if Coq finds an
empty file foo.vos
, then it will load foo.vo
instead of foo.vos
.
The purpose of this feature is to allow users to benefit from the -vos
option even if they depend on libraries that were compiled in the traditional
manner (i.e., never compiled using the -vos
option).
Compiled libraries checker (coqchk)¶
The coqchk
command takes a list of library paths as argument, described either
by their logical name or by their physical filename, which must end in .vo
. 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 with 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 -Q
, -R
, -where
and -impredicative-set
are supported
by coqchk
and have the same meaning as for coqtop
. As there is no notion of
relative paths in object files -Q
and -R
have exactly the same meaning.
- -norec module
Check module but do not check 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 a body).
- -silent
Do not write progress information to the 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 \(\overline{S}\) for the
set of reflexive transitive dependencies of set \(S\). Then:
Modules \(C = \overline{M} \backslash \overline{A} \cup M \cup N\) are loaded and type checked before being added to the context.
And \(M \cup N \backslash 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, -admit can be used to tell Coq 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.