\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#3})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

# Documenting Rocq files with rocq doc

`rocq doc` is a documentation tool for the Rocq Prover, similar to `javadoc` or `ocamldoc`. The task of `rocq doc` is

1. to produce a nice LaTeX and/or HTML document from Rocq source files, readable for a human and not only for the proof assistant;

2. to help users navigate their own (or third-party) sources.

## Principles

Documentation is inserted into Rocq files as special comments. Thus your files will compile as usual, whether you use `rocq doc` or not. `rocq doc` presupposes that the given Rocq files are well-formed (at least lexically). Documentation starts with `(**`, followed by a space, and ends with `*)`. The documentation format is inspired by Todd A. Coram’s Almost Free Text (AFT) tool: it is mainly `ASCII` text with some syntax-light controls, described below. `rocq doc` is robust: it shouldn’t fail, whatever the input is. But remember: “garbage in, garbage out”.

### Rocq material inside documentation.

Rocq material is quoted between the delimiters `[` and `]`. Square brackets may be nested, the inner ones being understood as being part of the quoted code (thus you can quote a term like `let id := fun [T : Type] (x : t) => x in id 0` by writing `[let id := fun [T : Type] (x : t) => x in id 0]`). Inside quotations, the code is pretty-printed the same way as in code parts.

Preformatted vernacular is enclosed by `[[` and `]]`. The former must be followed by a newline and the latter must follow a newline.

### Pretty-printing.

