diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/MIGRATING | 238 | ||||
| -rw-r--r-- | doc/sphinx/README.rst | 325 | ||||
| -rw-r--r-- | doc/sphinx/README.template.rst | 117 | ||||
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 22 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 5 | ||||
| -rwxr-xr-x | doc/sphinx/conf.py | 12 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 28 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/proof-schemes.rst | 16 |
9 files changed, 488 insertions, 279 deletions
diff --git a/doc/sphinx/MIGRATING b/doc/sphinx/MIGRATING deleted file mode 100644 index fa6fe15379..0000000000 --- a/doc/sphinx/MIGRATING +++ /dev/null @@ -1,238 +0,0 @@ -How to migrate the Coq Reference Manual to Sphinx -================================================= - -# Install Python3 packages (requires Python 3, python3-pip, python3-setuptools) - - * pip3 install bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex - -# You may want to do this under a virtualenv, particularly if you end up with issues finding sphinxcontrib.bibtex. http://docs.python-guide.org/en/latest/dev/virtualenvs/ - - * pip3 install virtualenv - * virtualenv coqsphinxing # you may want to use -p to specify the python version - * source coqsphinxing/bin/activate # activate the virtual environment - -# After activating the virtual environment you can run the above pip3 command to install sphinx. You will have to activate the virtual environment before building the docs in your session. - -# Add this Elisp code to .emacs, if you're using emacs (recommended): - - (defun sphinx/quote-coq-refman-region (left right &optional beg end count) - (unless beg - (if (region-active-p) - (setq beg (region-beginning) end (region-end)) - (setq beg (point) end nil))) - (unless count - (setq count 1)) - (save-excursion - (goto-char (or end beg)) - (dotimes (_ count) (insert right))) - (save-excursion - (goto-char beg) - (dotimes (_ count) (insert left))) - (if (and end (characterp left)) ;; Second test handles the ::`` case - (goto-char (+ (* 2 count) end)) - (goto-char (+ count beg)))) - - (defun sphinx/coqtop (beg end) - (interactive (list (region-beginning) (region-end))) - (replace-regexp "^Coq < " " " nil beg end) - (indent-rigidly beg end -3) - (goto-char beg) - (insert ".. coqtop:: all\n\n")) - - (defun sphinx/rst-coq-action () - (interactive) - (pcase (read-char "Command?") - (?g (sphinx/quote-coq-refman-region ":g:`" "`")) - (?n (sphinx/quote-coq-refman-region ":n:`" "`")) - (?t (sphinx/quote-coq-refman-region ":token:`" "`")) - (?m (sphinx/quote-coq-refman-region ":math:`" "`")) - (?: (sphinx/quote-coq-refman-region "::`" "`")) - (?` (sphinx/quote-coq-refman-region "``" "``")) - (?c (sphinx/coqtop (region-beginning) (region-end))))) - - (global-set-key (kbd "<f12>") #'sphinx/rst-coq-action) - - With this code installed, you can hit "F12" followed by an appropriate key to do quick markup of text - (this will make more sense once you've started editing the text). - -# Fork the Coq repo, if needed: - - https://github.com/coq/coq - -# Clone the repo to your work machine - -# Add Maxime Dénès's repo as a remote: - - git remote add sphinx https://github.com/maximedenes/coq.git - - (or choose a name other than "sphinx") - - Verify with: - - git remote -v - -# Fetch from the remote - - git fetch sphinx - -# Checkout the sphinx-doc branch - - git checkout sphinx-doc - - You should pull from the repo from time to time to keep your local copy up-to-date: - - git pull sphinx sphinx-doc - - You may want to create a new branch to do your work in. - -# Choose a Reference Manual chapter to work on at - - https://docs.google.com/document/d/1Yo7dV4OI0AY9Di-lsEQ3UTmn5ygGLlhxjym7cTCMCWU - -# For each chapter, raw ReStructuredText (the Sphinx format), created by the "html2rest" utility, - is available in the directory porting/raw-rst/ - - Elsewhere, depending on the chapter, there should be an almost-empty template file already created, - which is in the location where the final version should go - -# Manually edit the .rst file, place it in the correct location - - There are small examples in sphinx/porting/, a larger example in language/gallina-extensions.rst - - (N.B.: the migration is a work-in-progress, your suggestions are welcome) - - Find the chapter you're working on from the online manual at https://coq.inria.fr/distrib/current/refman/. - At the top of the file, after the chapter heading, add: - - :Source: https://coq.inria.fr/distrib/current/refman/the-chapter-file.html - :Converted by: Your Name - - N.B.: These source and converted-by annotations should help for the migration phase. Later on, - those annotations will be removed, and contributors will be mentioned in the Coq credits. - - Remove chapter numbers - - Replace section, subsection numbers with reference labels: - - .. _some-reference-label: - - Place the label before the section or subsection, followed by a blank line. - - Note the leading underscore. Use :ref:`some_reference-label` to refer to such a label; note the leading underscore is omitted. - Many cross-references may be to other chapters. If the required label exists, use it. Otherwise, use a dummy reference of the form - `TODO-n.n.n-mnemonic` we can fixup later. Example: - - :ref:`TODO-1.3.2-definitions` - - We can grep for those TODOs, and the existing subsection number makes it easy to find in the exisyting manual. - - For the particular case of references to chapters, we can use a -convention for the cross-reference name, so no TODO is needed. - - :ref:`thegallinaspecificationlanguage` - -That is, the chapter label is the chapter title, all in lower-case, -with no spaces or punctuation. For chapters with subtitles marked with -a ":", like those for Omega and Nsatz, use just the chapter part -preceding the ":". These labels should already be in the -placeholder .rst files for each chapter. - - - You can also label other items, like grammars, with the same syntax. To refer to such labels, not involving a - section or subsection, use the syntax - - :ref:`Some link text <label-name>` - - Yes, the angle-brackets are needed here! - - For bibliographic references (those in biblio.bib), use :cite:`thecitation`. - - Grammars will get mangled by the translation. Look for "productionlist" in the examples, also see - http://www.sphinx-doc.org/en/stable/markup/para.html. - - For Coq examples that appear, look at the "coqtop" syntax in porting/tricky-bits.rst. The Sphinx - script will run coqtop on those examples, and can show the output (or not). - - The file replaces.rst contains replacement definitions for some items that are clumsy to write out otherwise. - Use - - .. include:: replaces.rst - - to gain access to those definitions in your file (you might need a path prefix). Some especially-important - replacements are |Cic|, |Coq|, |CoqIDE|, and |Gallina|, which display those names in small-caps. Please use them, - so that they're rendered consistently. - - Similarly, there are some LaTeX macros in preamble.rst that can be useful. - - Conventions: - - - Keywords and other literal text is double-backquoted (e.g. ``Module``, ``Section``, ``(``, ``,``). - - - Metavariables are single-backquotes (e.g. `term`, `ident`) - - - Use the cmd directive for Vernacular commands, like: - - .. cmd:: Set Printing All. - - Within this directive, prefix metavariables (ident, term) with @: - - .. cmd:: Add Printing Let @ident. - - There's also the "cmdv" directive for variants of a command. - - - Use the "exn" and "warn" directives for errors and warnings: - - .. exn:: Something's not right. - .. warn:: You shouldn't do that. - - - Use the "example" directive for examples - - - Use the "g" role for inline Gallina, like :g:`fun x => x` - - - Use code blocks for blocks of Gallina. You can use a double-colon at the end of a line:: - - your code here - - which prints a single colon, or put the double-colon on a newline. - -:: - - your other code here - -# Making changes to the text - - The goal of the migration is simply to change the storage format from LaTeX to ReStructuredText. The goal is not - to make any organizational or other substantive changes to the text. If you do notice nits (misspellings, wrong - verb tense, and so on), please do change them. For example, the programming language that Coq is written in is these days - called "OCaml", and there are mentions of the older name "Objective Caml" in the reference manual that should be changed. - -# Build, view the manual - - In the root directory of your local repo, run "make sphinx". You can view the result in a browser by loading the HTML file - associated with your chapter, which will be contained in the directory doc/sphinx/_build/html/ beneath the repo root directory. - Make any changes you need until there are no build warnings and the output is perfect. :-) - -# Creating pull requests - - When your changes are done, commit them, push to your fork: - - git commit -m "useful commit message" file - git push origin sphinx-doc - - (or push to another branch, if you've created one). Then go to your GitHub - fork and create a pull request against Maxime's sphinx-doc - branch. If your commit is recent, you should see a link on your - fork's code page to do that. Otherwise, you may need to go to your - branch on GitHub to do that. - -# Issues/Questions/Suggestions - - As the migration proceeds, if you have technical issues, have a more general question, or want to suggest something, please contact: - - Paul Steckler <steck@stecksoft.com> - Maxime Dénès <maxime.denes@inria.fr> - -# Issues - - Should the stuff in replaces.rst go in preamble.rst? - In LaTeX, some of the grammars add productions to existing nonterminals, like term ++= ... . How to indicate that? diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst new file mode 100644 index 0000000000..5f2f21f2b8 --- /dev/null +++ b/doc/sphinx/README.rst @@ -0,0 +1,325 @@ +============================= + 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 + +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 </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): + +``.. cmd::`` :black_nib: A Coq command. + Example:: + + .. cmd:: Infix "@symbol" := @term ({+, @modifier}). + + This command is equivalent to :n:`…`. + +``.. cmdv::`` :black_nib: 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::`` :black_nib: 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::`` :black_nib: 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::`` :black_nib: Grammar productions. + This is useful if you intend to document individual grammar productions. + Otherwise, use Sphinx's `production lists + <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_. + +``.. tacn::`` :black_nib: A tactic, or a tactic notation. + Example:: + + .. tacn:: do @num @expr + + :token:`expr` is evaluated to ``v`` which must be a tactic value. … + +``.. tacv::`` :black_nib: 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::`` :black_nib: 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 `\def`\ s and `\newcommand`\ s. + + 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 + <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_ + and reference its tokens using ``:token:`…```. + +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)) diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst new file mode 100644 index 0000000000..203251abf4 --- /dev/null +++ b/doc/sphinx/README.template.rst @@ -0,0 +1,117 @@ +============================= + 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 + +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 </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] + +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)) diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 152f4f6552..09faa06765 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -140,29 +140,29 @@ Declaration of Coercions .. warn:: Ambiguous path. - When the coercion `qualid` is added to the inheritance graph, non - valid coercion paths are ignored; they are signaled by a warning - displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`. + When the coercion :token:`qualid` is added to the inheritance graph, non + valid coercion paths are ignored; they are signaled by a warning + displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`. .. cmdv:: Local Coercion @qualid : @class >-> @class - Declares the construction denoted by `qualid` as a coercion local to - the current section. + Declares the construction denoted by `qualid` as a coercion local to + the current section. .. cmdv:: Coercion @ident := @term - This defines `ident` just like ``Definition`` `ident` ``:=`` `term`, - and then declares `ident` as a coercion between it source and its target. + This defines `ident` just like ``Definition`` `ident` ``:=`` `term`, + and then declares `ident` as a coercion between it source and its target. .. cmdv:: Coercion @ident := @term : @type - This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`, - and then declares `ident` as a coercion between it source and its target. + This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`, + and then declares `ident` as a coercion between it source and its target. .. cmdv:: Local Coercion @ident := @term - This defines `ident` just like ``Let`` `ident` ``:=`` `term`, - and then declares `ident` as a coercion between it source and its target. + This defines `ident` just like ``Let`` `ident` ``:=`` `term`, + and then declares `ident` as a coercion between it source and its target. Assumptions can be declared as coercions at declaration time. This extends the grammar of assumptions from diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index f887a5feea..0e9c23b9bb 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -150,9 +150,10 @@ are a way to take into account the discreteness of :math:`\mathbb{Z}` by roundin .. _ceil_thm: -**Theorem**. Let :math:`p` be an integer and :math:`c` a rational constant. Then +.. thm:: Bound on the ceiling function - :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil` + Let :math:`p` be an integer and :math:`c` a rational constant. Then + :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`. For instance, from 2 x = 1 we can deduce diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 23bc9a2e4a..1f7dd9d689 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -96,11 +96,13 @@ language = None # directories to ignore when looking for source files. # This patterns also effect to html_static_path and html_extra_path exclude_patterns = [ - '_build', - 'Thumbs.db', - '.DS_Store', - 'introduction.rst', - 'credits.rst' + '_build', + 'Thumbs.db', + '.DS_Store', + 'introduction.rst', + 'credits.rst', + 'README.rst', + 'README.template.rst' ] # The reST default role (used for this markup: `text`) to use for all diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index aa41f8058d..4dcd7deb13 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -553,8 +553,8 @@ has type :token:`type`. .. cmd:: Axiom @ident : @term - This command links *term* to the name *ident* as its specification in - the global context. The fact asserted by *term* is thus assumed as a + This command links :token:`term` to the name :token:`ident` as its specification in + the global context. The fact asserted by :token:`term` is thus assumed as a postulate. .. exn:: @ident already exists. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 0318bddde4..3835524f0a 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -653,7 +653,7 @@ be applied or the goal is not head-reducible. This repeats ``intro`` until it meets the head-constant. It never reduces head-constants and it never fails. -.. tac:: intro @ident +.. tacn:: intro @ident This applies ``intro`` but forces :n:`@ident` to be the name of the introduced hypothesis. @@ -904,15 +904,15 @@ quantification or an implication. .. tacn:: revert {+ @ident} :name: revert -This applies to any goal with variables :n:`{+ @ident}`. It moves the hypotheses -(possibly defined) to the goal, if this respects dependencies. This tactic is -the inverse of :tacn:`intro`. + This applies to any goal with variables :n:`{+ @ident}`. It moves the hypotheses + (possibly defined) to the goal, if this respects dependencies. This tactic is + the inverse of :tacn:`intro`. .. exn:: No such hypothesis. .. exn:: @ident is used in the hypothesis @ident. -.. tac:: revert dependent @ident +.. tacn:: revert dependent @ident This moves to the goal the hypothesis :n:`@ident` and all the hypotheses that depend on it. @@ -1122,7 +1122,7 @@ Controlling the proof flow This behaves as :n:`assert (@ident : form)` but :n:`@ident` is generated by Coq. -.. tacv:: assert form by tactic +.. tacv:: assert @form by @tactic This tactic behaves like :n:`assert` but applies tactic to solve the subgoals generated by assert. @@ -1130,7 +1130,7 @@ Controlling the proof flow .. exn:: Proof is not complete. :name: Proof is not complete. (assert) -.. tacv:: assert form as intro_pattern +.. tacv:: assert @form as @intro_pattern If :n:`intro_pattern` is a naming introduction pattern (see :tacn:`intro`), the hypothesis is named after this introduction pattern (in particular, if @@ -1139,7 +1139,7 @@ Controlling the proof flow introduction pattern, the tactic behaves like :n:`assert form` followed by the action done by this introduction pattern. -.. tacv:: assert form as intro_pattern by tactic +.. tacv:: assert @form as @intro_pattern by @tactic This combines the two previous variants of :n:`assert`. @@ -1192,9 +1192,9 @@ Controlling the proof flow This behaves like :n:`enough form` using :n:`intro_pattern` to name or destruct the new hypothesis. -.. tacv:: enough (@ident : form) by tactic -.. tacv:: enough form by tactic -.. tacv:: enough form as intro_pattern by tactic +.. tacv:: enough (@ident : @form) by @tactic +.. tacv:: enough @form by @tactic +.. tacv:: enough @form as @intro_pattern by @tactic This behaves as above but with :n:`tactic` expected to solve the initial goal after the extra assumption :n:`form` is added and possibly destructed. If the @@ -3240,7 +3240,9 @@ the processing of the rewriting rules. The rewriting rule bases are built with the ``Hint Rewrite vernacular`` command. -.. warn:: This tactic may loop if you build non terminating rewriting systems. +.. warning:: + + This tactic may loop if you build non terminating rewriting systems. .. tacv:: autorewrite with {+ @ident} using @tactic @@ -3444,7 +3446,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is Declares each :n:`@ident` as a transparent or opaque constant. - .. cmdv:: Hint Extern @num {? @pattern} => tactic + .. cmdv:: Hint Extern @num {? @pattern} => @tactic :name: Hint Extern This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index 682553c31b..838926d651 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -106,15 +106,15 @@ Automatic declaration of schemes .. opt:: Elimination Schemes -It is possible to deactivate the automatic declaration of the -induction principles when defining a new inductive type with the -``Unset Elimination Schemes`` command. It may be reactivated at any time with -``Set Elimination Schemes``. + It is possible to deactivate the automatic declaration of the + induction principles when defining a new inductive type with the + ``Unset Elimination Schemes`` command. It may be reactivated at any time with + ``Set Elimination Schemes``. .. 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. + This option controls whether types declared with the keywords :cmd:`Variant` and + :cmd:`Record` get an automatic declaration of the induction principles. .. opt:: Case Analysis Schemes @@ -125,8 +125,8 @@ This option controls whether types declared with the keywords :cmd:`Variant` and .. opt:: Decidable Equality Schemes -These flags control the automatic declaration of those Boolean equalities (see -the second variant of ``Scheme``). + These flags control the automatic declaration of those Boolean equalities (see + the second variant of ``Scheme``). .. warning:: |