1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
|
=============================
Documenting Coq with Sphinx
=============================
..
README.rst is auto-generated from README.template.rst and the coqrst docs;
use ``doc/tools/coqrst/regen_readme.py`` to rebuild it.
Coq's reference manual is written in `reStructuredText <http://www.sphinx-doc.org/en/master/usage/restructuredtext/basics.html>`_ (“reST”), and compiled with `Sphinx <http://www.sphinx-doc.org/en/master/>`_.
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 </doc/tools/coqrst/notations/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 ``%``)
..
FIXME document the new subscript support
As an exercise, what do the following patterns mean?
.. code::
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 :black_nib: indicates an object whose signature can be written using the notations DSL):
[OBJECTS]
Coq directives
==============
In addition to the objects above, the ``coqrst`` Sphinx plugin defines the following directives:
[DIRECTIVES]
Coq roles
=========
In addition to the objects and directives above, the ``coqrst`` Sphinx plugin defines the following roles:
[ROLES]
Common mistakes
===============
Improper nesting
----------------
DO
.. code::
.. 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
.. code::
.. 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
.. code::
This is equivalent to :n:`Axiom @ident : @term`.
DON'T
.. code::
This is equivalent to ``Axiom`` :token`ident` : :token:`term`.
Omitting annotations
--------------------
DO
.. code::
.. tacv:: assert @form as @intro_pattern
DON'T
.. code::
.. 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 </doc/sphinx/replaces.rst>`_ 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 :kbd:`F12` in ``rst-mode``::
(with-eval-after-load 'rst
(define-key rst-mode-map (kbd "<f12>") #'coqdev-sphinx-rst-coq-action))
|
