The Coq documentation #

The Coq documentation includes

• A Reference Manual
• A document presenting the Coq standard library

The documentation of the latest released version is available on the Coq web site at rocq-prover.org/docs.

Additionally, you can view the reference manual for the development version at https://rocq-prover.org/doc/master/refman/, and the documentation of the standard library for the development version at https://rocq-prover.org/doc/master/stdlib/.

The reference manual is written in reStructuredText and compiled using Sphinx. See sphinx/README.rst to learn more about the format that is used.

The documentation for the standard library is generated from the .v source files using rocq doc.

Dependencies #

HTML documentation #

To produce the complete documentation in HTML, you will need Coq dependencies listed in INSTALL.md. Additionally, the Sphinx-based reference manual requires Python 3, and the following Python packages:

• sphinx >= 5.0.0
• sphinx_rtd_theme >= 1.1.0
• beautifulsoup4 >= 4.10.0
• antlr4-python3-runtime >= 4.7.1 & <= 4.9.3
• pexpect >= 4.8.0
• sphinxcontrib-bibtex >= 2.4.2
• sphinx-markdown-builder >= 0.6.10

To install them, you should first install pip and setuptools (for instance, with apt install python3-pip python3-setuptools on Debian / Ubuntu) then run:

pip3 install sphinx sphinx_rtd_theme beautifulsoup4 \
             antlr4-python3-runtime==4.7.1 pexpect sphinxcontrib-bibtex \
             sphinx-markdown-builder==0.6.10

Nix users should get the correct development environment to build the HTML documentation from Coq's default.nix (note this doesn't include the LaTeX packages needed to build the full documentation).

You can check the dependencies using the doc/tools/coqrst/checkdeps.py script.

Other formats #

To produce the documentation in PDF and PostScript formats, the following additional tools are required:

• latex (latex2e)
• pdflatex
• dvips
• makeindex
• xelatex
• latexmk

All of them are part of the TexLive distribution. E.g. on Debian / Ubuntu, install them with:

apt install texlive-full

Or if you want to use less disk space:

apt install texlive-latex-extra texlive-fonts-recommended texlive-xetex \
            latexmk fonts-freefont-otf

JSON indices #

The documentation generator can also produce computer-readable JSON files for individual indices with make refman-indices. These files are meant to be useful for tool developers, for instance to power autocompletion in editors. They output files are found in doc/refman-indices/*.json.

Each JSON index has the following shape:

{
  // a key is the name of the index entry
  [string]: {
    // the refman documentation page path for that entry
    "documentation_path": string.
    // the anchor on that page that leads to the documentation entry
    "documentation_anchor": string,
    // the grammar description
    "syntax": Syntax,
    // a simpler, markdown documentation
    "documentation": string,
  }
}

Where Syntax can be used to match some text against the index entry or to propose the user a code snippet. It is of the following shape:

type Syntax =
  | ["Literal", Literal]
  | ["Reference", Reference]
  | ["Alternative", Alternative]
  | ["Repeat", Repeat]

// the literal string
type Literal = {
  value: string
  // an optional subscript, for example "1" which should be rendered as "₁"
  subscript: string | null
}

// a reference to a different entry in the documentation
type Reference = {
  value: string
  // an optional subscript, for example "1" which should be rendered as "₁"
  subscript: string | null
}

// an alternative between a list of options
type Alternative = {
  children: Syntax[]
}

// repetition of a list of syntax nodes
type Repeat = {
  // nodes have to repeat at least this many times
  min: number
  // nodes can repeat up to and including this many times
  max: number | null
  // each repetition has to be separated with this
  separator: string | null
  children: Syntax[]
}

Setting the locale for Python #

Make sure that the locale is configured on your platform so that Python encodes printed messages with utf-8 rather than generating runtime exceptions for non-ascii characters. The .UTF-8 in export LANG=C.UTF-8 sets UTF-8 encoding. The C can be replaced with any supported language code. You can set the default for a Docker build with ENV LANG C.UTF-8. (Python may look at other environment variables to determine the locale; see the Python documentation).

Libraries #

Most of the refman compiles with only the rocq-core package. However, in order to showcase some nice advertising examples with some external libraries included in Coq CI, a few code blocks in the refman depend on those libraries. These blocks are marked with the extra parameter (see sphinx/README.rst for more details). The targets below make those blocks optional but their correct compilation is checked in the CI target doc:ci-refman.

Compilation #

The current documentation targets are:

• make refman-html Build the reference manual in HTML form into _build/default/doc/refman-html

• make refman-pdf Build the reference manual in PDF form into _build/default/doc/refman-pdf

• make corelib-html Build Rocq core library documentation into _build/default/doc/corelib/html

• make refman-indices Build the JSON indices into doc/refman-indices

• make apidoc Build the ML API's documentation into _build/default/_doc/_html

To build the Sphinx documentation without stopping at the first warning, change the value of the SPHINXWARNOPT variable (default is -W). The following will build the Sphinx documentation without stopping at the first warning, and store all the warnings in the file /tmp/warn.log:

SPHINXWARNOPT="-w/tmp/warn.log" make refman-html

Note that inspecting local copies of the docs may behave in unexpected ways if opening the sources with a browser (eg with firefox _build/default/doc/refman-html/index.html). In order to avoid this, either inspect the version generated by the CI or run a local server, for example with:

cd _build/default/doc/refman-html/ && python3 -m http.server

Installation #

The produced documents are stored in the described directories above, you can install them just by copying the contents to the desired directory.

In the future, the rocq-doc and rocq-core opam packages will install the documentation automatically.