diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/LICENSE | 23 | ||||
| -rw-r--r-- | doc/README.md | 102 | ||||
| -rw-r--r-- | doc/sphinx/README.rst | 15 | ||||
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 23 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/biblio.bib | 32 | ||||
| -rwxr-xr-x | doc/sphinx/conf.py | 1 | ||||
| -rw-r--r-- | doc/sphinx/credits.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/index.rst | 38 | ||||
| -rw-r--r-- | doc/sphinx/introduction.rst | 61 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 10 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 42 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 13 | ||||
| -rw-r--r-- | doc/tools/coqrst/coqdoc/main.py | 4 | ||||
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 136 |
15 files changed, 338 insertions, 171 deletions
diff --git a/doc/LICENSE b/doc/LICENSE index c223a4e16c..3789d91040 100644 --- a/doc/LICENSE +++ b/doc/LICENSE @@ -2,7 +2,7 @@ The Coq Reference Manual is a collective work from the Coq Development Team whose members are listed in the file CREDITS of the Coq source package. All related documents (the LaTeX and BibTeX sources, the embedded png files, and the PostScript, PDF and html outputs) are -copyright (c) INRIA 1999-2006, with the exception of the Ubuntu font +copyright (c) INRIA 1999-2018, with the exception of the Ubuntu font file UbuntuMono-B.ttf, which is Copyright 2010,2011 Canonical Ltd and licensed under the Ubuntu font license, version 1.0 @@ -14,33 +14,14 @@ License, v1.0 or later (the latest version is presently available at http://www.opencontent.org/openpub/). Options A and B are *not* elected. -The Coq Tutorial is a work by Gérard Huet, Gilles Kahn and Christine -Paulin-Mohring. All documents (the LaTeX source and the PostScript, -PDF and html outputs) are copyright (c) INRIA 1999-2006. The material -connected to the Coq Tutorial may be distributed only subject to the -terms and conditions set forth in the Open Publication License, v1.0 -or later (the latest version is presently available at -http://www.opencontent.org/openpub/). Options A and B are *not* -elected. - The Coq Standard Library is a collective work from the Coq Development Team whose members are listed in the file CREDITS of the Coq source package. All related documents (the Coq vernacular source files and the PostScript, PDF and html outputs) are copyright (c) INRIA -1999-2006. The material connected to the Standard Library is +1999-2018. The material connected to the Standard Library is distributed under the terms of the Lesser General Public License version 2.1 or later. -The Tutorial on [Co-]Inductive Types in Coq is a work by Pierre -Castéran and Eduardo Gimenez. All related documents (the LaTeX and -BibTeX sources and the PostScript, PDF and html outputs) are copyright -(c) INRIA 1997-2006. The material connected to the Tutorial on -[Co-]Inductive Types in Coq may be distributed only subject to the -terms and conditions set forth in the Open Publication License, v1.0 -or later (the latest version is presently available at -http://www.opencontent.org/openpub/). Options A and B are -*not* elected. - ---------------------------------------------------------------------- *Open Publication License* diff --git a/doc/README.md b/doc/README.md new file mode 100644 index 0000000000..6c6e1f01fb --- /dev/null +++ b/doc/README.md @@ -0,0 +1,102 @@ +The Coq documentation +===================== + +The Coq documentation includes + +- A Reference Manual +- A document presenting the Coq standard library + +The documentation of the latest released version is available on the Coq +web site at [coq.inria.fr/documentation](http://coq.inria.fr/documentation). + +Additionnally, you can view the documentation for the current master version at +<https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=documentation>. + +The reference manual is written is reStructuredText and compiled +using Sphinx. See [`sphinx/README.rst`](sphinx/README.rst) +to learn more about the format that is used. + +The documentation for the standard library is generated from +the `.v` source files using coqdoc. + +Dependencies +------------ + +### HTML documentation + +To produce the complete documentation in HTML, you will need Coq dependencies +listed in [`INSTALL`](../INSTALL). Additionally, the Sphinx-based +reference manual requires Python 3, and the following Python packages: + + sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime pexpect sphinxcontrib-bibtex + +You can install them using `pip3 install` or using your distribution's package +manager. E.g. under recent Debian-based operating systems (Debian 10 "Buster", +Ubuntu 18.04, ...) you can use: + + apt install python3-sphinx python3-pexpect python3-sphinx-rtd-theme \ + python3-bs4 python3-sphinxcontrib.bibtex python3-pip + +Then, install the missing Python3 Antlr4 package: + + pip3 install antlr4-python3-runtime + +Nix users should get the correct development environment to build the +HTML documentation from Coq's [`default.nix`](../default.nix) (note this +doesn't include the LaTeX packages needed to build the full documentation). + +### Other formats + +To produce the documentation in PDF and PostScript formats, the following +additional tools are required: + + - latex (latex2e) + - pdflatex + - dvips + - makeindex + +Install them using your package manager. E.g. on Debian / Ubuntu: + + apt install texlive-latex-extra texlive-fonts-recommended + +Compilation +----------- + +To produce all documentation about Coq in all formats, just run: + + ./configure # (if you hadn't already) + make doc + + +Alternatively, you can use some specific targets: + +- `make doc-ps` + to produce all PostScript documents + +- `make doc-pdf` + to produce all PDF documents + +- `make doc-html` + to produce all HTML documents + +- `make sphinx` + to produce the HTML version of the reference manual + +- `make stdlib` + to produce all formats of the Coq standard library + + +Also note the `-with-doc yes` option of `./configure` to enable the +build of the documentation as part of the default make target. + + +Installation +------------ + +To install all produced documents, do: + + make install-doc + +This will install the documentation in `/usr/share/doc/coq` unless you +specify another value through the `-docdir` option of `./configure` or the +`DOCDIR` environment variable. diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 35a605ddd3..32de15ee31 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -123,11 +123,24 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the induction principles. -``.. prodn::`` :black_nib: Grammar productions. +``.. prodn::`` A grammar production. 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>`_. + Unlike ``.. productionlist``\ s, this directive accepts notation syntax. + + + Usage:: + + .. prodn:: token += production + .. prodn:: token ::= production + + Example:: + + .. prodn:: term += let: @pattern := @term in @term + .. prodn:: occ_switch ::= { {? + %| - } {* @num } } + ``.. tacn::`` :black_nib: A tactic, or a tactic notation. Example:: diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 47d3a7d7cd..6a9b343ba8 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -310,16 +310,15 @@ The :n:`@ident` is not relevant. It is just used for error messages. The axioms. The optional list of modifiers is used to tailor the behavior of the tactic. The following list describes their syntax and effects: -.. prodn:: - ring_mod ::= abstract %| decidable @term %| morphism @term - %| setoid @term @term - %| constants [@ltac] - %| preprocess [@ltac] - %| postprocess [@ltac] - %| power_tac @term [@ltac] - %| sign @term - %| div @term - +.. productionlist:: coq + ring_mod : abstract | decidable `term` | morphism `term` + : | setoid `term` `term` + : | constants [`ltac`] + : | preprocess [`ltac`] + : | postprocess [`ltac`] + : | power_tac `term` [`ltac`] + : | sign `term` + : | div `term` abstract declares the ring as abstract. This is the default. @@ -663,8 +662,8 @@ messages. :n:`@term` is a proof that the field signature satisfies the (semi-)field axioms. The optional list of modifiers is used to tailor the behavior of the tactic. -.. prodn:: - field_mod := @ring_mod %| completeness @term +.. productionlist:: coq + field_mod : `ring_mod` | completeness `term` Since field tactics are built upon ``ring`` tactics, all modifiers of the ``Add Ring`` apply. There is only one diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 6c7258f9c5..68b5b9d6fe 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -296,6 +296,10 @@ Variants: This variant declares a class a posteriori from a constant or inductive definition. No methods or instances are defined. + .. warn:: @ident is already declared as a typeclass + + This command has no effect when used on a typeclass. + .. cmd:: Instance @ident {? @binders} : Class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi } The :cmd:`Instance` command is used to declare a type class instance named diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index 3e988709c5..3574bf6750 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -3,6 +3,21 @@ @String{lnai = "Lecture Notes in Artificial Intelligence"} @String{SV = "{Sprin-ger-Verlag}"} +@InCollection{Asp00, + Title = {Proof General: A Generic Tool for Proof Development}, + Author = {Aspinall, David}, + Booktitle = {Tools and Algorithms for the Construction and + Analysis of Systems, {TACAS} 2000}, + Publisher = {Springer Berlin Heidelberg}, + Year = {2000}, + Editor = {Graf, Susanne and Schwartzbach, Michael}, + Pages = {38--43}, + Series = {Lecture Notes in Computer Science}, + Volume = {1785}, + Doi = {10.1007/3-540-46419-0_3}, + ISBN = {978-3-540-67282-1}, +} + @Book{Bar81, author = {H.P. Barendregt}, publisher = {North-Holland}, @@ -290,16 +305,13 @@ the Calculus of Inductive Constructions}}, year = {1995} } -@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/}} +@InProceedings{Pit16, + Title = {Company-Coq: Taking Proof General one step closer to a real IDE}, + Author = {Pit-Claudel, Clément and Courtieu, Pierre}, + Booktitle = {CoqPL'16: The Second International Workshop on Coq for PL}, + Year = {2016}, + Month = jan, + Doi = {10.5281/zenodo.44331}, } @Book{RC95, diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 135c24aed9..8127d3df3f 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -104,7 +104,6 @@ exclude_patterns = [ 'Thumbs.db', '.DS_Store', 'introduction.rst', - 'credits.rst', 'README.rst', 'README.template.rst' ] diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst index a756597986..2562dec468 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits.rst @@ -1,3 +1,8 @@ +.. include:: preamble.rst +.. include:: replaces.rst + +.. _credits: + ------------------------------------------- Credits ------------------------------------------- diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst index 136f9088b1..baf2e0d981 100644 --- a/doc/sphinx/index.rst +++ b/doc/sphinx/index.rst @@ -1,16 +1,31 @@ -.. _introduction: - .. include:: preamble.rst .. include:: replaces.rst .. include:: introduction.rst -.. include:: credits.rst ------------------ Table of contents ------------------ .. toctree:: + :caption: Indexes + + genindex + coq-cmdindex + coq-tacindex + coq-optindex + coq-exnindex + +.. No entries yet + * :index:`thmindex` + +.. toctree:: + :caption: Preamble + + self + credits + +.. toctree:: :caption: The language language/gallina-specification-language @@ -65,19 +80,12 @@ Table of contents zebibliography -.. toctree:: - :caption: Indexes - - genindex - coq-cmdindex - coq-tacindex - coq-optindex - coq-exnindex - -.. No entries yet - * :index:`thmindex` - This material (the Coq Reference Manual) may be distributed only subject to the terms and conditions set forth in the Open Publication License, v1.0 or later (the latest version is presently available at http://www.opencontent.org/openpub). Options A and B are not elected. + +.. [#PG] Proof-General is available at https://proofgeneral.github.io/. + Optionally, you can enhance it with the minor mode + Company-Coq :cite:`Pit16` + (see https://github.com/cpitclaudel/company-coq). diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index 75ff72c4da..c7bc69db4e 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -1,3 +1,5 @@ +.. _introduction: + ------------------------ Introduction ------------------------ @@ -26,37 +28,35 @@ programs called *tactics*. All services of the |Coq| proof assistant are accessible by interpretation of a command language called *the vernacular*. -Coq has an interactive mode in which commands are interpreted as the +Coq has an interactive mode in which commands are interpreted as the user types them in from the keyboard and a compiled mode where commands are processed from a file. -- The interactive mode may be used as a debugging mode in which the - user can develop his theories and proofs step by step, backtracking - if needed and so on. The interactive mode is run with the `coqtop` - command from the operating system (which we shall assume to be some - variety of UNIX in the rest of this document). +- In interactive mode, users can develop their theories and proofs step by + step, and query the system for available theorems and definitions. The + interactive mode is generally run with the help of an IDE, such + as CoqIDE, documented in :ref:`coqintegrateddevelopmentenvironment`, + Emacs with Proof-General :cite:`Asp00` [#PG]_, + or jsCoq to run Coq in your browser (see https://github.com/ejgallego/jscoq). + The `coqtop` read-eval-print-loop can also be used directly, for debugging + purposes. - The compiled mode acts as a proof checker taking a file containing a whole development in order to ensure its correctness. Moreover, |Coq|’s compiler provides an output file containing a compact representation of its input. The compiled mode is run with the `coqc` - command from the operating system. - -These two modes are documented in Chapter :ref:`thecoqcommands`. + command. -Other modes of interaction with |Coq| are possible: through an emacs shell -window, an emacs generic user-interface for proof assistant (Proof -General :cite:`ProofGeneral`) or through a customized -interface (PCoq :cite:`Pcoq`). These facilities are not -documented here. There is also a |Coq| Integrated Development Environment -described in :ref:`coqintegrateddevelopmentenvironment`. +.. seealso:: :ref:`thecoqcommands`. How to read this book ===================== -This is a Reference Manual, not a User Manual, so it is not made for a -continuous reading. However, it has some structure that is explained -below. +This is a Reference Manual, so it is not made for a continuous reading. +We recommend using the various indexes to quickly locate the documentation +you are looking for. There is a global index, and a number of specific indexes +for tactics, vernacular commands, and error messages and warnings. +Nonetheless, the manual has some structure that is explained below. - The first part describes the specification language, |Gallina|. Chapters :ref:`gallinaspecificationlanguage` and :ref:`extensionsofgallina` describe the concrete @@ -66,7 +66,7 @@ below. of the formalism. Chapter :ref:`themodulesystem` describes the module system. -- The second part describes the proof engine. It is divided in five +- The second part describes the proof engine. It is divided in six chapters. Chapter :ref:`vernacularcommands` presents all commands (we call them *vernacular commands*) that are not directly related to interactive proving: requests to the environment, complete or partial @@ -77,42 +77,35 @@ below. *tactics*. The language to combine these tactics into complex proof strategies is given in Chapter :ref:`ltac`. Examples of tactics are described in Chapter :ref:`detailedexamplesoftactics`. + Finally, the |SSR| proof language is presented in + Chapter :ref:`thessreflectprooflanguage`. -- The third part describes how to extend the syntax of |Coq|. It - corresponds to the Chapter :ref:`syntaxextensionsandinterpretationscopes`. +- The third part describes how to extend the syntax of |Coq| in + Chapter :ref:`syntaxextensionsandinterpretationscopes` and how to define + new induction principles in Chapter :ref:`proofschemes`. - In the fourth part more practical tools are documented. First in Chapter :ref:`thecoqcommands`, the usage of `coqc` (batch mode) and `coqtop` (interactive mode) with their options is described. Then, in Chapter :ref:`utilities`, various utilities that come with the |Coq| distribution are presented. Finally, Chapter :ref:`coqintegrateddevelopmentenvironment` - describes the |Coq| integrated development environment. + describes CoqIDE. - The fifth part documents a number of advanced features, including coercions, canonical structures, typeclasses, program extraction, and specialized solvers and tactics. See the table of contents for a complete list. -At the end of the document, after the global index, the user can find -specific indexes for tactics, vernacular commands, and error messages. - List of additional documentation ================================ This manual does not contain all the documentation the user may need about |Coq|. Various informations can be found in the following documents: -Tutorial - A companion volume to this reference manual, the |Coq| Tutorial, is - aimed at gently introducing new users to developing proofs in |Coq| - without assuming prior knowledge of type theory. In a second step, - the user can read also the tutorial on recursive types (document - `RecTutorial.ps`). - Installation A text file `INSTALL` that comes with the sources explains how to install |Coq|. The |Coq| standard library A commented version of sources of the |Coq| standard library - (including only the specifications, the proofs are removed) is given - in the additional document `Library.ps`. + (including only the specifications, the proofs are removed) is + available at https://coq.inria.fr/stdlib/. diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index c21d8d4ec8..8fbd2ea4e7 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -23,8 +23,9 @@ expressions. In this sense, the :cmd:`Record` construction allows defining .. _record_grammar: .. productionlist:: `sentence` - record : `record_keyword` `ident` [ `binders` ] [: `sort` ] := [ `ident` ] { [ `field` ; … ; `field` ] }. + record : `record_keyword` `record_body` with … with `record_body` record_keyword : Record | Inductive | CoInductive + record_body : `ident` [ `binders` ] [: `sort` ] := [ `ident` ] { [ `field` ; … ; `field` ] }. field : `ident` [ `binders` ] : `type` [ where `notation` ] : | `ident` [ `binders` ] [: `type` ] := `term` @@ -167,12 +168,13 @@ and the syntax `term.(@qualid` |term_1| |term_n| `)` to `@qualid` |term_1| `…` In each case, `term` is the object projected and the other arguments are the parameters of the inductive type. + .. note:: Records defined with the ``Record`` keyword are not allowed to be recursive (references to the record's name in the type of its field raises an error). To define recursive records, one can use the ``Inductive`` and ``CoInductive`` keywords, resulting in an inductive or co-inductive record. - A *caveat*, however, is that records cannot appear in mutually inductive - (or co-inductive) definitions. + Definition of mutal inductive or co-inductive records are also allowed, as long + as all of the types in the block are records. .. note:: Induction schemes are automatically generated for inductive records. Automatic generation of induction schemes for non-recursive records @@ -2226,7 +2228,7 @@ existential variable used in the same context as its context of definition is wr Check (fun x y => _) 0 1. Existential variables can be named by the user upon creation using -the syntax ``?``\ `ident`. This is useful when the existential +the syntax :n:`?[@ident]`. This is useful when the existential variable needs to be explicitly handled later in the script (e.g. with a named-goal selector, see :ref:`goal-selectors`). diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 3b2009657f..6fb73a030f 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -623,7 +623,9 @@ where: + In the occurrence switch :token:`occ_switch`, if the first element of the list is a natural, this element should be a number, and not an Ltac variable. The empty list ``{}`` is not interpreted as a valid occurrence - switch. + switch, it is rather used as a flag to signal the intent of the user to + clear the name following it (see :ref:`ssr_rewrite_occ_switch` and + :ref:`introduction_ssr`) The tactic: @@ -1484,7 +1486,7 @@ The abstract tactic ``````````````````` .. tacn:: abstract: {+ d_item} - :name abstract (ssreflect) + :name: abstract (ssreflect) This tactic assigns an abstract constant previously introduced with the ``[: name ]`` intro pattern (see section :ref:`introduction_ssr`). @@ -1539,7 +1541,7 @@ whose general syntax is :name: => .. prodn:: - i_item ::= @i_pattern %| @s_item %| @clear_switch %| /@term + i_item ::= @i_pattern %| @s_item %| @clear_switch %| {? %{%} } /@term .. prodn:: s_item ::= /= %| // %| //= @@ -1641,6 +1643,11 @@ The view is applied to the top assumption. While it is good style to use the :token:`i_item` i * to pop the variables and assumptions corresponding to each constructor, this is not enforced by |SSR|. +``/`` :token:`term` + Interprets the top of the stack with the view :token:`term`. + It is equivalent to ``move/term``. The optional flag ``{}`` can + be used to signal that the :token:`term`, when it is a context entry, + has to be cleared. ``-`` does nothing, but counts as an intro pattern. It can also be used to force the interpretation of ``[`` :token:`i_item` * ``| … |`` @@ -2402,7 +2409,7 @@ tactic: The behavior of the defective have tactic makes it possible to generalize it in the following general construction: -.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item | {+ @binder } } {? : @term } {? := @term | by @tactic } +.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item | {+ @ssr_binder } } {? : @term } {? := @term | by @tactic } Open syntax is supported for both :token:`term`. For the description of :token:`i_item` and :token:`s_item` see section @@ -3236,6 +3243,7 @@ the equality. Indeed the left hand side of ``H`` does not match the redex identified by the pattern ``x + y * 4``. +.. _ssr_rewrite_occ_switch: Occurrence switches and redex switches `````````````````````````````````````` @@ -3260,6 +3268,9 @@ the rewrite tactic. The effect of the tactic on the initial goal is to rewrite this lemma at the second occurrence of the first matching ``x + y + 0`` of the explicit rewrite redex ``_ + y + 0``. +An empty occurrence switch ``{}`` is not interpreted as a valid occurrence +switch. It has the effect of clearing the :token:`r_item` (when it is the name +of a context entry). Occurrence selection and repetition ``````````````````````````````````` @@ -3657,7 +3668,8 @@ selective rewriting, blocking on the fly the reduction in the term ``t``. .. coqtop:: reset - From Coq Require Import ssreflect ssrfun ssrbool List. + From Coq Require Import ssreflect ssrfun ssrbool. + From Coq Require Import List. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -5241,7 +5253,7 @@ Notation scope Module name -.. prodn:: name ::= @qualid +.. prodn:: modname ::= @qualid Natural number @@ -5251,14 +5263,10 @@ where :token:`ident` is an Ltac variable denoting a standard |Coq| numeral (should not be the name of a tactic which can be followed by a bracket ``[``, like ``do``, ``have``,…) -Pattern - -.. prodn:: pattern ::= @term - Items and switches ~~~~~~~~~~~~~~~~~~ -.. prodn:: binder ::= @ident %| ( @ident {? : @term } ) +.. prodn:: ssr_binder ::= @ident %| ( @ident {? : @term } ) binder see :ref:`abbreviations_ssr`. @@ -5282,7 +5290,7 @@ generalization item see :ref:`structure_ssr` intro pattern :ref:`introduction_ssr` -.. prodn:: i_item ::= @clear_switch %| @s_item %| @i_pattern %| / @term +.. prodn:: i_item ::= @clear_switch %| @s_item %| @i_pattern %| {? %{%} } / @term intro item see :ref:`introduction_ssr` @@ -5353,8 +5361,8 @@ case analysis see :ref:`the_defective_tactics_ssr` rewrite see :ref:`rewriting_ssr` -.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @binder } } {? : @term } := @term -.. tacv:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @binder } } : @term {? by @tactic } +.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } {? : @term } := @term +.. tacv:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } : @term {? by @tactic } .. tacn:: have suff {? @clear_switch } {? @i_pattern } {? : @term } := @term .. tacv:: have suff {? @clear_switch } {? @i_pattern } : @term {? by @tactic } .. tacv:: gen have {? @ident , } {? @i_pattern } : {+ @gen_item } / @term {? by @tactic } @@ -5368,9 +5376,9 @@ forward chaining see :ref:`structure_ssr` specializing see :ref:`structure_ssr` -.. tacn:: suff {* @i_item } {? @i_pattern } {+ @binder } : @term {? by @tactic } +.. tacn:: suff {* @i_item } {? @i_pattern } {+ @ssr_binder } : @term {? by @tactic } :name: suff -.. tacv:: suffices {* @i_item } {? @i_pattern } {+ @binder } : @term {? by @tactic } +.. tacv:: suffices {* @i_item } {? @i_pattern } {+ @ssr_binder } : @term {? by @tactic } :name: suffices .. tacv:: suff {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic } .. tacv:: suffices {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic } @@ -5381,7 +5389,7 @@ backchaining see :ref:`structure_ssr` local definition :ref:`definitions_ssr` -.. tacv:: pose @ident {+ @binder } := @term +.. tacv:: pose @ident {+ @ssr_binder } := @term local function definition diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 29c2f8b815..d0a0d568ea 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3949,9 +3949,20 @@ succeeds, and results in an error otherwise. :name: constr_eq This tactic checks whether its arguments are equal modulo alpha - conversion and casts. + conversion, casts and universe constraints. It may unify universes. .. exn:: Not equal. +.. exn:: Not equal (due to universes). + +.. tacn:: constr_eq_strict @term @term + :name: constr_eq_strict + + This tactic checks whether its arguments are equal modulo alpha + conversion, casts and universe constraints. It does not add new + constraints. + +.. exn:: Not equal. +.. exn:: Not equal (due to universes). .. tacn:: unify @term @term :name: unify diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py index cedd60d3bc..57adcb287c 100644 --- a/doc/tools/coqrst/coqdoc/main.py +++ b/doc/tools/coqrst/coqdoc/main.py @@ -20,6 +20,7 @@ lexer. """ import os +import platform from tempfile import mkstemp from subprocess import check_output @@ -36,6 +37,9 @@ 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") + if platform.system().startswith("CYGWIN"): + # coqdoc currently doesn't accept cygwin style paths in the form "/cygdrive/c/..." + filename = check_output(["cygpath", "-w", filename]).decode("utf-8").strip() try: os.write(fd, COQDOC_HEADER.encode("utf-8")) os.write(fd, coq_code.encode("utf-8")) diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index ab3a485b22..c9487abf03 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -28,6 +28,7 @@ from docutils.parsers.rst.directives.admonitions import BaseAdmonition from sphinx import addnodes from sphinx.roles import XRefRole +from sphinx.errors import ExtensionError from sphinx.util.nodes import set_source_info, set_role_source_info, make_refnode from sphinx.util.logging import getLogger from sphinx.directives import ObjectDescription @@ -103,10 +104,16 @@ class CoqObject(ObjectDescription): 'undocumented': directives.flag } - def _subdomain(self): + def subdomain_data(self): if self.subdomain is None: raise ValueError() - return self.subdomain + return self.env.domaindata['coq']['objects'][self.subdomain] + + def _render_annotation(self, signode): + if self.annotation: + annot_node = nodes.inline(self.annotation, self.annotation, classes=['sigannot']) + signode += addnodes.desc_annotation(self.annotation, '', annot_node) + signode += nodes.Text(' ') def handle_signature(self, signature, signode): """Prefix signature with the proper annotation, then render it using @@ -114,29 +121,32 @@ class CoqObject(ObjectDescription): :returns: the name given to the resulting node, if any """ - if self.annotation: - annotation = self.annotation + ' ' - signode += addnodes.desc_annotation(annotation, annotation) + self._render_annotation(signode) self._render_signature(signature, signode) return self._names.get(signature) or self._name_from_signature(signature) + def _warn_if_duplicate_name(self, objects, name): + """Check that two objects in the same domain don't have the same name.""" + if name in objects: + MSG = 'Duplicate object: {}; other is at {}' + msg = MSG.format(name, self.env.doc2path(objects[name][0])) + self.state_machine.reporter.warning(msg, line=self.lineno) + def _record_name(self, name, target_id): """Record a name, mapping it to target_id Warns if another object of the same name already exists. """ - names_in_subdomain = self.env.domaindata['coq']['objects'][self._subdomain()] - # Check that two objects in the same domain don't have the same name - if name in names_in_subdomain: - self.state_machine.reporter.warning( - 'Duplicate Coq object: {}; other is at {}'.format( - name, self.env.doc2path(names_in_subdomain[name][0])), - line=self.lineno) + names_in_subdomain = self.subdomain_data() + self._warn_if_duplicate_name(names_in_subdomain, name) names_in_subdomain[name] = (self.env.docname, self.objtype, target_id) + def _target_id(self, name): + return make_target(self.objtype, nodes.make_id(name)) + def _add_target(self, signode, name): """Register a link target ‘name’, pointing to signode.""" - targetid = make_target(self.objtype, nodes.make_id(name)) + targetid = self._target_id(name) if targetid not in self.state.document.ids: signode['ids'].append(targetid) signode['names'].append(name) @@ -314,50 +324,71 @@ class OptionObject(NotationObject): def _name_from_signature(self, signature): return stringify_with_ellipses(signature) -class ProductionObject(NotationObject): - """Grammar productions. +class ProductionObject(CoqObject): + r"""A grammar production. 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>`_. + + Unlike ``.. productionlist``\ s, this directive accepts notation syntax. + + + Usage:: + + .. prodn:: token += production + .. prodn:: token ::= production + + Example:: + + .. prodn:: term += let: @pattern := @term in @term + .. prodn:: occ_switch ::= { {? + %| - } {* @num } } + """ - # FIXME (CPC): I have no idea what this does :/ Someone should add an example. subdomain = "prodn" - index_suffix = None - annotation = None + #annotation = "Grammar production" - # override to create link targets for production left-hand sides - def run(self): + def _render_signature(self, signature, signode): + raise NotImplementedError(self) + + SIG_ERROR = ("Invalid syntax in ``.. prodn::`` directive" + + "\nExpected ``name ::= ...`` or ``name += ...``" + + " (e.g. ``pattern += constr:(@ident)``)") + + def handle_signature(self, signature, signode): + nsplits = 2 + parts = signature.split(maxsplit=nsplits) + if len(parts) != 3: + raise ExtensionError(ProductionObject.SIG_ERROR) + + lhs, op, rhs = (part.strip() for part in parts) + if op not in ["::=", "+="]: + raise ExtensionError(ProductionObject.SIG_ERROR) + + self._render_annotation(signode) + + lhs_op = '{} {} '.format(lhs, op) + lhs_node = nodes.literal(lhs_op, lhs_op) + + position = self.state_machine.get_source_and_line(self.lineno) + rhs_node = parse_notation(rhs, *position) + signode += addnodes.desc_name(signature, '', lhs_node, rhs_node) + + return ('token', lhs) if op == '::=' else None + + def _add_index_entry(self, name, target): + pass + + def _target_id(self, name): + # Use `name[1]` instead of ``nodes.make_id(name[1])`` to work around + # https://github.com/sphinx-doc/sphinx/issues/4983 + return 'grammar-token-{}'.format(name[1]) + + def _record_name(self, name, targetid): env = self.state.document.settings.env objects = env.domaindata['std']['objects'] - - class ProdnError(Exception): - """Exception for ill-formed prodn""" - pass - - [idx, node] = super().run() - try: - # find LHS of production - inline_lhs = node[0][0][0][0] # may be fragile !!! - lhs_str = str(inline_lhs) - if lhs_str[0:7] != "<inline": - raise ProdnError("Expected atom on LHS") - lhs = inline_lhs[0] - # register link target - subnode = addnodes.production() - subnode['tokenname'] = lhs - idname = 'grammar-token-%s' % subnode['tokenname'] - if idname not in self.state.document.ids: - subnode['ids'].append(idname) - self.state.document.note_implicit_target(subnode, subnode) - objects['token', subnode['tokenname']] = env.docname, idname - subnode.extend(token_xrefs(lhs)) - # patch in link target - inline_lhs['ids'].append(idname) - except ProdnError as err: - getLogger(__name__).warning("Could not create link target for prodn: " + str(err) + - "\nSphinx represents the prodn as: " + str(node) + "\n") - return [idx, node] + self._warn_if_duplicate_name(objects, name) + objects[name] = env.docname, targetid class ExceptionObject(NotationObject): """An error raised by a Coq command or tactic. @@ -841,11 +872,6 @@ class CoqOptionIndex(CoqSubdomainsIndex): class CoqGallinaIndex(CoqSubdomainsIndex): name, localname, shortname, subdomains = "thmindex", "Gallina Index", "theorems", ["thm"] -# we specify an index to make productions fit into the framework of notations -# but not likely to include a link to this index -class CoqProductionIndex(CoqSubdomainsIndex): - name, localname, shortname, subdomains = "prodnindex", "Production Index", "productions", ["prodn"] - class CoqExceptionIndex(CoqSubdomainsIndex): name, localname, shortname, subdomains = "exnindex", "Errors and Warnings Index", "errors", ["exn", "warn"] @@ -952,7 +978,7 @@ class CoqDomain(Domain): 'g': CoqCodeRole } - indices = [CoqVernacIndex, CoqTacticIndex, CoqOptionIndex, CoqGallinaIndex, CoqProductionIndex, CoqExceptionIndex] + indices = [CoqVernacIndex, CoqTacticIndex, CoqOptionIndex, CoqGallinaIndex, CoqExceptionIndex] data_version = 1 initial_data = { @@ -1047,7 +1073,7 @@ def setup(app): # A few sanity checks: subdomains = set(obj.subdomain for obj in CoqDomain.directives.values()) - assert subdomains == set(chain(*(idx.subdomains for idx in CoqDomain.indices))) + assert subdomains.issuperset(chain(*(idx.subdomains for idx in CoqDomain.indices))) assert subdomains.issubset(CoqDomain.roles.keys()) # Add domain, directives, and roles |