diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/MIGRATING | 238 | ||||
| -rw-r--r-- | doc/sphinx/README.rst | 386 | ||||
| -rw-r--r-- | doc/sphinx/README.template.rst | 178 | ||||
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 22 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/addendum/miscellaneous-extensions.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/biblio.bib | 1154 | ||||
| -rwxr-xr-x | doc/sphinx/conf.py | 16 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 13 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 15 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 49 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 294 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/proof-schemes.rst | 16 | ||||
| -rw-r--r-- | doc/tools/coqrst/coqdoc/main.py | 5 | ||||
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 357 | ||||
| -rwxr-xr-x | doc/tools/coqrst/regen_readme.py | 58 | ||||
| -rw-r--r-- | doc/tools/coqrst/repl/coqtop.py | 4 |
17 files changed, 1220 insertions, 1592 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..3036fac815 --- /dev/null +++ b/doc/sphinx/README.rst @@ -0,0 +1,386 @@ +============================= + 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. + +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:`…```. + +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)) diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst new file mode 100644 index 0000000000..f90efa9958 --- /dev/null +++ b/doc/sphinx/README.template.rst @@ -0,0 +1,178 @@ +============================= + 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. + +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)) 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/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index 80ea8a1166..b6c35d8fa7 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -11,7 +11,7 @@ Program derivation |Coq| comes with an extension called ``Derive``, which supports program derivation. Typically in the style of Bird and Meertens or derivations of program refinements. To use the Derive extension it must first be -required with ``Require Coq.Derive.Derive``. When the extension is loaded, +required with ``Require Coq.derive.Derive``. When the extension is loaded, it provides the following command: .. cmd:: Derive @ident SuchThat @term As @ident diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index aeb45611e6..3e988709c5 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -3,47 +3,6 @@ @String{lnai = "Lecture Notes in Artificial Intelligence"} @String{SV = "{Sprin-ger-Verlag}"} -@InProceedings{Aud91, - author = {Ph. Audebaud}, - booktitle = {Proceedings of the sixth Conf. on Logic in Computer Science.}, - publisher = {IEEE}, - title = {Partial {Objects} in the {Calculus of Constructions}}, - year = {1991} -} - -@PhDThesis{Aud92, - author = {Ph. Audebaud}, - school = {{Universit\'e} Bordeaux I}, - title = {Extension du Calcul des Constructions par Points fixes}, - year = {1992} -} - -@InProceedings{Audebaud92b, - author = {Ph. Audebaud}, - booktitle = {{Proceedings of the 1992 Workshop on Types for Proofs and Programs}}, - editor = {{B. Nordstr\"om and K. Petersson and G. Plotkin}}, - note = {Also Research Report LIP-ENS-Lyon}, - pages = {21--34}, - title = {{CC+ : an extension of the Calculus of Constructions with fixpoints}}, - year = {1992} -} - -@InProceedings{Augustsson85, - author = {L. Augustsson}, - title = {{Compiling Pattern Matching}}, - booktitle = {Conference Functional Programming and -Computer Architecture}, - year = {1985} -} - -@Article{BaCo85, - author = {J.L. Bates and R.L. Constable}, - journal = {ACM transactions on Programming Languages and Systems}, - title = {Proofs as {Programs}}, - volume = {7}, - year = {1985} -} - @Book{Bar81, author = {H.P. Barendregt}, publisher = {North-Holland}, @@ -51,55 +10,6 @@ Computer Architecture}, year = {1981} } -@TechReport{Bar91, - author = {H. Barendregt}, - institution = {Catholic University Nijmegen}, - note = {In Handbook of Logic in Computer Science, Vol II}, - number = {91-19}, - title = {Lambda {Calculi with Types}}, - year = {1991} -} - -@Article{BeKe92, - author = {G. Bellin and J. Ketonen}, - journal = {Theoretical Computer Science}, - pages = {115--142}, - title = {A decision procedure revisited : Notes on direct logic, linear logic and its implementation}, - volume = {95}, - year = {1992} -} - -@Book{Bee85, - author = {M.J. Beeson}, - publisher = SV, - title = {Foundations of Constructive Mathematics, Metamathematical Studies}, - year = {1985} -} - -@Book{Bis67, - author = {E. Bishop}, - publisher = {McGraw-Hill}, - title = {Foundations of Constructive Analysis}, - year = {1967} -} - -@Book{BoMo79, - author = {R.S. Boyer and J.S. Moore}, - key = {BoMo79}, - publisher = {Academic Press}, - series = {ACM Monograph}, - title = {A computational logic}, - year = {1979} -} - -@MastersThesis{Bou92, - author = {S. Boutin}, - month = sep, - school = {{Universit\'e Paris 7}}, - title = {Certification d'un compilateur {ML en Coq}}, - year = {1992} -} - @InProceedings{Bou97, title = {Using reflection to build efficient and certified decision procedure s}, @@ -112,15 +22,6 @@ s}, year = {1997} } -@PhDThesis{Bou97These, - author = {S. Boutin}, - title = {R\'eflexions sur les quotients}, - school = {Paris 7}, - year = 1997, - type = {th\`ese d'Universit\'e}, - month = apr -} - @Article{Bru72, author = {N.J. de Bruijn}, journal = {Indag. Math.}, @@ -129,121 +30,6 @@ s}, year = {1972} } - -@InCollection{Bru80, - author = {N.J. de Bruijn}, - booktitle = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.}, - editor = {J.P. Seldin and J.R. Hindley}, - publisher = {Academic Press}, - title = {A survey of the project {Automath}}, - year = {1980} -} - -@TechReport{COQ93, - author = {G. Dowek and A. Felty and H. Herbelin and G. Huet and C. Murthy and C. Parent and C. Paulin-Mohring and B. Werner}, - institution = {INRIA}, - month = may, - number = {154}, - title = {{The Coq Proof Assistant User's Guide Version 5.8}}, - year = {1993} -} - -@TechReport{COQ02, - author = {The Coq Development Team}, - institution = {INRIA}, - month = Feb, - number = {255}, - title = {{The Coq Proof Assistant Reference Manual Version 7.2}}, - year = {2002} -} - -@TechReport{CPar93, - author = {C. Parent}, - institution = {Ecole {Normale} {Sup\'erieure} de {Lyon}}, - month = oct, - note = {Also in~\cite{Nijmegen93}}, - number = {93-29}, - title = {Developing certified programs in the system {Coq}- {The} {Program} tactic}, - year = {1993} -} - -@PhDThesis{CPar95, - author = {C. Parent}, - school = {Ecole {Normale} {Sup\'erieure} de {Lyon}}, - title = {{Synth\`ese de preuves de programmes dans le Calcul des Constructions Inductives}}, - year = {1995} -} - -@Book{Caml, - author = {P. Weis and X. Leroy}, - publisher = {InterEditions}, - title = {Le langage Caml}, - year = {1993} -} - -@InProceedings{ChiPotSimp03, - author = {Laurent Chicli and Lo\"{\i}c Pottier and Carlos Simpson}, - title = {Mathematical Quotients and Quotient Types in Coq}, - booktitle = {TYPES}, - crossref = {DBLP:conf/types/2002}, - year = {2002} -} - -@TechReport{CoC89, - author = {Projet Formel}, - institution = {INRIA}, - number = {110}, - title = {{The Calculus of Constructions. Documentation and user's guide, Version 4.10}}, - year = {1989} -} - -@InProceedings{CoHu85a, - author = {Th. Coquand and G. Huet}, - address = {Linz}, - booktitle = {EUROCAL'85}, - publisher = SV, - series = LNCS, - title = {{Constructions : A Higher Order Proof System for Mechanizing Mathematics}}, - volume = {203}, - year = {1985} -} - -@InProceedings{CoHu85b, - author = {Th. Coquand and G. Huet}, - booktitle = {Logic Colloquium'85}, - editor = {The Paris Logic Group}, - publisher = {North-Holland}, - title = {{Concepts Math\'ematiques et Informatiques formalis\'es dans le Calcul des Constructions}}, - year = {1987} -} - -@Article{CoHu86, - author = {Th. Coquand and G. Huet}, - journal = {Information and Computation}, - number = {2/3}, - title = {The {Calculus of Constructions}}, - volume = {76}, - year = {1988} -} - -@InProceedings{CoPa89, - author = {Th. Coquand and C. Paulin-Mohring}, - booktitle = {Proceedings of Colog'88}, - editor = {P. Martin-L\"of and G. Mints}, - publisher = SV, - series = LNCS, - title = {Inductively defined types}, - volume = {417}, - year = {1990} -} - -@Book{Con86, - author = {R.L. {Constable et al.}}, - publisher = {Prentice-Hall}, - title = {{Implementing Mathematics with the Nuprl Proof Development System}}, - year = {1986} -} - @PhDThesis{Coq85, author = {Th. Coquand}, month = jan, @@ -261,24 +47,6 @@ s}, year = {1986} } -@InProceedings{Coq90, - author = {Th. Coquand}, - booktitle = {Logic and Computer Science}, - editor = {P. Oddifredi}, - note = {INRIA Research Report 1088, also in~\cite{CoC89}}, - publisher = {Academic Press}, - title = {{Metamathematical Investigations of a Calculus of Constructions}}, - year = {1990} -} - -@InProceedings{Coq91, - author = {Th. Coquand}, - booktitle = {Proceedings 9th Int. Congress of Logic, Methodology and Philosophy of Science}, - title = {{A New Paradox in Type Theory}}, - month = {August}, - year = {1991} -} - @InProceedings{Coq92, author = {Th. Coquand}, title = {{Pattern Matching with Dependent Types}}, @@ -286,49 +54,18 @@ s}, booktitle = {Proceedings of the 1992 Workshop on Types for Proofs and Programs} } -@InProceedings{Coquand93, - author = {Th. Coquand}, - booktitle = {Types for Proofs and Programs}, - editor = {H. Barendregt and T. Nipokow}, - publisher = SV, - series = LNCS, - title = {{Infinite objects in Type Theory}}, - volume = {806}, - year = {1993}, - pages = {62-78} -} - -@inproceedings{Corbineau08types, - author = {P. Corbineau}, - title = {A Declarative Language for the Coq Proof Assistant}, - editor = {M. Miculan and I. Scagnetto and F. Honsell}, - booktitle = {TYPES '07, Cividale del Friuli, Revised Selected Papers}, - publisher = {Springer}, - series = LNCS, - volume = {4941}, - year = {2007}, - pages = {69-84}, - ee = {http://dx.doi.org/10.1007/978-3-540-68103-8_5}, -} - -@PhDThesis{Cor97, - author = {C. Cornes}, - month = nov, - school = {{Universit\'e Paris 7}}, - title = {Conception d'un langage de haut niveau de représentation de preuves}, - type = {Th\`ese de Doctorat}, - year = {1997} -} - -@MastersThesis{Cou94a, - author = {J. Courant}, - month = sep, - school = {DEA d'Informatique, ENS Lyon}, - title = {Explicitation de preuves par r\'ecurrence implicite}, - year = {1994} +@InProceedings{DBLP:conf/types/CornesT95, + author = {Cristina Cornes and + Delphine Terrasse}, + title = {Automating Inversion of Inductive Predicates in Coq}, + booktitle = {TYPES}, + year = {1995}, + pages = {85-104}, + crossref = {DBLP:conf/types/1995}, + bibsource = {DBLP, http://dblp.uni-trier.de} } -@book{Cur58, +@Book{Cur58, author = {Haskell B. Curry and Robert Feys and William Craig}, title = {Combinatory Logic}, volume = 1, @@ -337,17 +74,40 @@ s}, note = {{\S{9E}}}, } -@InProceedings{Del99, - author = {Delahaye, D.}, - title = {Information Retrieval in a Coq Proof Library using - Type Isomorphisms}, - booktitle = {Proceedings of TYPES '99, L\"okeberg}, - publisher = SV, - series = lncs, - year = {1999}, - url = - "\\{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"# - "{\sf TYPES99-SIsos.ps.gz}" +@Article{CSlessadhoc, + author = {Gonthier, Georges and Ziliani, Beta and Nanevski, Aleksandar and Dreyer, Derek}, + title = {How to Make Ad Hoc Proof Automation Less Ad Hoc}, + journal = {SIGPLAN Not.}, + issue_date = {September 2011}, + volume = {46}, + number = {9}, + month = sep, + year = {2011}, + issn = {0362-1340}, + pages = {163--175}, + numpages = {13}, + url = {http://doi.acm.org/10.1145/2034574.2034798}, + doi = {10.1145/2034574.2034798}, + acmid = {2034798}, + publisher = {ACM}, + address = {New York, NY, USA}, + keywords = {canonical structures, coq, custom proof automation, hoare type theory, interactive theorem proving, tactics, type classes}, +} + +@InProceedings{CSwcu, + hal_id = {hal-00816703}, + url = {http://hal.inria.fr/hal-00816703}, + title = {{Canonical Structures for the working Coq user}}, + author = {Mahboubi, Assia and Tassi, Enrico}, + booktitle = {{ITP 2013, 4th Conference on Interactive Theorem Proving}}, + publisher = {Springer}, + pages = {19-34}, + address = {Rennes, France}, + volume = {7998}, + editor = {Sandrine Blazy and Christine Paulin and David Pichardie }, + series = {LNCS }, + doi = {10.1007/978-3-642-39634-2\_5 }, + year = {2013}, } @InProceedings{Del00, @@ -361,99 +121,7 @@ s}, pages = {85--95}, month = {November}, year = {2000}, - url = - "{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"# - "{\sf LPAR2000-ltac.ps.gz}" -} - -@InProceedings{DelMay01, - author = {Delahaye, D. and Mayero, M.}, - title = {{\tt Field}: une proc\'edure de d\'ecision pour les nombres r\'eels en {\Coq}}, - booktitle = {Journ\'ees Francophones des Langages Applicatifs, Pontarlier}, - publisher = {INRIA}, - month = {Janvier}, - year = {2001}, - url = - "\\{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"# - "{\sf JFLA2000-Field.ps.gz}" -} - -@TechReport{Dow90, - author = {G. Dowek}, - institution = {INRIA}, - number = {1283}, - title = {Naming and Scoping in a Mathematical Vernacular}, - type = {Research Report}, - year = {1990} -} - -@Article{Dow91a, - author = {G. Dowek}, - journal = {Compte-Rendus de l'Acad\'emie des Sciences}, - note = {The undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors}, - number = {12}, - pages = {951--956}, - title = {L'Ind\'ecidabilit\'e du Filtrage du Troisi\`eme Ordre dans les Calculs avec Types D\'ependants ou Constructeurs de Types}, - volume = {I, 312}, - year = {1991} -} - -@InProceedings{Dow91b, - author = {G. Dowek}, - booktitle = {Proceedings of Mathematical Foundation of Computer Science}, - note = {Also INRIA Research Report}, - pages = {151--160}, - publisher = SV, - series = LNCS, - title = {A Second Order Pattern Matching Algorithm in the Cube of Typed $\lambda$-calculi}, - volume = {520}, - year = {1991} -} - -@PhDThesis{Dow91c, - author = {G. Dowek}, - month = dec, - school = {Universit\'e Paris 7}, - title = {D\'emonstration automatique dans le Calcul des Constructions}, - year = {1991} -} - -@Article{Dow92a, - author = {G. Dowek}, - title = {The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable}, - year = 1993, - journal = {Theoretical Computer Science}, - volume = 107, - number = 2, - pages = {349-356} -} - -@Article{Dow94a, - author = {G. Dowek}, - journal = {Annals of Pure and Applied Logic}, - volume = {69}, - pages = {135--155}, - title = {Third order matching is decidable}, - year = {1994} -} - -@InProceedings{Dow94b, - author = {G. Dowek}, - booktitle = {Proceedings of the second international conference on typed lambda calculus and applications}, - title = {Lambda-calculus, Combinators and the Comprehension Schema}, - year = {1995} -} - -@InProceedings{Dyb91, - author = {P. Dybjer}, - booktitle = {Logical Frameworks}, - editor = {G. Huet and G. Plotkin}, - pages = {59--79}, - publisher = {Cambridge University Press}, - title = {Inductive sets and families in {Martin-Löf's} - Type Theory and their set-theoretic semantics: An inversion principle for {Martin-L\"of's} type theory}, - volume = {14}, - year = {1991} + url = {http://www.lirmm.fr/\%7Edelahaye/papers/ltac\%20(LPAR\%2700).pdf} } @Article{Dyc92, @@ -466,75 +134,6 @@ s}, year = {1992} } -@MastersThesis{Fil94, - author = {J.-C. Filli\^atre}, - month = sep, - school = {DEA d'Informatique, ENS Lyon}, - title = {Une proc\'edure de d\'ecision pour le Calcul des Pr\'edicats Direct. Étude et impl\'ementation dans le syst\`eme {\Coq}}, - year = {1994} -} - -@TechReport{Filliatre95, - author = {J.-C. Filli\^atre}, - institution = {LIP-ENS-Lyon}, - title = {A decision procedure for Direct Predicate Calculus}, - type = {Research report}, - number = {96--25}, - year = {1995} -} - -@Article{Filliatre03jfp, - author = {J.-C. Filliâtre}, - title = {Verification of Non-Functional Programs - using Interpretations in Type Theory}, - journal = jfp, - volume = 13, - number = 4, - pages = {709--745}, - month = jul, - year = 2003, - note = {[English translation of \cite{Filliatre99}]}, - url = {http://www.lri.fr/~filliatr/ftp/publis/jphd.ps.gz}, - topics = {team, lri}, - type_publi = {irevcomlec} -} - -@PhDThesis{Filliatre99, - author = {J.-C. Filli\^atre}, - title = {Preuve de programmes imp\'eratifs en th\'eorie des types}, - type = {Thèse de Doctorat}, - school = {Universit\'e Paris-Sud}, - year = 1999, - month = {July}, - url = {\url{http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz}} -} - -@Unpublished{Filliatre99c, - author = {J.-C. Filli\^atre}, - title = {{Formal Proof of a Program: Find}}, - month = {January}, - year = 2000, - note = {Submitted to \emph{Science of Computer Programming}}, - url = {\url{http://www.lri.fr/~filliatr/ftp/publis/find.ps.gz}} -} - -@InProceedings{FilliatreMagaud99, - author = {J.-C. Filli\^atre and N. Magaud}, - title = {Certification of sorting algorithms in the system {\Coq}}, - booktitle = {Theorem Proving in Higher Order Logics: - Emerging Trends}, - year = 1999, - url = {\url{http://www.lri.fr/~filliatr/ftp/publis/Filliatre-Magaud.ps.gz}} -} - -@Unpublished{Fle90, - author = {E. Fleury}, - month = jul, - note = {Rapport de Stage}, - title = {Implantation des algorithmes de {Floyd et de Dijkstra} dans le {Calcul des Constructions}}, - year = {1990} -} - @Book{Fourier, author = {Jean-Baptiste-Joseph Fourier}, publisher = {Gauthier-Villars}, @@ -554,13 +153,6 @@ s}, year = {1994} } -@PhDThesis{Gim96, - author = {E. Gim\'enez}, - title = {Un calcul des constructions infinies et son application \'a la v\'erification de syst\`emes communicants}, - school = {\'Ecole Normale Sup\'erieure de Lyon}, - year = {1996} -} - @TechReport{Gim98, author = {E. Gim\'enez}, title = {A Tutorial on Recursive Types in Coq}, @@ -591,21 +183,6 @@ s}, year = {1995} } -@InProceedings{Gir70, - author = {J.-Y. Girard}, - booktitle = {Proceedings of the 2nd Scandinavian Logic Symposium}, - publisher = {North-Holland}, - title = {Une extension de l'interpr\'etation de {G\"odel} \`a l'analyse, et son application \`a l'\'elimination des coupures dans l'analyse et la th\'eorie des types}, - year = {1970} -} - -@PhDThesis{Gir72, - author = {J.-Y. Girard}, - school = {Universit\'e Paris~7}, - title = {Interpr\'etation fonctionnelle et \'elimination des coupures de l'arithm\'etique d'ordre sup\'erieur}, - year = {1972} -} - @Book{Gir89, author = {J.-Y. Girard and Y. Lafont and P. Taylor}, publisher = {Cambridge University Press}, @@ -614,32 +191,6 @@ s}, year = {1989} } -@TechReport{Har95, - author = {John Harrison}, - title = {Metatheory and Reflection in Theorem Proving: A Survey and Critique}, - institution = {SRI International Cambridge Computer Science Research Centre,}, - year = 1995, - type = {Technical Report}, - number = {CRC-053}, - abstract = {http://www.cl.cam.ac.uk/users/jrh/papers.html} -} - -@MastersThesis{Hir94, - author = {D. Hirschkoff}, - month = sep, - school = {DEA IARFA, Ecole des Ponts et Chauss\'ees, Paris}, - title = {Écriture d'une tactique arithm\'etique pour le syst\`eme {\Coq}}, - year = {1994} -} - -@InProceedings{HofStr98, - author = {Martin Hofmann and Thomas Streicher}, - title = {The groupoid interpretation of type theory}, - booktitle = {Proceedings of the meeting Twenty-five years of constructive type theory}, - publisher = {Oxford University Press}, - year = {1998} -} - @InCollection{How80, author = {W.A. Howard}, booktitle = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.}, @@ -650,27 +201,6 @@ s}, year = {1980} } -@InProceedings{Hue87tapsoft, - author = {G. Huet}, - title = {Programming of Future Generation Computers}, - booktitle = {Proceedings of TAPSOFT87}, - series = LNCS, - volume = 249, - pages = {276--286}, - year = 1987, - publisher = SV -} - -@InProceedings{Hue87, - author = {G. Huet}, - booktitle = {Programming of Future Generation Computers}, - editor = {K. Fuchi and M. Nivat}, - note = {Also in \cite{Hue87tapsoft}}, - publisher = {Elsevier Science}, - title = {Induction Principles Formalized in the {Calculus of Constructions}}, - year = {1988} -} - @InProceedings{Hue88, author = {G. Huet}, booktitle = {A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney}, @@ -680,112 +210,17 @@ s}, year = {1989} } -@Unpublished{Hue88b, - author = {G. Huet}, - title = {Extending the Calculus of Constructions with Type:Type}, - year = 1988, - note = {Unpublished} -} - -@Book{Hue89, - editor = {G. Huet}, - publisher = {Addison-Wesley}, - series = {The UT Year of Programming Series}, - title = {Logical Foundations of Functional Programming}, - year = {1989} -} - -@InProceedings{Hue92, - author = {G. Huet}, - booktitle = {Proceedings of 12th FST/TCS Conference, New Delhi}, - pages = {229--240}, - publisher = SV, - series = LNCS, - title = {The Gallina Specification Language : A case study}, - volume = {652}, - year = {1992} -} - -@Article{Hue94, - author = {G. Huet}, - journal = {J. Functional Programming}, - pages = {371--394}, - publisher = {Cambridge University Press}, - title = {Residual theory in $\lambda$-calculus: a formal development}, - volume = {4,3}, - year = {1994} -} - -@InCollection{HuetLevy79, - author = {G. Huet and J.-J. L\'{e}vy}, - title = {Call by Need Computations in Non-Ambigous -Linear Term Rewriting Systems}, - note = {Also research report 359, INRIA, 1979}, - booktitle = {Computational Logic, Essays in Honor of -Alan Robinson}, - editor = {J.-L. Lassez and G. Plotkin}, - publisher = {The MIT press}, - year = {1991} -} - -@Article{KeWe84, - author = {J. Ketonen and R. Weyhrauch}, - journal = {Theoretical Computer Science}, - pages = {297--307}, - title = {A decidable fragment of {P}redicate {C}alculus}, - volume = {32}, - year = {1984} -} - -@Book{Kle52, - author = {S.C. Kleene}, - publisher = {North-Holland}, - series = {Bibliotheca Mathematica}, - title = {Introduction to Metamathematics}, - year = {1952} -} - -@Book{Kri90, - author = {J.-L. Krivine}, - publisher = {Masson}, - series = {Etudes et recherche en informatique}, - title = {Lambda-calcul {types et mod\`eles}}, - year = {1990} -} - -@Book{LE92, - editor = {G. Huet and G. Plotkin}, - publisher = {Cambridge University Press}, - title = {Logical Environments}, - year = {1992} -} - -@Book{LF91, - editor = {G. Huet and G. Plotkin}, - publisher = {Cambridge University Press}, - title = {Logical Frameworks}, - year = {1991} -} - -@Article{Laville91, - author = {A. Laville}, - title = {Comparison of Priority Rules in Pattern -Matching and Term Rewriting}, - journal = {Journal of Symbolic Computation}, - volume = {11}, - pages = {321--347}, - year = {1991} -} - -@InProceedings{LePa94, - author = {F. Leclerc and C. Paulin-Mohring}, - booktitle = {{Types for Proofs and Programs, Types' 93}}, - editor = {H. Barendregt and T. Nipkow}, - publisher = SV, - series = {LNCS}, - title = {{Programming with Streams in Coq. A case study : The Sieve of Eratosthenes}}, - volume = {806}, - year = {1994} +@Article{LeeWerner11, + author = {Gyesik Lee and + Benjamin Werner}, + title = {Proof-irrelevant model of {CC} with predicative induction + and judgmental equality}, + journal = {Logical Methods in Computer Science}, + volume = {7}, + number = {4}, + year = {2011}, + ee = {http://dx.doi.org/10.2168/LMCS-7(4:5)2011}, + bibsource = {DBLP, http://dblp.uni-trier.de} } @TechReport{Leroy90, @@ -805,14 +240,7 @@ Matching and Term Rewriting}, url = {draft at \url{http://www.irif.fr/~letouzey/download/extraction2002.pdf}} } -@PhDThesis{Luo90, - author = {Z. Luo}, - title = {An Extended Calculus of Constructions}, - school = {University of Edinburgh}, - year = {1990} -} - -@inproceedings{Luttik97specificationof, +@InProceedings{Luttik97specificationof, author = {Sebastiaan P. Luttik and Eelco Visser}, booktitle = {2nd International Workshop on the Theory and Practice of Algebraic Specifications (ASF+SDF'97), Electronic Workshops in Computing}, publisher = {Springer-Verlag}, @@ -820,92 +248,15 @@ Matching and Term Rewriting}, year = {1997} } -@Book{MaL84, - author = {{P. Martin-L\"of}}, - publisher = {Bibliopolis}, - series = {Studies in Proof Theory}, - title = {Intuitionistic Type Theory}, - year = {1984} -} - -@Article{MaSi94, - author = {P. Manoury and M. Simonot}, - title = {Automatizing Termination Proofs of Recursively Defined Functions.}, - journal = {TCS}, - volume = {135}, - number = {2}, - year = {1994}, - pages = {319-343}, -} - -@InProceedings{Miquel00, - author = {A. Miquel}, - title = {A Model for Impredicative Type Systems with Universes, -Intersection Types and Subtyping}, - booktitle = {{Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS'00)}}, - publisher = {IEEE Computer Society Press}, - year = {2000} -} - -@PhDThesis{Miquel01a, - author = {A. Miquel}, - title = {Le Calcul des Constructions implicite: syntaxe et s\'emantique}, - month = {dec}, - school = {{Universit\'e Paris 7}}, - year = {2001} -} - -@InProceedings{Miquel01b, - author = {A. Miquel}, - title = {The Implicit Calculus of Constructions: Extending Pure Type Systems with an Intersection Type Binder and Subtyping}, - booktitle = {{Proceedings of the fifth International Conference on Typed Lambda Calculi and Applications (TLCA01), Krakow, Poland}}, - publisher = SV, - series = {LNCS}, - number = 2044, - year = {2001} -} - -@InProceedings{MiWer02, - author = {A. Miquel and B. Werner}, - title = {The Not So Simple Proof-Irrelevant Model of CC}, - booktitle = {TYPES}, - year = {2002}, - pages = {240-258}, - ee = {http://link.springer.de/link/service/series/0558/bibs/2646/26460240.htm}, - crossref = {DBLP:conf/types/2002}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@proceedings{DBLP:conf/types/2002, - editor = {H. Geuvers and F. Wiedijk}, - title = {Types for Proofs and Programs, Second International Workshop, - TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, - Selected Papers}, - booktitle = {TYPES}, - publisher = SV, - series = LNCS, - volume = {2646}, - year = {2003}, - isbn = {3-540-14031-X}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@InProceedings{Moh89a, - author = {C. Paulin-Mohring}, - address = {Austin}, - booktitle = {Sixteenth Annual ACM Symposium on Principles of Programming Languages}, - month = jan, - publisher = {ACM}, - title = {Extracting ${F}_{\omega}$'s programs from proofs in the {Calculus of Constructions}}, - year = {1989} -} - -@PhDThesis{Moh89b, - author = {C. Paulin-Mohring}, - month = jan, - school = {{Universit\'e Paris 7}}, - title = {Extraction de programmes dans le {Calcul des Constructions}}, - year = {1989} +@InProceedings{DBLP:conf/types/McBride00, + author = {Conor McBride}, + title = {Elimination with a Motive}, + booktitle = {TYPES}, + year = {2000}, + pages = {197-216}, + ee = {http://link.springer.de/link/service/series/0558/bibs/2277/22770197.htm}, + crossref = {DBLP:conf/types/2000}, + bibsource = {DBLP, http://dblp.uni-trier.de} } @InProceedings{Moh93, @@ -920,14 +271,6 @@ Intersection Types and Subtyping}, year = {1993} } -@Book{Moh97, - author = {C. Paulin-Mohring}, - month = jan, - publisher = {{ENS Lyon}}, - title = {{Le syst\`eme Coq. \mbox{Th\`ese d'habilitation}}}, - year = {1997} -} - @MastersThesis{Mun94, author = {C. Muñoz}, month = sep, @@ -936,73 +279,6 @@ Intersection Types and Subtyping}, year = {1994} } -@PhDThesis{Mun97d, - author = {C. Mu{\~{n}}oz}, - title = {Un calcul de substitutions pour la repr\'esentation - de preuves partielles en th\'eorie de types}, - school = {Universit\'e Paris 7}, - year = {1997}, - note = {Version en anglais disponible comme rapport de - recherche INRIA RR-3309}, - type = {Th\`ese de Doctorat} -} - -@Book{NoPS90, - author = {B. {Nordstr\"om} and K. Peterson and J. Smith}, - booktitle = {Information Processing 83}, - publisher = {Oxford Science Publications}, - series = {International Series of Monographs on Computer Science}, - title = {Programming in {Martin-L\"of's} Type Theory}, - year = {1990} -} - -@Article{Nor88, - author = {B. {Nordstr\"om}}, - journal = {BIT}, - title = {Terminating General Recursion}, - volume = {28}, - year = {1988} -} - -@Book{Odi90, - editor = {P. Odifreddi}, - publisher = {Academic Press}, - title = {Logic and Computer Science}, - year = {1990} -} - -@InProceedings{PaMS92, - author = {M. Parigot and P. Manoury and M. Simonot}, - address = {St. Petersburg, Russia}, - booktitle = {Logic Programming and automated reasoning}, - editor = {A. Voronkov}, - month = jul, - number = {624}, - publisher = SV, - series = {LNCS}, - title = {{ProPre : A Programming language with proofs}}, - year = {1992} -} - -@Article{PaWe92, - author = {C. Paulin-Mohring and B. Werner}, - journal = {Journal of Symbolic Computation}, - pages = {607--640}, - title = {{Synthesis of ML programs in the system Coq}}, - volume = {15}, - year = {1993} -} - -@Article{Par92, - author = {M. Parigot}, - journal = {Theoretical Computer Science}, - number = {2}, - pages = {335--356}, - title = {{Recursive Programming with Proofs}}, - volume = {94}, - year = {1992} -} - @InProceedings{Parent95b, author = {C. Parent}, booktitle = {{Mathematics of Program Construction'95}}, @@ -1014,14 +290,16 @@ the Calculus of Inductive Constructions}}, year = {1995} } -@InProceedings{Prasad93, - author = {K.V. Prasad}, - booktitle = {{Proceedings of CONCUR'93}}, - publisher = SV, - series = {LNCS}, - title = {{Programming with broadcasts}}, - volume = {715}, - year = {1993} +@Misc{Pcoq, + author = {Lemme Team}, + title = {Pcoq a graphical user-interface for {Coq}}, + note = {\url{http://www-sop.inria.fr/lemme/pcoq/}} +} + +@Misc{ProofGeneral, + author = {David Aspinall}, + title = {Proof General}, + note = {\url{https://proofgeneral.github.io/}} } @Book{RC95, @@ -1034,15 +312,6 @@ the Calculus of Inductive Constructions}}, note = {ISBN-0-8176-3763-X} } -@TechReport{Rou92, - author = {J. Rouyer}, - institution = {INRIA}, - month = nov, - number = {1795}, - title = {{Développement de l'Algorithme d'Unification dans le Calcul des Constructions}}, - year = {1992} -} - @Article{Rushby98, title = {Subtypes for Specifications: Predicate Subtyping in {PVS}}, @@ -1055,115 +324,7 @@ the Calculus of Inductive Constructions}}, year = 1998 } -@TechReport{Saibi94, - author = {A. Sa\"{\i}bi}, - institution = {INRIA}, - month = dec, - number = {2345}, - title = {{Axiomatization of a lambda-calculus with explicit-substitutions in the Coq System}}, - year = {1994} -} - - -@MastersThesis{Ter92, - author = {D. Terrasse}, - month = sep, - school = {IARFA}, - title = {{Traduction de TYPOL en COQ. Application \`a Mini ML}}, - year = {1992} -} - -@TechReport{ThBeKa92, - author = {L. Th\'ery and Y. Bertot and G. Kahn}, - institution = {INRIA Sophia}, - month = may, - number = {1684}, - title = {Real theorem provers deserve real user-interfaces}, - type = {Research Report}, - year = {1992} -} - -@Book{TrDa89, - author = {A.S. Troelstra and D. van Dalen}, - publisher = {North-Holland}, - series = {Studies in Logic and the foundations of Mathematics, volumes 121 and 123}, - title = {Constructivism in Mathematics, an introduction}, - year = {1988} -} - -@PhDThesis{Wer94, - author = {B. Werner}, - school = {Universit\'e Paris 7}, - title = {Une th\'eorie des constructions inductives}, - type = {Th\`ese de Doctorat}, - year = {1994} -} - -@PhDThesis{Bar99, - author = {B. Barras}, - school = {Universit\'e Paris 7}, - title = {Auto-validation d'un système de preuves avec familles inductives}, - type = {Th\`ese de Doctorat}, - year = {1999} -} - -@Unpublished{ddr98, - author = {D. de Rauglaudre}, - title = {Camlp4 version 1.07.2}, - year = {1998}, - note = {In Camlp4 distribution} -} - -@Article{dowek93, - author = {G. Dowek}, - title = {{A Complete Proof Synthesis Method for the Cube of Type Systems}}, - journal = {Journal Logic Computation}, - volume = {3}, - number = {3}, - pages = {287--315}, - month = {June}, - year = {1993} -} - -@InProceedings{manoury94, - author = {P. Manoury}, - title = {{A User's Friendly Syntax to Define -Recursive Functions as Typed $\lambda-$Terms}}, - booktitle = {{Types for Proofs and Programs, TYPES'94}}, - series = {LNCS}, - volume = {996}, - month = jun, - year = {1994} -} - -@TechReport{maranget94, - author = {L. Maranget}, - institution = {INRIA}, - number = {2385}, - title = {{Two Techniques for Compiling Lazy Pattern Matching}}, - year = {1994} -} - -@InProceedings{puel-suarez90, - author = {L.Puel and A. Su\'arez}, - booktitle = {{Conference Lisp and Functional Programming}}, - series = {ACM}, - publisher = SV, - title = {{Compiling Pattern Matching by Term -Decomposition}}, - year = {1990} -} - -@MastersThesis{saidi94, - author = {H. Saidi}, - month = sep, - school = {DEA d'Informatique Fondamentale, Universit\'e Paris 7}, - title = {R\'esolution d'\'equations dans le syst\`eme T - de G\"odel}, - year = {1994} -} - -@inproceedings{sozeau06, +@InProceedings{sozeau06, author = {Matthieu Sozeau}, title = {Subset Coercions in {C}oq}, year = {2007}, @@ -1174,7 +335,7 @@ Decomposition}}, series = {LNCS} } -@inproceedings{sozeau08, +@InProceedings{sozeau08, Author = {Matthieu Sozeau and Nicolas Oury}, booktitle = {TPHOLs'08}, Pdf = {http://www.lri.fr/~sozeau/research/publications/drafts/classes.pdf}, @@ -1182,87 +343,7 @@ Decomposition}}, Year = {2008}, } -@Misc{streicher93semantical, - author = {T. Streicher}, - title = {Semantical Investigations into Intensional Type Theory}, - note = {Habilitationsschrift, LMU Munchen.}, - year = {1993} -} - -@Misc{Pcoq, - author = {Lemme Team}, - title = {Pcoq a graphical user-interface for {Coq}}, - note = {\url{http://www-sop.inria.fr/lemme/pcoq/}} -} - -@Misc{ProofGeneral, - author = {David Aspinall}, - title = {Proof General}, - note = {\url{https://proofgeneral.github.io/}} -} - -@InCollection{wadler87, - author = {P. Wadler}, - title = {Efficient Compilation of Pattern Matching}, - booktitle = {The Implementation of Functional Programming -Languages}, - editor = {S.L. Peyton Jones}, - publisher = {Prentice-Hall}, - year = {1987} -} - -@inproceedings{DBLP:conf/types/CornesT95, - author = {Cristina Cornes and - Delphine Terrasse}, - title = {Automating Inversion of Inductive Predicates in Coq}, - booktitle = {TYPES}, - year = {1995}, - pages = {85-104}, - crossref = {DBLP:conf/types/1995}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} -@proceedings{DBLP:conf/types/1995, - editor = {Stefano Berardi and - Mario Coppo}, - title = {Types for Proofs and Programs, International Workshop TYPES'95, - Torino, Italy, June 5-8, 1995, Selected Papers}, - booktitle = {TYPES}, - publisher = {Springer}, - series = {Lecture Notes in Computer Science}, - volume = {1158}, - year = {1996}, - isbn = {3-540-61780-9}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@inproceedings{DBLP:conf/types/McBride00, - author = {Conor McBride}, - title = {Elimination with a Motive}, - booktitle = {TYPES}, - year = {2000}, - pages = {197-216}, - ee = {http://link.springer.de/link/service/series/0558/bibs/2277/22770197.htm}, - crossref = {DBLP:conf/types/2000}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@proceedings{DBLP:conf/types/2000, - editor = {Paul Callaghan and - Zhaohui Luo and - James McKinna and - Robert Pollack}, - title = {Types for Proofs and Programs, International Workshop, TYPES - 2000, Durham, UK, December 8-12, 2000, Selected Papers}, - booktitle = {TYPES}, - publisher = {Springer}, - series = {Lecture Notes in Computer Science}, - volume = {2277}, - year = {2002}, - isbn = {3-540-43287-6}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@INPROCEEDINGS{sugar, +@InProceedings{sugar, author = {Alessandro Giovini and Teo Mora and Gianfranco Niesi and Lorenzo Robbiano and Carlo Traverso}, title = {"One sugar cube, please" or Selection strategies in the Buchberger algorithm}, booktitle = { Proceedings of the ISSAC'91, ACM Press}, @@ -1271,38 +352,7 @@ Languages}, publisher = {} } -@article{LeeWerner11, - author = {Gyesik Lee and - Benjamin Werner}, - title = {Proof-irrelevant model of {CC} with predicative induction - and judgmental equality}, - journal = {Logical Methods in Computer Science}, - volume = {7}, - number = {4}, - year = {2011}, - ee = {http://dx.doi.org/10.2168/LMCS-7(4:5)2011}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@Comment{cross-references, must be at end} - -@Book{Bastad92, - editor = {B. Nordstr\"om and K. Petersson and G. Plotkin}, - publisher = {Available by ftp at site ftp.inria.fr}, - title = {Proceedings of the 1992 Workshop on Types for Proofs and Programs}, - year = {1992} -} - -@Book{Nijmegen93, - editor = {H. Barendregt and T. Nipkow}, - publisher = SV, - series = LNCS, - title = {Types for Proofs and Programs}, - volume = {806}, - year = {1994} -} - -@article{TheOmegaPaper, +@Article{TheOmegaPaper, author = "W. Pugh", title = "The Omega test: a fast and practical integer programming algorithm for dependence analysis", journal = "Communication of the ACM", @@ -1310,43 +360,15 @@ Languages}, year = "1992", } -@inproceedings{CSwcu, - hal_id = {hal-00816703}, - url = {http://hal.inria.fr/hal-00816703}, - title = {{Canonical Structures for the working Coq user}}, - author = {Mahboubi, Assia and Tassi, Enrico}, - booktitle = {{ITP 2013, 4th Conference on Interactive Theorem Proving}}, - publisher = {Springer}, - pages = {19-34}, - address = {Rennes, France}, - volume = {7998}, - editor = {Sandrine Blazy and Christine Paulin and David Pichardie }, - series = {LNCS }, - doi = {10.1007/978-3-642-39634-2\_5 }, - year = {2013}, -} - -@article{CSlessadhoc, - author = {Gonthier, Georges and Ziliani, Beta and Nanevski, Aleksandar and Dreyer, Derek}, - title = {How to Make Ad Hoc Proof Automation Less Ad Hoc}, - journal = {SIGPLAN Not.}, - issue_date = {September 2011}, - volume = {46}, - number = {9}, - month = sep, - year = {2011}, - issn = {0362-1340}, - pages = {163--175}, - numpages = {13}, - url = {http://doi.acm.org/10.1145/2034574.2034798}, - doi = {10.1145/2034574.2034798}, - acmid = {2034798}, - publisher = {ACM}, - address = {New York, NY, USA}, - keywords = {canonical structures, coq, custom proof automation, hoare type theory, interactive theorem proving, tactics, type classes}, +@PhDThesis{Wer94, + author = {B. Werner}, + school = {Universit\'e Paris 7}, + title = {Une th\'eorie des constructions inductives}, + type = {Th\`ese de Doctorat}, + year = {1994} } -@inproceedings{CompiledStrongReduction, +@InProceedings{CompiledStrongReduction, author = {Benjamin Gr{\'{e}}goire and Xavier Leroy}, editor = {Mitchell Wand and @@ -1365,7 +387,7 @@ Languages}, bibsource = {dblp computer science bibliography, http://dblp.org} } -@inproceedings{FullReduction, +@InProceedings{FullReduction, author = {Mathieu Boespflug and Maxime D{\'{e}}n{\`{e}}s and Benjamin Gr{\'{e}}goire}, diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 23bc9a2e4a..f65400e88c 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -51,6 +51,10 @@ extensions = [ 'coqrst.coqdomain' ] +# Change this to "info" or "warning" to get notifications about undocumented Coq +# objects (objects with no contents). +report_undocumented_coq_objects = None + # Add any paths that contain templates here, relative to this directory. templates_path = ['_templates'] @@ -96,11 +100,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..76a016ff64 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. @@ -1260,6 +1260,12 @@ Chapter :ref:`Tactics`. The basic assertion command is: The name you provided is already defined. You have then to choose another name. + .. exn:: Nested proofs are not allowed unless you turn option Nested Proofs Allowed on. + + You are asserting a new statement while already being in proof editing mode. + This feature, called nested proofs, is disabled by default. + To activate it, turn option :opt:`Nested Proofs Allowed` on. + The following commands are synonyms of :n:`Theorem @ident {? @binders } : type`: .. cmdv:: Lemma @ident {? @binders } : @type @@ -1339,7 +1345,8 @@ using the keyword :cmd:`Qed`. .. note:: - #. Several statements can be simultaneously asserted. + #. Several statements can be simultaneously asserted provided option + :opt:`Nested Proofs Allowed` was turned on. #. Not only other assertions but any vernacular command can be given while in the process of proving a given assertion. In this case, the diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 83dddab4f5..ad1f0caa60 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -55,15 +55,20 @@ Customization at launch time By resource file ~~~~~~~~~~~~~~~~~~~~~~~ -When |Coq| is launched, with either ``coqtop`` or ``coqc``, the resource file -``$XDG_CONFIG_HOME/coq/coqrc.xxx`` is loaded, where ``$XDG_CONFIG_HOME`` +When |Coq| is launched, with either ``coqtop`` or ``coqc``, the +resource file ``$XDG_CONFIG_HOME/coq/coqrc.xxx``, if it exists, will +be implicitly prepended to any document read by Coq, whether it is an +interactive session or a file to compile. Here, ``$XDG_CONFIG_HOME`` is the configuration directory of the user (by default its home -directory ``/.config`` and ``xxx`` is the version number (e.g. 8.8). If +directory ``~/.config``) and ``xxx`` is the version number (e.g. 8.8). If this file is not found, then the file ``$XDG_CONFIG_HOME/coqrc`` is -searched. You can also specify an arbitrary name for the resource file +searched. If not found, it is the file ``~/.coqrc.xxx`` which is searched, +and, if still not found, the file ``~/.coqrc``. If the latter is also +absent, no resource file is loaded. +You can also specify an arbitrary name for the resource file (see option ``-init-file`` below). -This file may contain, for instance, ``Add LoadPath`` commands to add +The resource file may contain, for instance, ``Add LoadPath`` commands to add directories to the load path of |Coq|. It is possible to skip the loading of the resource file with the option ``-q``. diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 892ddbc165..eba0db3ff5 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -113,6 +113,8 @@ list of assertion commands is given in :ref:`Assertions`. The command Aborts the editing of the proof named :token:`ident` (in case you have nested proofs). + .. seealso:: :opt:`Nested Proofs Allowed` + .. cmdv:: Abort All Aborts all current goals. @@ -542,23 +544,34 @@ Controlling the effect of proof editing commands .. opt:: Hyps Limit @num -This option controls the maximum number of hypotheses displayed in goals -after the application of a tactic. All the hypotheses remain usable -in the proof development. -When unset, it goes back to the default mode which is to print all -available hypotheses. + This option controls the maximum number of hypotheses displayed in goals + after the application of a tactic. All the hypotheses remain usable + in the proof development. + When unset, it goes back to the default mode which is to print all + available hypotheses. .. opt:: Automatic Introduction -This option controls the way binders are handled -in assertion commands such as ``Theorem ident [binders] : form``. When the -option is on, which is the default, binders are automatically put in -the local context of the goal to prove. + This option controls the way binders are handled + in assertion commands such as :n:`Theorem @ident {? @binders} : @term`. When the + option is on, which is the default, binders are automatically put in + the local context of the goal to prove. + + When the option is off, binders are discharged on the statement to be + proved and a tactic such as :tacn:`intro` (see Section :ref:`managingthelocalcontext`) + has to be used to move the assumptions to the local context. + + +.. opt:: Nested Proofs Allowed -When the option is off, binders are discharged on the statement to be -proved and a tactic such as :tacn:`intro` (see Section :ref:`managingthelocalcontext`) -has to be used to move the assumptions to the local context. + When turned on (it is off by default), this option enables support for nested + proofs: a new assertion command can be inserted before the current proof is + finished, in which case Coq will temporarily switch to the proof of this + *nested lemma*. When the proof of the nested lemma is finished (with :cmd:`Qed` + or :cmd:`Defined`), its statement will be made available (as if it had been + proved before starting the previous proof) and Coq will switch back to the + proof of the previous assertion. Controlling memory usage @@ -570,13 +583,13 @@ to force |Coq| to optimize some of its internal data structures. .. cmd:: Optimize Proof -This command forces |Coq| to shrink the data structure used to represent -the ongoing proof. + This command forces |Coq| to shrink the data structure used to represent + the ongoing proof. .. cmd:: Optimize Heap -This command forces the |OCaml| runtime to perform a heap compaction. -This is in general an expensive operation. -See: `OCaml Gc <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_ -There is also an analogous tactic :tacn:`optimize_heap`. + This command forces the |OCaml| runtime to perform a heap compaction. + This is in general an expensive operation. + See: `OCaml Gc <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_ + There is also an analogous tactic :tacn:`optimize_heap`. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 0318bddde4..da4c3f9d74 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 @@ -2398,35 +2398,35 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. .. tacn:: rewrite @term :name: rewrite -This tactic applies to any goal. The type of :n:`@term` must have the form + This tactic applies to any goal. The type of :token:`term` must have the form -``forall (x``:sub:`1` ``:A``:sub:`1` ``) ... (x``:sub:`n` ``:A``:sub:`n` ``). eq term``:sub:`1` ``term``:sub:`2` ``.`` + ``forall (x``:sub:`1` ``:A``:sub:`1` ``) ... (x``:sub:`n` ``:A``:sub:`n` ``). eq term``:sub:`1` ``term``:sub:`2` ``.`` -where :g:`eq` is the Leibniz equality or a registered setoid equality. + where :g:`eq` is the Leibniz equality or a registered setoid equality. -Then :n:`rewrite @term` finds the first subterm matching `term`\ :sub:`1` in the goal, -resulting in instances `term`:sub:`1`' and `term`:sub:`2`' and then -replaces every occurrence of `term`:subscript:`1`' by `term`:subscript:`2`'. -Hence, some of the variables :g:`x`\ :sub:`i` are solved by unification, -and some of the types :g:`A`\ :sub:`1`:g:`, ..., A`\ :sub:`n` become new -subgoals. + Then :n:`rewrite @term` finds the first subterm matching `term`\ :sub:`1` in the goal, + resulting in instances `term`:sub:`1`' and `term`:sub:`2`' and then + replaces every occurrence of `term`:subscript:`1`' by `term`:subscript:`2`'. + Hence, some of the variables :g:`x`\ :sub:`i` are solved by unification, + and some of the types :g:`A`\ :sub:`1`:g:`, ..., A`\ :sub:`n` become new + subgoals. -.. exn:: The @term provided does not end with an equation. + .. exn:: The @term provided does not end with an equation. -.. exn:: Tactic generated a subgoal identical to the original goal. This happens if @term does not occur in the goal. + .. exn:: Tactic generated a subgoal identical to the original goal. This happens if @term does not occur in the goal. -.. tacv:: rewrite -> @term + .. tacv:: rewrite -> @term - Is equivalent to :n:`rewrite @term` + Is equivalent to :n:`rewrite @term` -.. tacv:: rewrite <- @term + .. tacv:: rewrite <- @term - Uses the equality :n:`@term`:sub:`1` :n:`= @term` :sub:`2` from right to left + Uses the equality :n:`@term`:sub:`1` :n:`= @term` :sub:`2` from right to left -.. tacv:: rewrite @term in clause + .. tacv:: rewrite @term in clause - Analogous to :n:`rewrite @term` but rewriting is done following clause - (similarly to :ref:`performing computations <performingcomputations>`). For instance: + Analogous to :n:`rewrite @term` but rewriting is done following clause + (similarly to :ref:`performing computations <performingcomputations>`). For instance: + :n:`rewrite H in H`:sub:`1` will rewrite `H` in the hypothesis `H`:sub:`1` instead of the current goal. @@ -2440,136 +2440,128 @@ subgoals. + :n:`rewrite H in *` is a combination of :n:`rewrite H` and :n:`rewrite H in * |-` that succeeds if at least one of these two tactics succeeds. - Orientation :g:`->` or :g:`<-` can be inserted before the :n:`@term` to rewrite. + Orientation :g:`->` or :g:`<-` can be inserted before the :token:`term` to rewrite. -.. tacv:: rewrite @term at occurrences + .. tacv:: rewrite @term at occurrences - Rewrite only the given occurrences of :n:`@term`. Occurrences are - specified from left to right as for pattern (:tacn:`pattern`). The rewrite is - always performed using setoid rewriting, even for Leibniz’s equality, so one - has to ``Import Setoid`` to use this variant. + Rewrite only the given occurrences of :token:`term`. Occurrences are + specified from left to right as for pattern (:tacn:`pattern`). The rewrite is + always performed using setoid rewriting, even for Leibniz’s equality, so one + has to ``Import Setoid`` to use this variant. -.. tacv:: rewrite @term by tactic + .. tacv:: rewrite @term by tactic - Use tactic to completely solve the side-conditions arising from the - :tacn:`rewrite`. + Use tactic to completely solve the side-conditions arising from the + :tacn:`rewrite`. -.. tacv:: rewrite {+ @term} + .. tacv:: rewrite {+, @term} - Is equivalent to the `n` successive tactics :n:`{+ rewrite @term}`, each one - working on the first subgoal generated by the previous one. Orientation - :g:`->` or :g:`<-` can be inserted before each :n:`@term` to rewrite. One - unique clause can be added at the end after the keyword in; it will then - affect all rewrite operations. + Is equivalent to the `n` successive tactics :n:`{+; rewrite @term}`, each one + working on the first subgoal generated by the previous one. Orientation + :g:`->` or :g:`<-` can be inserted before each :token:`term` to rewrite. One + unique clause can be added at the end after the keyword in; it will then + affect all rewrite operations. - In all forms of rewrite described above, a :n:`@term` to rewrite can be - immediately prefixed by one of the following modifiers: + In all forms of rewrite described above, a :token:`term` to rewrite can be + immediately prefixed by one of the following modifiers: - + `?` : the tactic rewrite :n:`?@term` performs the rewrite of :n:`@term` as many - times as possible (perhaps zero time). This form never fails. - + `n?` : works similarly, except that it will do at most `n` rewrites. - + `!` : works as ?, except that at least one rewrite should succeed, otherwise - the tactic fails. - + `n!` (or simply `n`) : precisely `n` rewrites of :n:`@term` will be done, - leading to failure if these n rewrites are not possible. + + `?` : the tactic :n:`rewrite ?@term` performs the rewrite of :token:`term` as many + times as possible (perhaps zero time). This form never fails. + + :n:`@num?` : works similarly, except that it will do at most :token:`num` rewrites. + + `!` : works as `?`, except that at least one rewrite should succeed, otherwise + the tactic fails. + + :n:`@num!` (or simply :n:`@num`) : precisely :token:`num` rewrites of :token:`term` will be done, + leading to failure if these :token:`num` rewrites are not possible. -.. tacv:: erewrite @term - :name: erewrite + .. tacv:: erewrite @term + :name: erewrite - This tactic works as :n:`rewrite @term` but turning - unresolved bindings into existential variables, if any, instead of - failing. It has the same variants as :tacn:`rewrite` has. + This tactic works as :n:`rewrite @term` but turning + unresolved bindings into existential variables, if any, instead of + failing. It has the same variants as :tacn:`rewrite` has. -.. tacn:: replace @term with @term +.. tacn:: replace @term with @term’ :name: replace This tactic applies to any goal. It replaces all free occurrences of :n:`@term` - in the current goal with :n:`@term` and generates the equality :n:`@term = - @term` as a subgoal. This equality is automatically solved if it occurs among - the assumption, or if its symmetric form occurs. It is equivalent to - :n:`cut @term = @term; [intro H`:sub:`n` :n:`; rewrite <- H`:sub:`n` :n:`; clear H`:sub:`n`:n:`|| assumption || symmetry; try assumption]`. + in the current goal with :n:`@term’` and generates an equality :n:`@term = @term’` + as a subgoal. This equality is automatically solved if it occurs among + the assumptions, or if its symmetric form occurs. It is equivalent to + :n:`cut @term = @term’; [intro H`:sub:`n` :n:`; rewrite <- H`:sub:`n` :n:`; clear H`:sub:`n`:n:`|| assumption || symmetry; try assumption]`. -.. exn:: @terms do not have convertible types. + .. exn:: Terms do not have convertible types. -.. tacv:: replace @term with @term by tactic + .. tacv:: replace @term with @term’ by @tactic - This acts as :n:`replace @term` with :n:`@term` but applies tactic to solve the generated - subgoal :n:`@term = @term`. + This acts as :n:`replace @term with @term’` but applies :token:`tactic` to solve the generated + subgoal :n:`@term = @term’`. -.. tacv:: replace @term + .. tacv:: replace @term - Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has - the form :n:`@term = @term’` or :n:`@term’ = @term`. + Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has + the form :n:`@term = @term’` or :n:`@term’ = @term`. -.. tacv:: replace -> @term + .. tacv:: replace -> @term - Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has - the form :n:`@term = @term’` + Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has + the form :n:`@term = @term’` -.. tacv:: replace <- @term + .. tacv:: replace <- @term - Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has - the form :n:`@term’ = @term` + Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has + the form :n:`@term’ = @term` -.. tacv:: replace @term with @term in clause -.. tacv:: replace @term with @term in clause by tactic -.. tacv:: replace @term in clause replace -> @term in clause -.. tacv:: replace <- @term in clause + .. tacv:: replace @term {? with @term} in clause {? by @tactic} + .. tacv:: replace -> @term in clause + .. tacv:: replace <- @term in clause - Acts as before but the replacements take place inclause (see - :ref:`performingcomputations`) and not only in the conclusion of the goal. The - clause argument must not contain any type of nor value of. + Acts as before but the replacements take place in the specified clause (see + :ref:`performingcomputations`) and not only in the conclusion of the goal. The + clause argument must not contain any ``type of`` nor ``value of``. -.. tacv:: cutrewrite <- (@term = @term) - :cutrewrite: + .. tacv:: cutrewrite <- (@term = @term’) + :name: cutrewrite - This tactic is deprecated. It acts like :n:`replace @term with @term`, or, - equivalently as :n:`enough (@term = @term) as <-`. + This tactic is deprecated. It can be replaced by :n:`enough (@term = @term’) as <-`. -.. tacv:: cutrewrite -> (@term = @term) + .. tacv:: cutrewrite -> (@term = @term’) - This tactic is deprecated. It can be replaced by enough :n:`(@term = @term) as ->`. + This tactic is deprecated. It can be replaced by :n:`enough (@term = @term’) as ->`. .. tacn:: subst @ident :name: subst + This tactic applies to a goal that has :n:`@ident` in its context and (at + least) one hypothesis, say :g:`H`, of type :n:`@ident = t` or :n:`t = @ident` + with :n:`@ident` not occurring in :g:`t`. Then it replaces :n:`@ident` by + :g:`t` everywhere in the goal (in the hypotheses and in the conclusion) and + clears :n:`@ident` and :g:`H` from the context. -This tactic applies to a goal that has :n:`@ident` in its context and (at -least) one hypothesis, say :g:`H`, of type :n:`@ident = t` or :n:`t = @ident` -with :n:`@ident` not occurring in :g:`t`. Then it replaces :n:`@ident` by -:g:`t` everywhere in the goal (in the hypotheses and in the conclusion) and -clears :n:`@ident` and :g:`H` from the context. - -If :n:`@ident` is a local definition of the form :n:`@ident := t`, it is also -unfolded and cleared. - - -.. note:: - When several hypotheses have the form :n:`@ident = t` or :n:`t = @ident`, the - first one is used. - - -.. note:: - If `H` is itself dependent in the goal, it is replaced by the proof of - reflexivity of equality. + If :n:`@ident` is a local definition of the form :n:`@ident := t`, it is also + unfolded and cleared. + .. note:: + + When several hypotheses have the form :n:`@ident = t` or :n:`t = @ident`, the + first one is used. -.. tacv:: subst {+ @ident} + + If :g:`H` is itself dependent in the goal, it is replaced by the proof of + reflexivity of equality. - This is equivalent to :n:`subst @ident`:sub:`1`:n:`; ...; subst @ident`:sub:`n`. + .. tacv:: subst {+ @ident} -.. tacv:: subst + This is equivalent to :n:`subst @ident`:sub:`1`:n:`; ...; subst @ident`:sub:`n`. - This applies subst repeatedly from top to bottom to all identifiers of the - context for which an equality of the form :n:`@ident = t` or :n:`t = @ident` - or :n:`@ident := t` exists, with :n:`@ident` not occurring in `t`. + .. tacv:: subst + This applies subst repeatedly from top to bottom to all identifiers of the + context for which an equality of the form :n:`@ident = t` or :n:`t = @ident` + or :n:`@ident := t` exists, with :n:`@ident` not occurring in ``t``. .. opt:: Regular Subst Tactic This option controls the behavior of :tacn:`subst`. When it is - activated, :tacn:`subst` also deals with the following corner cases: + activated (it is by default), :tacn:`subst` also deals with the following corner cases: + A context with ordered hypotheses :n:`@ident`:sub:`1` :n:`= @ident`:sub:`2` and :n:`@ident`:sub:`1` :n:`= t`, or :n:`t′ = @ident`:sub:`1`` with `t′` not @@ -2587,41 +2579,40 @@ unfolded and cleared. unfolded which otherwise it would exceptionally unfold in configurations containing hypotheses of the form :n:`@ident = u`, or :n:`u′ = @ident` with `u′` not a variable. Finally, it preserves the initial order of - hypotheses, which without the option it may break. The option is on by + hypotheses, which without the option it may break. default. .. tacn:: stepl @term :name: stepl + This tactic is for chaining rewriting steps. It assumes a goal of the + form :n:`R @term @term` where ``R`` is a binary relation and relies on a + database of lemmas of the form :g:`forall x y z, R x y -> eq x z -> R z y` + where `eq` is typically a setoid equality. The application of :n:`stepl @term` + then replaces the goal by :n:`R @term @term` and adds a new goal stating + :n:`eq @term @term`. -This tactic is for chaining rewriting steps. It assumes a goal of the -form :n:`R @term @term` where `R` is a binary relation and relies on a -database of lemmas of the form :g:`forall x y z, R x y -> eq x z -> R z y` -where `eq` is typically a setoid equality. The application of :n:`stepl @term` -then replaces the goal by :n:`R @term @term` and adds a new goal stating -:n:`eq @term @term`. - -.. cmd:: Declare Left Step @term + .. cmd:: Declare Left Step @term - Adds :n:`@term` to the database used by :tacn:`stepl`. + Adds :n:`@term` to the database used by :tacn:`stepl`. -The tactic is especially useful for parametric setoids which are not accepted -as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see -:ref:`Generalizedrewriting`). + The tactic is especially useful for parametric setoids which are not accepted + as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see + :ref:`Generalizedrewriting`). -.. tacv:: stepl @term by tactic + .. tacv:: stepl @term by @tactic - This applies :n:`stepl @term` then applies tactic to the second goal. + This applies :n:`stepl @term` then applies :token:`tactic` to the second goal. -.. tacv:: stepr @term stepr @term by tactic - :name: stepr + .. tacv:: stepr @term stepr @term by tactic + :name: stepr - This behaves as :tacn:`stepl` but on the right-hand-side of the binary - relation. Lemmas are expected to be of the form :g:`forall x y z, R x y -> eq - y z -> R x z`. + This behaves as :tacn:`stepl` but on the right-hand-side of the binary + relation. Lemmas are expected to be of the form + :g:`forall x y z, R x y -> eq y z -> R x z`. - .. cmd:: Declare Right Step @term + .. cmd:: Declare Right Step @term Adds :n:`@term` to the database used by :tacn:`stepr`. @@ -2634,28 +2625,25 @@ as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see with `U` providing that `U` is well-formed and that `T` and `U` are convertible. -.. exn:: Not convertible. + .. exn:: Not convertible. + .. tacv:: change @term with @term’ -.. tacv:: change @term with @term + This replaces the occurrences of :n:`@term` by :n:`@term’` in the current goal. + The term :n:`@term` and :n:`@term’` must be convertible. - This replaces the occurrences of :n:`@term` by :n:`@term` in the current goal. - The term :n:`@term` and :n:`@term` must be convertible. + .. tacv:: change @term at {+ @num} with @term’ -.. tacv:: change @term at {+ @num} with @term + This replaces the occurrences numbered :n:`{+ @num}` of :n:`@term` by :n:`@term’` + in the current goal. The terms :n:`@term` and :n:`@term’` must be convertible. - This replaces the occurrences numbered :n:`{+ @num}` of :n:`@term by @term` - in the current goal. The terms :n:`@term` and :n:`@term` must be convertible. + .. exn:: Too few occurrences. -.. exn:: Too few occurrences. + .. tacv:: change @term {? {? at {+ @num}} with @term} in @ident -.. tacv:: change @term in @ident -.. tacv:: change @term with @term in @ident -.. tacv:: change @term at {+ @num} with @term in @ident + This applies the :tacn:`change` tactic not to the goal but to the hypothesis :n:`@ident`. - This applies the change tactic not to the goal but to the hypothesis :n:`@ident`. - -See also: :ref:`Performing computations <performingcomputations>` + .. seealso:: :ref:`Performing computations <performingcomputations>` .. _performingcomputations: @@ -3240,7 +3228,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 @@ -3432,7 +3422,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is Adds each :n:`Hint Unfold @ident`. .. cmdv:: Hint %( Transparent %| Opaque %) @qualid - :name: Hint %( Transparent %| Opaque %) + :name: Hint ( Transparent | Opaque ) This adds a transparency hint to the database, making :n:`@qualid` a transparent or opaque constant during resolution. This information is used @@ -3444,7 +3434,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:: diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py index d464f75bb2..cedd60d3bc 100644 --- a/doc/tools/coqrst/coqdoc/main.py +++ b/doc/tools/coqrst/coqdoc/main.py @@ -32,14 +32,15 @@ COQDOC_OPTIONS = ['--body-only', '--no-glob', '--no-index', '--no-externals', COQDOC_SYMBOLS = ["->", "<-", "<->", "=>", "<=", ">=", "<>", "~", "/\\", "\\/", "|-", "*", "forall", "exists"] COQDOC_HEADER = "".join("(** remove printing {} *)".format(s) for s in COQDOC_SYMBOLS) -def coqdoc(coq_code, coqdoc_bin = os.path.join(os.getenv("COQBIN"),"coqdoc")): +def coqdoc(coq_code, coqdoc_bin=None): """Get the output of coqdoc on coq_code.""" + coqdoc_bin = coqdoc_bin or os.path.join(os.getenv("COQBIN"), "coqdoc") fd, filename = mkstemp(prefix="coqdoc-", suffix=".v") try: os.write(fd, COQDOC_HEADER.encode("utf-8")) os.write(fd, coq_code.encode("utf-8")) os.close(fd) - return check_output([coqdoc_bin] + COQDOC_OPTIONS + [filename], timeout = 2).decode("utf-8") + return check_output([coqdoc_bin] + COQDOC_OPTIONS + [filename], timeout = 10).decode("utf-8") finally: os.remove(filename) diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 21093bd904..8d6e23764f 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -1,3 +1,4 @@ +# -*- coding: utf-8 -*- ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## ## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## @@ -57,30 +58,37 @@ def make_target(objtype, targetid): return "coq:{}.{}".format(objtype, targetid) class CoqObject(ObjectDescription): - """A generic Coq object; all Coq objects are subclasses of this. + """A generic Coq object for Sphinx; all Coq objects are subclasses of this. The fields and methods to override are listed at the top of this class' implementation. Each object supports the :name: option, which gives an explicit name to link to. - See the documentation of CoqDomain for high-level information. + See the comments and docstrings in CoqObject for more information. """ - # The semantic domain in which this object lives. + # The semantic domain in which this object lives (eg. “tac”, “cmd”, “chm”…). # It matches exactly one of the roles used for cross-referencing. - subdomain = None + subdomain = None # type: str - # The suffix to use in indices for objects of this type - index_suffix = None + # The suffix to use in indices for objects of this type (eg. “(tac)”) + index_suffix = None # type: str # The annotation to add to headers of objects of this type - annotation = None + # (eg. “Command”, “Theorem”) + annotation = None # type: str def _name_from_signature(self, signature): # pylint: disable=no-self-use, unused-argument """Convert a signature into a name to link to. + ‘Signature’ is Sphinx parlance for an object's header (think “type + signature”); for example, the signature of the simplest form of the + ``exact`` tactic is ``exact @id``. + Returns None by default, in which case no name will be automatically - generated. + generated. This is a convenient way to automatically generate names + (link targets) without having to write explicit names everywhere. + """ return None @@ -89,8 +97,10 @@ class CoqObject(ObjectDescription): raise NotImplementedError(self) option_spec = { - # One can give an explicit name to each documented object - 'name': directives.unchanged + # Explicit object naming + 'name': directives.unchanged, + # Silence warnings produced by report_undocumented_coq_objects + 'undocumented': directives.flag } def _subdomain(self): @@ -100,7 +110,7 @@ class CoqObject(ObjectDescription): def handle_signature(self, signature, signode): """Prefix signature with the proper annotation, then render it using - _render_signature. + ``_render_signature`` (for example, add “Command” in front of commands). :returns: the name given to the resulting node, if any """ @@ -110,11 +120,6 @@ class CoqObject(ObjectDescription): self._render_signature(signature, signode) return self.options.get("name") or self._name_from_signature(signature) - @property - def _index_suffix(self): - if self.index_suffix: - return " " + self.index_suffix - def _record_name(self, name, target_id): """Record a name, mapping it to target_id @@ -141,12 +146,14 @@ class CoqObject(ObjectDescription): return targetid def _add_index_entry(self, name, target): - """Add name (with target) to the main index.""" - index_text = name + self._index_suffix + """Add `name` (pointing to `target`) to the main index.""" + index_text = name + if self.index_suffix: + index_text += " " + self.index_suffix self.indexnode['entries'].append(('single', index_text, target, '', None)) def add_target_and_index(self, name, _, signode): - """Create a target and an index entry for name""" + """Attach a link target to `signode` and an index entry for `name`.""" if name: target = self._add_target(signode, name) # remove trailing . , found in commands, but not ... (ellipsis) @@ -155,32 +162,63 @@ class CoqObject(ObjectDescription): self._add_index_entry(name, target) return target + def _warn_if_undocumented(self): + document = self.state.document + config = document.settings.env.config + report = config.report_undocumented_coq_objects + if report and not self.content and "undocumented" not in self.options: + # This is annoyingly convoluted, but we don't want to raise warnings + # or interrupt the generation of the current node. For more details + # see https://github.com/sphinx-doc/sphinx/issues/4976. + msg = 'No contents in directive {}'.format(self.name) + node = document.reporter.info(msg, line=self.lineno) + getLogger(__name__).info(node.astext()) + if report == "warning": + raise self.warning(msg) + + def run(self): + self._warn_if_undocumented() + return super().run() + class PlainObject(CoqObject): - """A base class for objects whose signatures should be rendered literaly.""" + """A base class for objects whose signatures should be rendered literally.""" def _render_signature(self, signature, signode): signode += addnodes.desc_name(signature, signature) class NotationObject(CoqObject): - """A base class for objects whose signatures should be rendered as nested boxes.""" + """A base class for objects whose signatures should be rendered as nested boxes. + + Objects that inherit from this class can use the notation grammar (“{+ …}”, + “@…”, etc.) in their signature. + """ def _render_signature(self, signature, signode): position = self.state_machine.get_source_and_line(self.lineno) tacn_node = parse_notation(signature, *position) signode += addnodes.desc_name(signature, '', tacn_node) -class TacticObject(PlainObject): - """An object to represent Coq tactics""" - subdomain = "tac" - index_suffix = "(tac)" - annotation = None - class GallinaObject(PlainObject): - """An object to represent Coq theorems""" + r"""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`. + """ subdomain = "thm" index_suffix = "(thm)" annotation = "Theorem" class VernacObject(NotationObject): - """An object to represent Coq commands""" + """A Coq command. + + Example:: + + .. cmd:: Infix "@symbol" := @term ({+, @modifier}). + + This command is equivalent to :n:`…`. + """ subdomain = "cmd" index_suffix = "(cmd)" annotation = "Command" @@ -191,7 +229,20 @@ class VernacObject(NotationObject): return m.group(0).strip() class VernacVariantObject(VernacObject): - """An object to represent variants of Coq commands""" + """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`. + """ index_suffix = "(cmdv)" annotation = "Variant" @@ -199,18 +250,49 @@ class VernacVariantObject(VernacObject): return None class TacticNotationObject(NotationObject): - """An object to represent Coq tactic notations""" + """A tactic, or a tactic notation. + + Example:: + + .. tacn:: do @num @expr + + :token:`expr` is evaluated to ``v`` which must be a tactic value. … + """ subdomain = "tacn" index_suffix = "(tacn)" annotation = None class TacticNotationVariantObject(TacticNotationObject): - """An object to represent variants of Coq tactic notations""" + """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. … + """ index_suffix = "(tacnv)" annotation = "Variant" class OptionObject(NotationObject): - """An object to represent Coq options""" + """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. + """ subdomain = "opt" index_suffix = "(opt)" annotation = "Option" @@ -219,7 +301,13 @@ class OptionObject(NotationObject): return stringify_with_ellipses(signature) class ProductionObject(NotationObject): - """An object to represent grammar productions""" + """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>`_. + """ + # FIXME (CPC): I have no idea what this does :/ Someone should add an example. subdomain = "prodn" index_suffix = None annotation = None @@ -258,7 +346,22 @@ class ProductionObject(NotationObject): return [idx, node] class ExceptionObject(NotationObject): - """An object to represent Coq errors.""" + """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. + """ subdomain = "exn" index_suffix = "(err)" annotation = "Error" @@ -269,7 +372,19 @@ class ExceptionObject(NotationObject): return stringify_with_ellipses(signature) class WarningObject(NotationObject): - """An object to represent Coq warnings.""" + """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. + """ subdomain = "warn" index_suffix = "(warn)" annotation = "Warning" @@ -280,14 +395,33 @@ class WarningObject(NotationObject): def NotationRole(role, rawtext, text, lineno, inliner, options={}, content=[]): #pylint: disable=unused-argument, dangerous-default-value - """And inline role for notations""" + """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:`@…```. + """ notation = utils.unescape(text, 1) position = inliner.reporter.get_source_and_line(lineno) return [nodes.literal(rawtext, '', parse_notation(notation, *position, rawtext=rawtext))], [] def coq_code_role(role, rawtext, text, lineno, inliner, options={}, content=[]): #pylint: disable=dangerous-default-value - """And inline role for Coq source code""" + """Coq code. + + Use this for Gallina and Ltac snippets:: + + :g:`apply plus_comm; reflexivity` + :g:`Set Printing All.` + :g:`forall (x: t), P(x)` + """ options['language'] = 'Coq' return code_role(role, rawtext, text, lineno, inliner, options, content) ## Too heavy: @@ -300,15 +434,14 @@ def coq_code_role(role, rawtext, text, lineno, inliner, options={}, content=[]): # node = nodes.literal(rawtext, '', *highlight_using_coqdoc(code), classes=classes) # return [node], [] -# TODO pass different languages? -LtacRole = GallinaRole = VernacRole = coq_code_role +CoqCodeRole = coq_code_role class CoqtopDirective(Directive): """A reST directive to describe interactions with Coqtop. Usage:: - .. coqtop:: (options)+ + .. coqtop:: options… Coq code to send to coqtop @@ -321,20 +454,28 @@ class CoqtopDirective(Directive): Here is a list of permissible options: - Display - - ‘all’: Display input and output - - ‘in’: Display only input - - ‘out’: Display only output - - ‘none’: Display neither (useful for setup commands) - Behaviour - - ‘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 + - 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. """ has_content = True required_arguments = 0 optional_arguments = 1 final_argument_whitespace = True + directive_name = "coqtop" def run(self): # Uses a ‘container’ instead of a ‘literal_block’ to disable @@ -349,12 +490,26 @@ class CoqtopDirective(Directive): return [node] class CoqdocDirective(Directive): - """A reST directive to display Coqtop-formatted source code""" + """A reST directive to display Coqtop-formatted source code. + + Usage:: + + .. coqdoc:: + + Coq code to highlight + + Example:: + + .. coqdoc:: + + Definition test := 1. + """ # TODO implement this as a Pygments highlighter? has_content = True required_arguments = 0 optional_arguments = 0 final_argument_whitespace = True + directive_name = "coqdoc" def run(self): # Uses a ‘container’ instead of a ‘literal_block’ to disable @@ -365,8 +520,24 @@ class CoqdocDirective(Directive): return [wrapper] class ExampleDirective(BaseAdmonition): - """A reST directive for examples""" + """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. + """ node_class = nodes.admonition + directive_name = "example" def run(self): # ‘BaseAdmonition’ checks whether ‘node_class’ is ‘nodes.admonition’, @@ -380,8 +551,17 @@ class ExampleDirective(BaseAdmonition): class PreambleDirective(MathDirective): r"""A reST directive for hidden math. - Mostly useful to let MathJax know about `\def`s and `\newcommand`s + Mostly useful to let MathJax know about `\def`\ s and `\newcommand`\ s. + + Example:: + + .. preamble:: + + \newcommand{\paren}[#1]{\left(#1\right)} """ + + directive_name = "preamble" + def run(self): self.options['nowrap'] = True [node] = super().run() @@ -389,14 +569,17 @@ class PreambleDirective(MathDirective): return [node] class InferenceDirective(Directive): - r"""A small example of what directives let you do in Sphinx. + r"""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 - \n-separated premisses - ---------------------- + newline-separated premisses + ------------------------ conclusion Example:: @@ -413,6 +596,7 @@ class InferenceDirective(Directive): optional_arguments = 0 has_content = True final_argument_whitespace = True + directive_name = "inference" def make_math_node(self, latex): node = displaymath() @@ -613,7 +797,7 @@ class CoqSubdomainsIndex(Index): Just as in the original manual, we want to have separate indices for each Coq subdomain (tactics, commands, options, etc)""" - name, localname, shortname, subdomains = None, None, None, None # Must be overwritten + name, localname, shortname, subdomains = None, None, None, [] # Must be overwritten def generate(self, docnames=None): content = defaultdict(list) @@ -635,7 +819,7 @@ class CoqVernacIndex(CoqSubdomainsIndex): name, localname, shortname, subdomains = "cmdindex", "Command Index", "commands", ["cmd"] class CoqTacticIndex(CoqSubdomainsIndex): - name, localname, shortname, subdomains = "tacindex", "Tactic Index", "tactics", ["tac", "tacn"] + name, localname, shortname, subdomains = "tacindex", "Tactic Index", "tactics", ["tacn"] class CoqOptionIndex(CoqSubdomainsIndex): name, localname, shortname, subdomains = "optindex", "Option Index", "options", ["opt"] @@ -665,10 +849,18 @@ class IndexXRefRole(XRefRole): return title, target def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, content=[]): - """An inline role to declare grammar productions that are not in fact 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 + 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:`…```. """ #pylint: disable=dangerous-default-value, unused-argument env = inliner.document.settings.env @@ -681,6 +873,8 @@ def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, conte env.domaindata['std']['objects']['token', text] = env.docname, targetid return [node], [] +GrammarProductionRole.role_name = "production" + class CoqDomain(Domain): """A domain to document Coq code. @@ -703,7 +897,6 @@ class CoqDomain(Domain): # ObjType (= directive type) → (Local name, *xref-roles) 'cmd': ObjType('cmd', 'cmd'), 'cmdv': ObjType('cmdv', 'cmd'), - 'tac': ObjType('tac', 'tac'), 'tacn': ObjType('tacn', 'tacn'), 'tacv': ObjType('tacv', 'tacn'), 'opt': ObjType('opt', 'opt'), @@ -720,7 +913,6 @@ class CoqDomain(Domain): # the same role. 'cmd': VernacObject, 'cmdv': VernacVariantObject, - 'tac': TacticObject, 'tacn': TacticNotationObject, 'tacv': TacticNotationVariantObject, 'opt': OptionObject, @@ -733,7 +925,6 @@ class CoqDomain(Domain): roles = { # Each of these roles lives in a different semantic “subdomain” 'cmd': XRefRole(warn_dangling=True), - 'tac': XRefRole(warn_dangling=True), 'tacn': XRefRole(warn_dangling=True), 'opt': XRefRole(warn_dangling=True), 'thm': XRefRole(warn_dangling=True), @@ -743,12 +934,8 @@ class CoqDomain(Domain): # This one is special 'index': IndexXRefRole(), # These are used for highlighting - 'notation': NotationRole, - 'gallina': GallinaRole, - 'ltac': LtacRole, 'n': NotationRole, - 'g': GallinaRole, - 'l': LtacRole, #FIXME unused? + 'g': CoqCodeRole } indices = [CoqVernacIndex, CoqTacticIndex, CoqOptionIndex, CoqGallinaIndex, CoqProductionIndex, CoqExceptionIndex] @@ -759,7 +946,6 @@ class CoqDomain(Domain): # others, such as “version” 'objects' : { # subdomain → name → docname, objtype, targetid 'cmd': {}, - 'tac': {}, 'tacn': {}, 'opt': {}, 'thm': {}, @@ -829,11 +1015,18 @@ def simplify_source_code_blocks_for_latex(app, doctree, fromdocname): # pylint: for node in doctree.traverse(is_coqtop_or_coqdoc_block): if is_html: node.rawsource = '' # Prevent pygments from kicking in + elif 'coqtop-hidden' in node['classes']: + node.parent.remove(node) else: - if 'coqtop-hidden' in node['classes']: - node.parent.remove(node) - else: - node.replace_self(nodes.literal_block(node.rawsource, node.rawsource, language="Coq")) + node.replace_self(nodes.literal_block(node.rawsource, node.rawsource, language="Coq")) + +COQ_ADDITIONAL_DIRECTIVES = [CoqtopDirective, + CoqdocDirective, + ExampleDirective, + InferenceDirective, + PreambleDirective] + +COQ_ADDITIONAL_ROLES = [GrammarProductionRole] def setup(app): """Register the Coq domain""" @@ -845,12 +1038,13 @@ def setup(app): # Add domain, directives, and roles app.add_domain(CoqDomain) - app.add_role("production", GrammarProductionRole) - app.add_directive("coqtop", CoqtopDirective) - app.add_directive("coqdoc", CoqdocDirective) - app.add_directive("example", ExampleDirective) - app.add_directive("inference", InferenceDirective) - app.add_directive("preamble", PreambleDirective) + + for role in COQ_ADDITIONAL_ROLES: + app.add_role(role.role_name, role) + + for directive in COQ_ADDITIONAL_DIRECTIVES: + app.add_directive(directive.directive_name, directive) + app.add_transform(CoqtopBlocksTransform) app.connect('doctree-resolved', simplify_source_code_blocks_for_latex) @@ -862,4 +1056,7 @@ def setup(app): app.add_stylesheet("notations.css") app.add_stylesheet("pre-text.css") + # Tell Sphinx about extra settings + app.add_config_value("report_undocumented_coq_objects", None, 'env') + return {'version': '0.1', "parallel_read_safe": True} diff --git a/doc/tools/coqrst/regen_readme.py b/doc/tools/coqrst/regen_readme.py new file mode 100755 index 0000000000..e56882a521 --- /dev/null +++ b/doc/tools/coqrst/regen_readme.py @@ -0,0 +1,58 @@ +#!/usr/bin/env python3 +# -*- coding: utf-8 -*- + +"""Rebuild sphinx/README.rst from sphinx/README.template.rst.""" + +import re +from os import sys, path + +SCRIPT_DIR = path.dirname(path.abspath(__file__)) +if __name__ == "__main__" and __package__ is None: + sys.path.append(path.dirname(SCRIPT_DIR)) + +import sphinx +from coqrst import coqdomain + +README_ROLES_MARKER = "[ROLES]" +README_OBJECTS_MARKER = "[OBJECTS]" +README_DIRECTIVES_MARKER = "[DIRECTIVES]" + +FIRST_LINE_BLANKS = re.compile("^(.*)\n *\n") +def format_docstring(template, obj, *strs): + docstring = obj.__doc__.strip() + strs = strs + (FIRST_LINE_BLANKS.sub(r"\1\n", docstring),) + return template.format(*strs) + +SPHINX_DIR = path.join(SCRIPT_DIR, "../../sphinx/") +README_PATH = path.join(SPHINX_DIR, "README.rst") +README_TEMPLATE_PATH = path.join(SPHINX_DIR, "README.template.rst") + +def notation_symbol(d): + return " :black_nib:" if issubclass(d, coqdomain.NotationObject) else "" + +def regen_readme(): + objects_docs = [format_docstring("``.. {}::``{} {}", obj, objname, notation_symbol(obj)) + for objname, obj in sorted(coqdomain.CoqDomain.directives.items())] + + roles = ([(name, cls) + for name, cls in sorted(coqdomain.CoqDomain.roles.items()) + if not isinstance(cls, (sphinx.roles.XRefRole, coqdomain.IndexXRefRole))] + + [(fn.role_name, fn) + for fn in coqdomain.COQ_ADDITIONAL_ROLES]) + roles_docs = [format_docstring("``:{}:`` {}", role, name) + for (name, role) in roles] + + directives_docs = [format_docstring("``.. {}::`` {}", d, d.directive_name) + for d in coqdomain.COQ_ADDITIONAL_DIRECTIVES] + + with open(README_TEMPLATE_PATH, encoding="utf-8") as readme: + contents = readme.read() + + with open(README_PATH, mode="w", encoding="utf-8") as readme: + readme.write(contents + .replace(README_ROLES_MARKER, "\n\n".join(roles_docs)) + .replace(README_OBJECTS_MARKER, "\n\n".join(objects_docs)) + .replace(README_DIRECTIVES_MARKER, "\n\n".join(directives_docs))) + +if __name__ == '__main__': + regen_readme() diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py index efb5cb5505..aeadce4c4a 100644 --- a/doc/tools/coqrst/repl/coqtop.py +++ b/doc/tools/coqrst/repl/coqtop.py @@ -41,7 +41,9 @@ class CoqTop: the ansicolors module) :param args: Additional arugments to coqtop. """ - self.coqtop_bin = coqtop_bin or os.path.join(os.getenv('COQBIN'),"coqtop") + self.coqtop_bin = coqtop_bin or os.path.join(os.getenv('COQBIN', ""), "coqtop") + if not pexpect.utils.which(self.coqtop_bin): + raise ValueError("coqtop binary not found: '{}'".format(self.coqtop_bin)) self.args = (args or []) + ["-boot", "-color", "on"] * color self.coqtop = None |