Skip to content

Latest commit

 

History

History
 
 

sphinx

README.rst

Documenting Coq with Sphinx

Coq's reference manual is written in reStructuredText (“reST”), and compiled with Sphinx.

In addition to standard reST directives (a directive is similar to a LaTeX environment) and roles (a role is similar to a LaTeX command), the coqrst plugin loaded by the documentation uses a custom Coq domain — a set of Coq-specific directives that define objects like tactics, commands (vernacs), warnings, etc. —, some custom directives, and a few custom roles. Finally, this manual uses a small DSL to describe tactic invocations and commands.

Coq objects

Our Coq domain define multiple objects. Each object has a signature (think type signature), followed by an optional body (a description of that object). The following example defines two objects: a variant of the simpl tactic, and an error that it may raise:

.. tacv:: simpl @pattern at {+ @num}
   :name: simpl_at

   This applies ``simpl`` only to the :n:`{+ @num}` occurrences of the subterms
   matching :n:`@pattern` in the current goal.

   .. exn:: Too few occurrences
      :undocumented:

Objects are automatically collected into indices, and can be linked to using the role version of the object's directive. For example, you could link to the tactic variant above using :tacv:`simpl_at`, and to its exception using :exn:`Too few occurrences`.

Names (link targets) are auto-generated for most simple objects, though they can always be overwritten using a :name: option, as shown above.

  • Options, errors, warnings have their name set to their signature, with ... replacing all notation bits. For example, the auto-generated name of .. exn:: @qualid is not a module is ... is not a module, and a link to it would take the form :exn:`... is not a module`.
  • Vernacs (commands) have their name set to the first word of their signature. For example, the auto-generated name of Axiom @ident : @term is Axiom, and a link to it would take the form :cmd:`Axiom`.
  • Vernac variants, tactic notations, and tactic variants do not have a default name.

Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms). Undocumented objects should have the :undocumented: flag instead, as shown above. When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects):

.. cmdv:: Lemma @ident {? @binders} : @type
          Remark @ident {? @binders} : @type
          Fact @ident {? @binders} : @type
          Corollary @ident {? @binders} : @type
          Proposition @ident {? @binders} : @type
   :name: Lemma; Remark; Fact; Corollary; Proposition

   These commands are all synonyms of :n:`Theorem @ident {? @binders } : type`.

Notations

The signatures of most objects can be written using a succinct DSL for Coq notations (think regular expressions written with a Lispy syntax). A typical signature might look like Hint Extern @num {? @pattern} => @tactic, which means that the Hint Extern command takes a number (num), followed by an optional pattern, and a mandatory tactic. The language has the following constructs (the full grammar is in TacticNotations.g):

