From e266976abc8c170c1e4bf1c98629c190b844f1ab Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Sat, 5 May 2018 12:25:46 -0400 Subject: [doc] More feedback on doc writer guide Co-Authored-By: @Zimmi48 --- doc/sphinx/README.rst | 25 +++++++++++++++++++------ doc/sphinx/README.template.rst | 21 ++++++++++++++++++--- doc/tools/coqrst/coqdomain.py | 3 +-- 3 files changed, 38 insertions(+), 11 deletions(-) diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 4dba012163..5f2f21f2b8 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -13,7 +13,7 @@ In addition to standard reST directives (a directive is similar to a LaTeX envir 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:: +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 @@ -34,7 +34,7 @@ Names (link targets) are auto-generated for most simple objects, though they can 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 `_): +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``\ …) @@ -279,9 +279,7 @@ In addition to the objects and directives above, the ``coqrst`` Sphinx plugin de 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 Sphinx role to format grammar productions not included in a - `productionlist` directive. - +``:production:`` A grammar production not included in a ``productionlist`` directive. Useful to informally introduce a production, as part of running text. Example:: @@ -296,10 +294,25 @@ In addition to the objects and directives above, the ``coqrst`` Sphinx plugin de 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|``, and ``|Gallina|``) are defined in a `separate file `_ included by most chapters of the manual. Some useful LaTeX macros (like ``\alors``), are defined in ``_. +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 ``_. Emacs ----- diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index 11bcbb0833..203251abf4 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -13,7 +13,7 @@ In addition to standard reST directives (a directive is similar to a LaTeX envir 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:: +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 @@ -34,7 +34,7 @@ Names (link targets) are auto-generated for most simple objects, though they can 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 `_): +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``\ …) @@ -86,10 +86,25 @@ In addition to the objects and directives above, the ``coqrst`` Sphinx plugin de 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|``, and ``|Gallina|``) are defined in a `separate file `_ included by most chapters of the manual. Some useful LaTeX macros (like ``\alors``), are defined in ``_. +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 ``_. Emacs ----- diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index f8bb113a7b..606d725bf0 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -829,8 +829,7 @@ class IndexXRefRole(XRefRole): return title, target def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, content=[]): - """A Sphinx role to format grammar productions not included in a - `productionlist` directive. + """A grammar production not included in a ``productionlist`` directive. Useful to informally introduce a production, as part of running text. -- cgit v1.2.3