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