@…
A placeholder (@ident, @num, @tactic…)
{? …}
an optional block
{* …}, {+ …}
an optional (*) or mandatory (+) block that can be repeated, with repetitions separated by spaces
{*, …}, {+, …}
an optional or mandatory repeatable block, with repetitions separated by commas
%|, %{, …
an escaped character (rendered without the leading %)

As an exercise, what do the following patterns mean?

pattern {+, @term {? at {+ @num}}}
generalize {+, @term at {+ @num} as @ident}
fix @ident @num with {+ (@ident {+ @binder} {? {struct @ident'}} : @type)}

Objects

Here is the list of all objects of the Coq domain (The symbol ✒️ indicates an object whose signature can be written using the notations DSL):

.. cmd:: ✒️ A Coq command.

Example:

.. cmd:: Infix "@symbol" := @term ({+, @modifier}).

   This command is equivalent to :n:`…`.
.. cmdv:: ✒️ A variant of a Coq command.

Example:

.. cmd:: Axiom @ident : @term.

   This command links :token:`term` to the name :token:`term` as its specification in
   the global context. The fact asserted by :token:`term` is thus assumed as a
   postulate.

   .. cmdv:: Parameter @ident : @term.

      This is equivalent to :n:`Axiom @ident : @term`.
.. exn:: ✒️ An error raised by a Coq command or tactic.

This commonly appears nested in the .. tacn:: that raises the exception.

Example:

.. tacv:: assert @form by @tactic

   This tactic applies :n:`@tactic` to solve the subgoals generated by
   ``assert``.

   .. exn:: Proof is not complete

      Raised if :n:`@tactic` does not fully solve the goal.
.. opt:: ✒️ A Coq option.

Example:

.. opt:: Nonrecursive Elimination Schemes

   This option controls whether types declared with the keywords
   :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the
   induction principles.
.. prodn:: ✒️ Grammar productions.
This is useful if you intend to document individual grammar productions. Otherwise, use Sphinx's production lists.
.. tacn:: ✒️ A tactic, or a tactic notation.

Example:

.. tacn:: do @num @expr

   :token:`expr` is evaluated to ``v`` which must be a tactic value. …
.. tacv:: ✒️ A variant of a tactic.

Example:

.. tacn:: fail

   This is the always-failing tactic: it does not solve any goal. It is
   useful for defining other tacticals since it can be caught by
   :tacn:`try`, :tacn:`repeat`, :tacn:`match goal`, or the branching
   tacticals. …

   .. tacv:: fail @natural

      The number is the failure level. If no level is specified, it
      defaults to 0. …
.. thm:: A theorem.

Example:

.. thm:: Bound on the ceiling function

   Let :math:`p` be an integer and :math:`c` a rational constant. Then
   :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`.
.. warn:: ✒️ An warning raised by a Coq command or tactic..

Do not mistake this for .. warning::; this directive is for warning messages produced by Coq.

Example:

.. warn:: Ambiguous path

   When the coercion :token:`qualid` is added to the inheritance graph, non
   valid coercion paths are ignored.

Coq directives

In addition to the objects above, the coqrst Sphinx plugin defines the following directives:

.. coqtop:: A reST directive to describe interactions with Coqtop.

Usage:

.. coqtop:: options…

   Coq code to send to coqtop

Example:

.. coqtop:: in reset undo

   Print nat.
   Definition a := 1.

Here is a list of permissible options:

  • Display options
    • all: Display input and output
    • in: Display only input
    • out: Display only output
    • none: Display neither (useful for setup commands)
  • Behavior options
    • reset: Send a Reset Initial command before running this block
    • undo: Send an Undo n (n = number of sentences) command after running all the commands in this block

coqtop's state is preserved across consecutive .. coqtop:: blocks of the same document (coqrst creates a single coqtop process per reST source file). Use the reset option to reset Coq's state.

.. coqdoc:: A reST directive to display Coqtop-formatted source code.

Usage:

.. coqdoc::

   Coq code to highlight

Example:

.. coqdoc::

   Definition test := 1.
.. example:: A reST directive for examples.

This behaves like a generic admonition; see http://docutils.sourceforge.net/docs/ref/rst/directives.html#generic-admonition for more details.

Example:

.. example:: Adding a hint to a database

   The following adds ``plus_comm`` to the ``plu`` database:

   .. coqdoc::

      Hint Resolve plus_comm : plu.
.. inference:: A reST directive to format inference rules.

This also serves as a small illustration of the way to create new Sphinx directives.

Usage:

.. inference:: name

   newline-separated premisses
   ------------------------
   conclusion

Example:

.. inference:: Prod-Pro

   \WTEG{T}{s}
   s \in \Sort
   \WTE{\Gamma::(x:T)}{U}{\Prop}
   -----------------------------
   \WTEG{\forall~x:T,U}{\Prop}
.. preamble:: A reST directive for hidden math.

Mostly useful to let MathJax know about defs and newcommands.

Example:

.. preamble::

   \newcommand{\paren}[#1]{\left(#1\right)}

Coq roles

In addition to the objects and directives above, the coqrst Sphinx plugin defines the following roles:

:g: Coq code.

Use this for Gallina and Ltac snippets:

:g:`apply plus_comm; reflexivity`
:g:`Set Printing All.`
:g:`forall (x: t), P(x)`
:n: Any text using the notation syntax (@id, {+, …}, etc.).

Use this to explain tactic equivalences. For example, you might write this:

:n:`generalize @term as @ident` is just like :n:`generalize @term`, but
it names the introduced hypothesis :token:`ident`.

Note that this example also uses :token:. That's because ident is defined in the the Coq manual as a grammar production, and :token: creates a link to that. When referring to a placeholder that happens to be a grammar production, :token:`…` is typically preferable to :n:`@…`.

:production: A grammar production not included in a productionlist directive.

Useful to informally introduce a production, as part of running text.

Example:

:production:`string` indicates a quoted string.

You're not likely to use this role very commonly; instead, use a production list and reference its tokens using :token:`…`.

Common mistakes

Improper nesting

DO
.. cmd:: Foo @bar

   Foo the first instance of :token:`bar`\ s.

   .. cmdv:: Foo All

      Foo all the :token:`bar`\ s in
      the current context
DON'T
.. cmd:: Foo @bar

Foo the first instance of :token:`bar`\ s.

.. cmdv:: Foo All

Foo all the :token:`bar`\ s in
the current context

You can set the report_undocumented_coq_objects setting in conf.py to "info" or "warning" to get a list of all Coq objects without a description.

Overusing :token:

DO
This is equivalent to :n:`Axiom @ident : @term`.
DON'T
This is equivalent to ``Axiom`` :token`ident` : :token:`term`.

Omitting annotations

DO
.. tacv:: assert @form as @intro_pattern
DON'T
.. tacv:: assert form as intro_pattern

Tips and tricks

Nested lemmas

The .. coqtop:: directive does not reset Coq after running its contents. That is, the following will create two nested lemmas:

.. coqtop:: all

   Lemma l1: 1 + 1 = 2.

.. coqtop:: all

   Lemma l2: 2 + 2 <> 1.

Add either undo to the first block or reset to the second block to avoid nesting lemmas.

Abbreviations and macros

Abbreviations and placeholders for specially-formatted names (like |Cic|, |Coq|, |CoqIDE|, |Ltac|, and |Gallina|) are defined in a separate file included by most chapters of the manual. Some useful LaTeX macros are defined in /doc/sphinx/preamble.rst.

Emacs

The dev/tools/coqdev.el folder contains a convenient Emacs function to quickly insert Sphinx roles and quotes. It takes a single character (one of gntm:`), and inserts one of :g:, :n:, :t:, or an arbitrary role, or double quotes. You can also select a region of text, and wrap it in single or double backticks using that function.

Use the following snippet to bind it to F12 in rst-mode:

(with-eval-after-load 'rst
  (define-key rst-mode-map (kbd "<f12>") #'coqdev-sphinx-rst-coq-action))