From 6f3a8a90514669c84be4de5726fe65f15141ca4d Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Sun, 29 Apr 2018 23:55:51 -0400 Subject: [doc] Add a README to doc/sphinx/ The readme is auto-generated by combining introductory text with the docstrings in coqdomain.py. --- doc/sphinx/README.template.rst | 83 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 83 insertions(+) create mode 100644 doc/sphinx/README.template.rst (limited to 'doc/sphinx/README.template.rst') diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst new file mode 100644 index 0000000000..a387247e52 --- /dev/null +++ b/doc/sphinx/README.template.rst @@ -0,0 +1,83 @@ +============================= + Documenting Coq with Sphinx +============================= + +.. + This README is auto-generated from the coqrst docs; use ``./regen_readme.py`` to rebuild the it. + +Coq's documentation 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 the following 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 + +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. + +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 (``@id``, ``@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 spaces + +``%|``, ``%{``, … + 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] -- cgit v1.2.3 From dc5b6e15a2db658fb36754608683b10f847b3e94 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Mon, 30 Apr 2018 00:32:00 -0400 Subject: [doc] Add an ELisp snippet to insert Sphinx roles and quotes --- doc/sphinx/README.template.rst | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'doc/sphinx/README.template.rst') diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index a387247e52..2f7ba028a3 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -81,3 +81,13 @@ Coq roles In addition to the objects and directives above, the ``coqrst`` Sphinx plugin defines the following roles: [ROLES] + +Tips and tricks +=============== + +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 "") #'coqdev-sphinx-rst-coq-action)) -- cgit v1.2.3 From a6545a120c6587af38883597d20ac28131b813a9 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Mon, 30 Apr 2018 09:53:18 -0400 Subject: [doc] Clarify a comment in the README --- doc/sphinx/README.template.rst | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'doc/sphinx/README.template.rst') diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index 2f7ba028a3..10a4fcadfe 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -3,7 +3,8 @@ ============================= .. - This README is auto-generated from the coqrst docs; use ``./regen_readme.py`` to rebuild the it. + 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 documentation is written in `reStructuredText `_ (“reST”), and compiled with `Sphinx `_. -- cgit v1.2.3 From d5bb8a4ae2f509532ecfb4a53bb91c64d992c2e6 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Fri, 4 May 2018 19:02:11 -0400 Subject: [doc] Address feedback on doc writer guide Co-Authored-By: @Zimmi48 --- doc/sphinx/README.template.rst | 24 ++++++++++++++++-------- 1 file changed, 16 insertions(+), 8 deletions(-) (limited to 'doc/sphinx/README.template.rst') diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index 10a4fcadfe..11bcbb0833 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -6,14 +6,14 @@ 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 documentation is written in `reStructuredText `_ (“reST”), and compiled 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. +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 the following 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 @@ -25,7 +25,7 @@ Our Coq domain define the following objects. Each object has a “signature” 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. +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```. @@ -34,10 +34,10 @@ 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 (``@id``, ``@num``, ``@tactic``) + A placeholder (``@ident``, ``@num``, ``@tactic``\ …) ``{? …}`` an optional block @@ -46,7 +46,7 @@ The signatures of most objects can be written using a succinct DSL for Coq notat an optional (``*``) or mandatory (``+``) block that can be repeated, with repetitions separated by spaces ``{*, …}``, ``{+, …}`` - an optional or mandatory repeatable block, with repetitions separated by spaces + an optional or mandatory repeatable block, with repetitions separated by commas ``%|``, ``%{``, … an escaped character (rendered without the leading ``%``) @@ -86,7 +86,15 @@ In addition to the objects and directives above, the ``coqrst`` Sphinx plugin de Tips and tricks =============== -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. +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 ``_. + +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``:: -- cgit v1.2.3 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.template.rst | 21 ++++++++++++++++++--- 1 file changed, 18 insertions(+), 3 deletions(-) (limited to 'doc/sphinx/README.template.rst') 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 ----- -- cgit v1.2.3