Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.Sign up
The information below are valid for developing in Coq 8.10 (2018)
Developing Coq: A tutorial
Getting Coq sources
Coq sources are hosted on GitHub. The recommended way is to get them is:
git clone https://github.com/coq/coq
Compiling Coq sources
Follow the instructions from the file INSTALL of the Coq archive
Basic developer setup
Development process might be faster by working locally and not installing Coq in the path. To do so run
-local option means that you will not need to install coq to
/usr/local but instead that you will run Coq directly from the
In fact, the recommended way of running configure for hacking Coq is
./configure -profile devel (which includes
-local among other developer settings). An alternative way of building Coq is by using dune (run
make -f Makefile.dune to learn about available targets).
The Coq archive contains the following subdirectories:
binwhere binaries are created
devmiscellaneous information for developers
docthe Coq documentation and User's reference manual sources
manCoq man pages
theoriesthe Coq standard library
pluginssources of plugins (extraction, firstorder, ...)
test-suitethe Coq test suite
The sources of Coq reside in the following directories
configOCaml files created by the configure script
libutilities, general-purpose data structures, ...
kernelthe Coq kernel, which implements the type-checker of the Calculus of Inductive Constructions
libraryglobal names, infrastructure for backtracking, reading/writing vo files, ...
pretypingunification, compilation of pattern-matching, type inference, coercions
enginelow-level part of the proof engine
proofshigh-level part of the proof engine
tacticsspecific tactics and the tactic language
interpsyntax interpretation layer: notations, implicit arguments, globalization of names, ...
stmthe state transition machine for asynchronous evaluation
toplevelinteractive loop, treatment of options, ...
idesource of the CoqIDE graphical interface
The Coq source contains the usual OCaml
.mli files but it
.mlg files that need to be preprocessed by coqpp, and
.mlp files preprocessed by camlp5 (the later will probably be
removed between 8.9 and 8.10, they're only used for processing the
.ml4 files in external plugins).
Main developer targets
A complete compilation is done by
make world. It takes about 10 minutes with option -j4 on a 4 core processor.
When developing, you may use partial targets such as:
statesbuilds the initial state, this is required to run Coq.
bin/coqtop.byteand plugins in byte code; this is the fastest target when debugging the OCaml code.
bin/coqtop pluginsoptto compile Coq to native code.
coqidebuilds CoqIDE and the initial state but no standard library.
bin/coqidenor the library
The compiling process require preprocessing, which requires some compiling, this is why the following sequence should better be respected when adding new files to Coq:
make cleanfor binary compatibility
make worldto rebuild (or simply
Another way to clean the archive from all non-registered files is to use
git clean -fxd.
Adding a new file
Files to be linked are registered in files named
pretyping/pretyping.mllib). The files must be given in an order compatible with the linking dependency order.
Simple debugging with
bin/coqtop.byte and type
Drop.. This will drop to the OCaml toplevel. Then type:
#use "include";; #trace String.uppercase;; (* or any name of a function you'd like to trace *) go();;
go() restarts the Coq parser. You can type any Coq command and observe when it calls the function asked to be traced.
Debugging with ocamldebug
Look at file
dev/doc/debugging.txt in the archive.