DevelopmentTutorial - rocq-prover/rocq GitHub Wiki

The information below are valid for developing in Rocq 9.1 (2025)

Developing Rocq: A tutorial

Getting Rocq sources

Rocq sources are hosted on GitHub. The recommended way is to get them is:

git clone https://github.com/rocq-prover/rocq

Compiling Rocq sources

Follow the instructions from the file INSTALL of the Rocq archive

Basic developer setup

Before running dune build commands to build .vo files you need to run make dunestrap.

Alternatively you can stick to the make check and make world targets which will handle dunestrap automatically and never call dune directly yourself.

Directory structure

The Rocq archive contains the following subdirectories:

  • dev miscellaneous tools and information for developers (notably including CI scripts)

  • doc the Rocq documentation and User's reference manual sources

  • man Rocq man pages

  • tools sources of rocq doc, rocq dep, rocq tex, rocq makefile, etc.

  • theories the Rocq Corelib library and Ltac2 library

  • plugins sources of plugins (extraction, firstorder, ...)

  • test-suite the Rocq test suite

The sources of Rocq reside in the following directories

  • config OCaml files created by the configure script

  • clib general purpose data structures

  • lib utilities, general-purpose data structures, ...

  • perf performance counter code (for CPU instruction counting)

  • boot path bootstrapping (eg finding the corelib), cf system configuration in the refman

  • kernel the Rocq kernel, which implements the type-checker of the Calculus of Inductive Constructions

  • library global names, infrastructure for backtracking, reading/writing vo files, ...

  • pretyping unification, compilation of pattern-matching, type inference, coercions

  • engine low-level part of the proof engine

  • proofs high-level part of the proof engine

  • tactics specific tactics and the tactic language

  • interp syntax interpretation layer: notations, implicit arguments, globalization of names, ...

  • gramlib parsing engine (fork of camlp5)

  • parsing parsers

  • printing printers

  • stm the state transition machine for asynchronous evaluation

  • vernac vernacular commands

  • sysinit initialization (setting up custom GC params, handling command line args, ...)

  • toplevel interactive loop, treatment of options, ...

  • topbin main executables

  • ide source of the RocqIDE graphical interface (and coqide-server ie the XML protocol)

  • checker source of rocqchk

  • coqpp source of rocq preprocess-mlg

.mlg files

The Rocq source contains the usual OCaml .ml and .mli files but it also contains .mlg files that need to be preprocessed by rocq preprocess-mlg.

See dev/doc/parsing.md for more info.

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:

  • states builds the initial state, this is required to run Rocq. Since the stdlib moved to a separate repo this is not much smaller than world, so you may as well build world instead.

  • rocqide builds RocqIDE.

  • check (equivalent to dune build @check) typechecks OCaml files.

  • refman-html and refman-pdf build the refman (both need sphinx, PDF version needs latex, see dev/ci/docker for packages installed in CI).

Simple debugging with Drop

After make world, run dune exec -- rocq top-with-drop 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();;

The last 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

https://github.com/rocq-prover/rocq/wiki/OCamldebug