diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/LICENSE | 19 | ||||
| -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 | ||||
| -rwxr-xr-x | doc/sphinx/conf.py | 1 | ||||
| -rw-r--r-- | doc/sphinx/credits.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/index.rst | 33 | ||||
| -rw-r--r-- | doc/sphinx/introduction.rst | 9 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 39 | ||||
| -rw-r--r-- | doc/tools/coqrst/coqdoc/main.py | 4 | ||||
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 136 |
11 files changed, 162 insertions, 126 deletions
diff --git a/doc/LICENSE b/doc/LICENSE index c223a4e16..c9f574afb 100644 --- a/doc/LICENSE +++ b/doc/LICENSE @@ -14,15 +14,6 @@ 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 @@ -31,16 +22,6 @@ the PostScript, PDF and html outputs) are copyright (c) INRIA 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/sphinx/README.rst b/doc/sphinx/README.rst index 35a605ddd..32de15ee3 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 47d3a7d7c..6a9b343ba 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 6c7258f9c..68b5b9d6f 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/conf.py b/doc/sphinx/conf.py index 135c24aed..8127d3df3 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 a75659798..2562dec46 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 7baa4c450..baf2e0d98 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,18 +80,6 @@ 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 diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index 49f5db342..c7bc69db4 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -1,3 +1,5 @@ +.. _introduction: + ------------------------ Introduction ------------------------ @@ -99,13 +101,6 @@ 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|. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 1c554acdb..6fb73a030 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 ``````````````````````````````````` @@ -5242,7 +5253,7 @@ Notation scope Module name -.. prodn:: name ::= @qualid +.. prodn:: modname ::= @qualid Natural number @@ -5252,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`. @@ -5283,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` @@ -5354,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 } @@ -5369,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 } @@ -5382,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/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py index cedd60d3b..57adcb287 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 ab3a485b2..c9487abf0 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 |