`rocq doc` uses different faces for identifiers and keywords. The pretty- printing of Rocq tokens (identifiers or symbols) can be controlled using one of the following commands:

    (** printing  *token* %...LATEX...% #...html...# *)

or

    (** printing  *token* $...LATEX math...$ #...html...# *)

It gives the LaTeX and HTML texts to be produced for the given Rocq token. Either the LaTeX or the HTML rule may be omitted, causing the default pretty-printing to be used for this token.

The printing for one token can be removed with

    (** remove printing  *token* *)

Initially, the pretty-printing table contains the following mapping:

`->` | → |  | `<-` | ← |  | `*` | ×
`<=` | ≤ |  | `>=` | ≥ |  | `=>` | ⇒
`<>` | ≠ |  | `<->` | ↔ |  | `|-` | ⊢
`\/` | ∨ |  | `/\` | ∧ |  | `~` | ¬

Any of these can be overwritten or suppressed using the printing commands.

Note

The recognition of tokens is done by a (`ocaml`) lex automaton and thus applies the longest-match rule. For instance, `->~` is recognized as a single token, where Rocq sees two tokens. It is the responsibility of the user to insert space between tokens or to give pretty-printing rules for the possible combinations, e.g.

    (** printing ->~ %\ensuremath{\rightarrow\lnot}% *)

### Sections

Sections are introduced by 1 to 4 asterisks at the beginning of a line followed by a space and the title of the section. One asterisk is a section, two a subsection, etc.

Example

    (** * Well-founded relations

        In this section, we introduce...  *)

### Lists.

List items are introduced by a leading dash. `rocq doc` uses whitespace to determine the depth of a new list item and which text belongs in which list items. A list ends when a line of text starts at or before the level of indenting of the list’s dash. A list item’s dash must always be the first non-space character on its line (so, in particular, a list can not begin on the first line of a comment - start it on the second line instead).

Example

    We go by induction on [n]:
    - If [n] is 0...
    - If [n] is [S n'] we require...

      two paragraphs of reasoning, and two subcases:

      - In the first case...
      - In the second case...

    So the theorem holds.

### Rules.

More than 4 leading dashes produce a horizontal rule.

### Emphasis.

Text can be italicized by enclosing it in underscores. A non-identifier character must precede the leading underscore and follow the trailing underscore, so that uses of underscores in names aren’t mistaken for emphasis. Usually, these are spaces or punctuation.

    This sentence contains some _emphasized text_.

### Escaping to LaTeX and HTML.

Pure LaTeX or HTML material can be inserted using the following escape sequences:

- `$...LATEX stuff...$` inserts some LaTeX material in math mode. Simply discarded in HTML output.

- `%...LATEX stuff...%` inserts some LaTeX material. Simply discarded in HTML output.

- `#...HTML stuff...#` inserts some HTML material. Simply discarded in LaTeX output.

Note

to simply output the characters `$`, `%` and `#` and escaping their escaping role, these characters must be doubled.

### Verbatim

Verbatim material is introduced by a leading `<<` and closed by `>>` at the beginning of a line.

Example

    Here is the corresponding caml code:
    <<
      let rec fact n =
        if n <= 1 then 1 else n * fact (n-1)
    >>

Verbatim material on a single line is also possible (assuming that `>>` is not part of the text to be presented as verbatim).

Example

    Here is the corresponding caml expression: << fact (n-1) >>

### Hyperlinks

Hyperlinks can be inserted into the HTML output, so that any identifier is linked to the place of its definition.

`rocq c file.v` automatically dumps localization information in `file.glob` or appends it to a file specified using the option `--dump-glob file`. Take care of erasing this global file, if any, when starting the whole compilation process.

Then invoke `rocq doc` or `rocq doc --glob-from file` to tell `rocq doc` to look for name resolutions in the file `file` (it will look in `file.glob` by default).

Identifiers from the Rocq standard library are linked to the Coq website https://rocq-prover.org/stdlib. This behavior can be changed using command line options `--no-externals` and `--coqlib_url`; see below.

### Hiding / Showing parts of the source

Some parts of the source can be hidden using command line options `-g` and `-l` (see below), or using such comments:

    (* begin hide *)
     *some Rocq material*
    (* end hide *)

Conversely, some parts of the source which would be hidden can be shown using such comments:

    (* begin show *)
     *some Rocq material*
    (* end show *)

The latter cannot be used around some inner parts of a proof, but can be used around a whole proof.

Lastly, it is possible to adopt a middle-ground approach when the desired output is HTML, where a given snippet of Rocq material is hidden by default, but can be made visible with user interaction.

    (* begin details *)
     *some Rocq material*
    (* end details *)

There is also an alternative syntax available.

    (* begin details : Some summary describing the snippet *)
     *some Rocq material*
    (* end details *)

## Usage

`rocq doc` is invoked on a shell command line as follows: `rocq doc <options and files>`. Any command line argument which is not an option is considered to be a file (even if it starts with a `-`). Rocq files are identified by the suffixes `.v` and `.g` and LaTeX files by the suffix `.tex`.

HTML output:

  This is the default output format. One HTML file is created for each Rocq file given on the command line, together with a file `index.html` (unless option `--no-index` is passed). The HTML pages use a style sheet named `style.css`. Such a file is distributed with `rocq doc`.

LaTeX output:

  A single LaTeX file is created, on standard output. It can be redirected to a file using the option `-o`. The order of files on the command line is kept in the final document. LaTeX files given on the command line are copied ‘as is’ in the final document . DVI and PostScript can be produced directly with the options `-dvi` and `-ps` respectively.

TEXmacs output:

  To translate the input files to TEXmacs format, to be used by the TEXmacs Rocq interface.

### Command line options

Overall options

> --HTML:

>   Select a HTML output.

> --LaTeX:

>   Select a LaTeX output.

> --dvi:

>   Select a DVI output.

> --ps:

>   Select a PostScript output.

> --texmacs:

>   Select a TEXmacs output.

> --stdout:

>   Write output to stdout.

> -o file, --output file:

>   Redirect the output into the file ‘file’ (meaningless with `-html`).

> -d dir, --directory dir:

>   Output files into directory ‘dir’ instead of the current directory (option `-d` does not change the filename specified with the option `-o`, if any).

> --body-only:

>   Suppress the header and trailer of the final document. Thus, you can insert the resulting document into a larger one.

> -p string, --preamble string:

>   Insert some material in the LaTeX preamble, right before `\begin{document}` (meaningless with `-html`).

> --vernac-file file,--tex-file file:

>   Considers the file ‘file’ respectively as a `.v` (or `.g`) file or a `.tex` file.

> --files-from file:

>   Read filenames to be processed from the file ‘file’ as if they were given on the command line. Useful for program sources split up into several directories.

> -q, --quiet:

>   Be quiet. Do not print anything except errors.

> -h, --help:

>   Give a short summary of the options and exit.

> -v, --version:

>   Print the version and exit.

Index options

> The default behavior is to build an index, for the HTML output only, into `index.html`.

> --no-index:

>   Do not output the index.

> --binder-index:

>   Include variable binders in the index. Not recommended with large source files, where binder information may dominate the index.

> --multi-index:

>   Generate one page for each category and each letter in the index, together with a top page `index.html`.

> --index string:

>   Make the filename of the index "`string`.html" instead of “index.html”. Useful since “index.html” is special.

Table of contents option

> -toc, --table-of-contents:

>   Insert a table of contents. For a LaTeX output, it inserts a `\tableofcontents` at the beginning of the document. For a HTML output, it builds a table of contents into `toc.html`.

> --toc-depth int:

>   Only include headers up to depth `int` in the table of contents.

Hyperlink options

> --glob-from file:

>   Make references using Rocq globalizations from file file. (Such globalizations are obtained with Rocq option `-dump-glob`).

> --no-externals:

>   Do not insert links to the Rocq standard library.

> --external url coqdir:

>   Use given URL for linking references whose name starts with prefix `coqdir`.

> --coqlib_url url:

>   Set base URL for the Rocq standard library (default is https://rocq-prover.org/stdlib). This is equivalent to `--external url Stdlib`.

> -R dir coqdir:

>   Recursively map physical directory dir to Rocq logical directory `coqdir` (similarly to Rocq option `-R`).

> -Q dir coqdir:

>   Map physical directory dir to Rocq logical directory `coqdir` (similarly to Rocq option `-Q`).

>   Note

>   options `-R` and `-Q` only have effect on the files following them on the command line, so you will probably need to put this option first.

Title options

> -s , --short:

>   Do not insert titles for the files. The default behavior is to insert a title like “Library Foo” for each file.

> --lib-name string:

>   Print “string Foo” instead of “Library Foo” in titles. For example “Chapter” and “Module” are reasonable choices.

> --no-lib-name:

>   Print just “Foo” instead of “Library Foo” in titles.

> --lib-subtitles:

>   Look for library subtitles. When enabled, the first line of each file is checked for a comment of the form:

>       (** * ModuleName : text *)

>   where `ModuleName` must be the name of the file. If it is present, the text is used as a subtitle for the module in appropriate places.

> -t string, --title string:

>   Set the document title.

Contents options

> -g, --gallina:

>   Do not print proofs.

> -l, --light:

>   Light mode. Suppress proofs (as with `-g`) and the following commands:

>   > - [Recursive] Tactic Definition

>   > - Hint / Hints

>   > - Require

>   > - Transparent / Opaque

>   > - Implicit Argument / Implicits

>   > - Section / Variable / Hypothesis / End

>   The behavior of options `-g` and `-l` can be locally overridden using the `(* begin show *) … (* end show *)` environment (see above).

>   There are a few options that control the parsing of comments:

> --parse-comments:

>   Parse regular comments delimited by `(*` and `*)` as well. They are typeset inline.

> --plain-comments:

>   Do not interpret comments, simply copy them as plain-text.

> --interpolate:

>   Use the globalization information to typeset identifiers appearing in Rocq escapings inside comments.

Language options

> The default behavior is to assume ASCII 7 bit input files.

> -latin1, --latin1:

>   Select ISO-8859-1 input files. It is equivalent to --inputenc latin1 --charset iso-8859-1.

> -utf8, --utf8:

>   Set --inputenc utf8x for LaTeX output and --charset utf-8 for HTML output. Also use Unicode replacements for a couple of standard plain ASCII notations such as → for `->` and ∀ for `forall`. LaTeX UTF-8 support can be found at http://www.ctan.org/pkg/unicode. For the interpretation of Unicode characters by LaTeX, extra packages which `rocq doc` does not provide by default might be required, such as textgreek for some Greek letters or `stmaryrd` for some mathematical symbols. If a Unicode character is missing an interpretation in the utf8x input encoding, add `\DeclareUnicodeCharacter{code}{LATEX-interpretation}`. Packages and declarations can be added with option `-p`.

> --inputenc string:

>   Give a LaTeX input encoding, as an option to LaTeX package `inputenc`.

> --charset string:

>   Specify the HTML character set, to be inserted in the HTML header.

### Custom HTML header and footer

With `--with-header` and `--with-footer` respectively, in HTML mode `rocq doc` will include the header at the beginning and the footer at the end of the file.

Additionally the string `@@TITLE@@` is replaced by the page title in the header file.

## The rocq doc LaTeX style file

In case you choose to produce a document without the default LaTeX preamble (by using option `--no-preamble`), then you must insert into your own preamble the command

    \usepackage{coqdoc}

The package optionally takes the argument `[color]` to typeset identifiers with colors (this requires the `xcolor` package).

Then you may alter the rendering of the document by redefining some macros:

coqdockw, coqdocid, …:

  The one-argument macros for typesetting keywords and identifiers. Defaults are sans-serif for keywords and italic for identifiers.For example, if you would like a slanted font for keywords, you may insert

      \renewcommand{\coqdockw}[1]{\textsl{#1}}

  anywhere between `\usepackage{coqdoc}` and `\begin{document}`.

coqdocmodule:

  One-argument macro for typesetting the title of a `.v` file. Default is

      \newcommand{\coqdocmodule}[1]{\section*{Module #1}}

  and you may redefine it using `\renewcommand`.

Other versions v: 9.2

Versions
  dev
  stable
  9.2
  9.1
  9.0
  8.20
  8.19
  8.18
  8.17
  8.16
  8.15
  8.14
  8.13
  8.12
  8.11
  8.10
  8.9
  8.8
  8.7
  8.6
  8.5
  8.4
  8.3
  8.2
  8.1
  8.0

Downloads
  PDF