aboutsummaryrefslogtreecommitdiff
path: root/doc/tools
diff options
context:
space:
mode:
Diffstat (limited to 'doc/tools')
-rw-r--r--doc/tools/Translator.tex2
-rw-r--r--doc/tools/coqrst/coqdoc/main.py9
-rw-r--r--doc/tools/coqrst/coqdomain.py702
-rw-r--r--doc/tools/coqrst/notations/CoqNotations.ttfbin0 -> 37988 bytes
-rw-r--r--doc/tools/coqrst/notations/TacticNotations.g11
-rw-r--r--doc/tools/coqrst/notations/TacticNotations.tokens3
-rw-r--r--doc/tools/coqrst/notations/TacticNotationsLexer.py48
-rw-r--r--doc/tools/coqrst/notations/TacticNotationsLexer.tokens3
-rw-r--r--doc/tools/coqrst/notations/TacticNotationsParser.py71
-rw-r--r--doc/tools/coqrst/notations/UbuntuMono-Square.ttfbin38200 -> 0 bytes
-rwxr-xr-xdoc/tools/coqrst/notations/fontsupport.py7
-rw-r--r--doc/tools/coqrst/notations/html.py9
-rw-r--r--doc/tools/coqrst/notations/sphinx.py21
-rwxr-xr-xdoc/tools/coqrst/regen_readme.py58
-rw-r--r--doc/tools/coqrst/repl/coqtop.py9
15 files changed, 708 insertions, 245 deletions
diff --git a/doc/tools/Translator.tex b/doc/tools/Translator.tex
index 3ee65d6f22..d8ac640f2a 100644
--- a/doc/tools/Translator.tex
+++ b/doc/tools/Translator.tex
@@ -490,7 +490,7 @@ to be applied are separated by a {\tt =>}.
to turn implicit only the arguments that are {\em strictly} implicit
(or rigid), i.e. that remains inferable whatever the other arguments
are. For instance {\tt x} inferable from {\tt P x} is not strictly
-inferable since it can disappears if {\tt P} is instanciated by a term
+inferable since it can disappears if {\tt P} is instantiated by a term
which erases {\tt x}.
\begin{transbox}
diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py
index d464f75bb2..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
@@ -32,14 +33,18 @@ 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")
+ 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"))
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 663ab9d371..2c69dcfe08 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 ##
@@ -27,12 +28,13 @@ 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
from sphinx.domains import Domain, ObjType, Index
from sphinx.domains.std import token_xrefs
-from sphinx.ext.mathbase import MathDirective, displaymath
+from sphinx.ext import mathbase
from . import coqdoc
from .repl import ansicolors
@@ -56,31 +58,47 @@ def make_target(objtype, targetid):
"""Create a target to an object of type objtype and id targetid"""
return "coq:{}.{}".format(objtype, targetid)
+def make_math_node(latex, docname, nowrap):
+ node = mathbase.displaymath()
+ node['latex'] = latex
+ node['label'] = None # Otherwise equations are numbered
+ node['nowrap'] = nowrap
+ node['docname'] = docname
+ node['number'] = None
+ return node
+
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,49 +107,70 @@ 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,
+ # noindex omits this object from its index
+ 'noindex': 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
- _render_signature.
+ ``_render_signature`` (for example, add “Command” in front of commands).
: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._name_from_signature(signature)
-
- @property
- def _index_suffix(self):
- if self.index_suffix:
- return " " + self.index_suffix
+ name = self._names.get(signature)
+ if name is None:
+ name = self._name_from_signature(signature)
+ # remove trailing ‘.’ found in commands, but not ‘...’ (ellipsis)
+ if name is not None and name.endswith(".") and not name.endswith("..."):
+ name = name[:-1]
+ return name
+
+ 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 _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)
@@ -141,79 +180,169 @@ 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
- self.indexnode['entries'].append(('single', index_text, target, '', None))
-
- def run(self):
- """Small extension of the parent's run method, handling user-provided names."""
- [idx, node] = super().run()
- custom_name = self.options.get("name")
- if custom_name:
- self.add_target_and_index(custom_name, "", node.children[0])
- return [idx, node]
+ """Add `name` (pointing to `target`) to the main index."""
+ assert isinstance(name, str)
+ if not name.startswith("_"):
+ # remove trailing . , found in commands, but not ... (ellipsis)
+ trim = name.endswith(".") and not name.endswith("...")
+ index_text = name[:-1] if trim else 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`.
+ This is only called (from ``ObjectDescription.run``) if ``:noindex:`` isn't specified."""
if name:
target = self._add_target(signode, name)
- # remove trailing . , found in commands, but not ... (ellipsis)
- if name[-1] == "." and not name[-3:] == "..." :
- name = name[0:-1]
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 _prepare_names(self):
+ sigs = self.get_signatures()
+ names = self.options.get("name")
+ if names is None:
+ self._names = {}
+ else:
+ names = [n.strip() for n in names.split(";")]
+ if len(names) != len(sigs):
+ ERR = ("Expected {} semicolon-separated names, got {}. " +
+ "Please provide one name per signature line.")
+ raise self.error(ERR.format(len(names), len(sigs)))
+ self._names = dict(zip(sigs, names))
+
+ def run(self):
+ self._warn_if_undocumented()
+ self._prepare_names()
+ 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"
def _name_from_signature(self, signature):
- return stringify_with_ellipses(signature)
+ m = re.match(r"[a-zA-Z ]+", signature)
+ if m:
+ 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"
+ def _name_from_signature(self, signature):
+ 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 (a setting with non-boolean value, e.g. a string or numeric value).
+
+ Example::
+
+ .. opt:: Hyps Limit @num
+ :name Hyps Limit
+
+ Controls the maximum number of hypotheses displayed in goals after
+ application of a tactic.
+ """
subdomain = "opt"
index_suffix = "(opt)"
annotation = "Option"
@@ -221,47 +350,126 @@ class OptionObject(NotationObject):
def _name_from_signature(self, signature):
return stringify_with_ellipses(signature)
-class ProductionObject(NotationObject):
- """An object to represent grammar productions"""
+
+class FlagObject(NotationObject):
+ """A Coq flag (i.e. a boolean setting).
+
+ Example::
+
+ .. flag:: Nonrecursive Elimination Schemes
+
+ Controls whether types declared with the keywords
+ :cmd:`Variant` and :cmd:`Record` get an automatic declaration of
+ induction principles.
+ """
+ subdomain = "flag"
+ index_suffix = "(flag)"
+ annotation = "Flag"
+
+ def _name_from_signature(self, signature):
+ return stringify_with_ellipses(signature)
+
+
+class TableObject(NotationObject):
+ """A Coq table, i.e. a setting that is a set of values.
+
+ Example::
+
+ .. table:: Search Blacklist @string
+ :name: Search Blacklist
+
+ Controls ...
+ """
+ subdomain = "table"
+ index_suffix = "(table)"
+ annotation = "Table"
+
+ def _name_from_signature(self, signature):
+ return stringify_with_ellipses(signature)
+
+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 } }
+
+ """
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 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"
@@ -272,7 +480,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"
@@ -283,14 +503,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 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:
@@ -303,15 +542,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.
+ r"""A reST directive to describe interactions with Coqtop.
Usage::
- .. coqtop:: (options)+
+ .. coqtop:: options…
Coq code to send to coqtop
@@ -322,42 +560,69 @@ class CoqtopDirective(Directive):
Print nat.
Definition a := 1.
+ The blank line after the directive is required. If you begin a proof,
+ include an ``Abort`` afterwards to reset coqtop for the next example.
+
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
+ option_spec = { 'name': directives.unchanged }
+ directive_name = "coqtop"
def run(self):
# Uses a ‘container’ instead of a ‘literal_block’ to disable
# Pygments-based post-processing (we could also set rawsource to '')
content = '\n'.join(self.content)
- options = self.arguments[0].split() if self.arguments else ['in']
- if 'all' in options:
- options.extend(['in', 'out'])
- node = nodes.container(content, coqtop_options = list(set(options)),
+ args = self.arguments[0].split() if self.arguments else ['in']
+ if 'all' in args:
+ args.extend(['in', 'out'])
+ node = nodes.container(content, coqtop_options = list(set(args)),
classes=['coqtop', 'literal-block'])
self.add_name(node)
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
+ option_spec = { 'name': directives.unchanged }
+ directive_name = "coqdoc"
def run(self):
# Uses a ‘container’ instead of a ‘literal_block’ to disable
@@ -365,41 +630,91 @@ class CoqdocDirective(Directive):
content = '\n'.join(self.content)
node = nodes.inline(content, '', *highlight_using_coqdoc(content))
wrapper = nodes.container(content, node, classes=['coqdoc', 'literal-block'])
+ self.add_name(wrapper)
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.
+
+ Optionally, any text immediately following the ``.. example::`` header is
+ used as the example's title.
+
+ 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"
+ optional_arguments = 1
def run(self):
# ‘BaseAdmonition’ checks whether ‘node_class’ is ‘nodes.admonition’,
# and uses arguments[0] as the title in that case (in other cases, the
# title is unset, and it is instead set in the HTML visitor).
- assert not self.arguments # Arguments have been parsed as content
- self.arguments = ['Example']
+ assert len(self.arguments) <= 1
+ self.arguments = [": ".join(['Example'] + self.arguments)]
self.options['classes'] = ['admonition', 'note']
return super().run()
-class PreambleDirective(MathDirective):
- r"""A reST directive for hidden math.
+class PreambleDirective(Directive):
+ r"""A reST directive to include a TeX file.
- Mostly useful to let MathJax know about `\def`s and `\newcommand`s
+ Mostly useful to let MathJax know about `\def`s and `\newcommand`s. The
+ contents of the TeX file are wrapped in a math environment, as MathJax
+ doesn't process LaTeX definitions otherwise.
+
+ Usage::
+
+ .. preamble:: preamble.tex
"""
+ has_content = False
+ required_arguments = 1
+ optional_arguments = 0
+ final_argument_whitespace = True
+ option_spec = {}
+ directive_name = "preamble"
+
def run(self):
- self.options['nowrap'] = True
- [node] = super().run()
+ document = self.state.document
+ env = document.settings.env
+
+ if not document.settings.file_insertion_enabled:
+ msg = 'File insertion disabled'
+ return [document.reporter.warning(msg, line=self.lineno)]
+
+ rel_fname, abs_fname = env.relfn2path(self.arguments[0])
+ env.note_dependency(rel_fname)
+
+ with open(abs_fname, encoding="utf-8") as ltx:
+ latex = ltx.read()
+
+ node = make_math_node(latex, env.docname, nowrap=False)
node['classes'] = ["math-preamble"]
+ set_source_info(self, node)
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 premises
+ --------------------------
conclusion
Example::
@@ -416,15 +731,7 @@ class InferenceDirective(Directive):
optional_arguments = 0
has_content = True
final_argument_whitespace = True
-
- def make_math_node(self, latex):
- node = displaymath()
- node['latex'] = latex
- node['label'] = None # Otherwise equations are numbered
- node['nowrap'] = False
- node['docname'] = self.state.document.settings.env.docname
- node['number'] = None
- return node
+ directive_name = "inference"
@staticmethod
def prepare_latex_operand(op):
@@ -445,7 +752,8 @@ class InferenceDirective(Directive):
title = self.arguments[0]
content = '\n'.join(self.content)
latex = self.prepare_latex(content)
- math_node = self.make_math_node(latex)
+ docname = self.state.document.settings.env.docname
+ math_node = make_math_node(latex, docname, nowrap=False)
tid = nodes.make_id(title)
target = nodes.target('', '', ids=['inference-' + tid])
@@ -592,23 +900,28 @@ class CoqtopBlocksTransform(Transform):
kept_node['classes'] = [c for c in kept_node['classes']
if c != 'coqtop-hidden']
- def merge_consecutive_coqtop_blocks(self):
+ @staticmethod
+ def merge_consecutive_coqtop_blocks(app, doctree, _):
"""Merge consecutive divs wrapping lists of Coq sentences; keep ‘dl’s separate."""
- for node in self.document.traverse(CoqtopBlocksTransform.is_coqtop_block):
+ for node in doctree.traverse(CoqtopBlocksTransform.is_coqtop_block):
if node.parent:
+ rawsources, names = [node.rawsource], set(node['names'])
for sibling in node.traverse(include_self=False, descend=False,
siblings=True, ascend=False):
if CoqtopBlocksTransform.is_coqtop_block(sibling):
- self.merge_coqtop_classes(node, sibling)
+ CoqtopBlocksTransform.merge_coqtop_classes(node, sibling)
+ rawsources.append(sibling.rawsource)
+ names.update(sibling['names'])
node.extend(sibling.children)
node.parent.remove(sibling)
sibling.parent = None
else:
break
+ node.rawsource = "\n\n".join(rawsources)
+ node['names'] = list(names)
def apply(self):
self.add_coqtop_output()
- self.merge_consecutive_coqtop_blocks()
class CoqSubdomainsIndex(Index):
"""Index subclass to provide subdomain-specific indices.
@@ -616,7 +929,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)
@@ -638,19 +951,14 @@ 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"]
+ name, localname, shortname, subdomains = "optindex", "Flags, options and Tables Index", "options", ["flag", "opt", "table"]
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"]
@@ -668,10 +976,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
@@ -684,6 +1000,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.
@@ -706,10 +1024,11 @@ 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'),
+ 'flag': ObjType('flag', 'flag'),
+ 'table': ObjType('table', 'table'),
'thm': ObjType('thm', 'thm'),
'prodn': ObjType('prodn', 'prodn'),
'exn': ObjType('exn', 'exn'),
@@ -723,10 +1042,11 @@ class CoqDomain(Domain):
# the same role.
'cmd': VernacObject,
'cmdv': VernacVariantObject,
- 'tac': TacticObject,
'tacn': TacticNotationObject,
'tacv': TacticNotationVariantObject,
'opt': OptionObject,
+ 'flag': FlagObject,
+ 'table': TableObject,
'thm': GallinaObject,
'prodn' : ProductionObject,
'exn': ExceptionObject,
@@ -735,26 +1055,23 @@ class CoqDomain(Domain):
roles = {
# Each of these roles lives in a different semantic “subdomain”
- 'cmd': XRefRole(),
- 'tac': XRefRole(),
- 'tacn': XRefRole(),
- 'opt': XRefRole(),
- 'thm': XRefRole(),
- 'prodn' : XRefRole(),
- 'exn': XRefRole(),
- 'warn': XRefRole(),
+ 'cmd': XRefRole(warn_dangling=True),
+ 'tacn': XRefRole(warn_dangling=True),
+ 'opt': XRefRole(warn_dangling=True),
+ 'flag': XRefRole(warn_dangling=True),
+ 'table': XRefRole(warn_dangling=True),
+ 'thm': XRefRole(warn_dangling=True),
+ 'prodn' : XRefRole(warn_dangling=True),
+ 'exn': XRefRole(warn_dangling=True),
+ 'warn': XRefRole(warn_dangling=True),
# 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]
+ indices = [CoqVernacIndex, CoqTacticIndex, CoqOptionIndex, CoqGallinaIndex, CoqExceptionIndex]
data_version = 1
initial_data = {
@@ -762,9 +1079,10 @@ class CoqDomain(Domain):
# others, such as “version”
'objects' : { # subdomain → name → docname, objtype, targetid
'cmd': {},
- 'tac': {},
'tacn': {},
'opt': {},
+ 'flag': {},
+ 'table': {},
'thm': {},
'prodn' : {},
'exn': {},
@@ -827,35 +1145,43 @@ def simplify_source_code_blocks_for_latex(app, doctree, fromdocname): # pylint:
pygments if available. This prevents the LaTeX builder from getting
confused.
"""
-
is_html = app.builder.tags.has("html")
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"""
# 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
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)
+ app.connect('doctree-resolved', CoqtopBlocksTransform.merge_consecutive_coqtop_blocks)
# Add extra styles
app.add_stylesheet("fonts.css")
@@ -865,4 +1191,14 @@ def setup(app):
app.add_stylesheet("notations.css")
app.add_stylesheet("pre-text.css")
- return {'version': '0.1', "parallel_read_safe": True}
+ # Tell Sphinx about extra settings
+ app.add_config_value("report_undocumented_coq_objects", None, 'env')
+
+ # ``env_version`` is used by Sphinx to know when to invalidate
+ # coqdomain-specific bits in its caches. It should be incremented when the
+ # contents of ``env.domaindata['coq']`` change. See
+ # `https://github.com/sphinx-doc/sphinx/issues/4460`.
+ meta = { "version": "0.1",
+ "env_version": 2,
+ "parallel_read_safe": True }
+ return meta
diff --git a/doc/tools/coqrst/notations/CoqNotations.ttf b/doc/tools/coqrst/notations/CoqNotations.ttf
new file mode 100644
index 0000000000..da8f2850df
--- /dev/null
+++ b/doc/tools/coqrst/notations/CoqNotations.ttf
Binary files differ
diff --git a/doc/tools/coqrst/notations/TacticNotations.g b/doc/tools/coqrst/notations/TacticNotations.g
index 5176c51d28..a889ebda7b 100644
--- a/doc/tools/coqrst/notations/TacticNotations.g
+++ b/doc/tools/coqrst/notations/TacticNotations.g
@@ -20,13 +20,14 @@ repeat: LGROUP (ATOM)? WHITESPACE blocks (WHITESPACE)? RBRACE;
curlies: LBRACE (whitespace)? blocks (whitespace)? RBRACE;
whitespace: WHITESPACE;
meta: METACHAR;
-atomic: ATOM;
-hole: ID;
+atomic: ATOM (SUB)?;
+hole: ID (SUB)?;
LGROUP: '{' [+*?];
LBRACE: '{';
RBRACE: '}';
-METACHAR: '%' [|()];
-ATOM: '@' | ~[@{} ]+;
-ID: '@' [a-zA-Z0-9_]+;
+METACHAR: '%' [|(){}];
+ATOM: '@' | '_' | ~[@_{} ]+;
+ID: '@' ('_'? [a-zA-Z0-9])+;
+SUB: '_' '_' [a-zA-Z0-9]+;
WHITESPACE: ' '+;
diff --git a/doc/tools/coqrst/notations/TacticNotations.tokens b/doc/tools/coqrst/notations/TacticNotations.tokens
index 76ed2b065b..88b38f97a6 100644
--- a/doc/tools/coqrst/notations/TacticNotations.tokens
+++ b/doc/tools/coqrst/notations/TacticNotations.tokens
@@ -4,6 +4,7 @@ RBRACE=3
METACHAR=4
ATOM=5
ID=6
-WHITESPACE=7
+SUB=7
+WHITESPACE=8
'{'=2
'}'=3
diff --git a/doc/tools/coqrst/notations/TacticNotationsLexer.py b/doc/tools/coqrst/notations/TacticNotationsLexer.py
index ffa774b9ba..27293e7e09 100644
--- a/doc/tools/coqrst/notations/TacticNotationsLexer.py
+++ b/doc/tools/coqrst/notations/TacticNotationsLexer.py
@@ -7,24 +7,28 @@ import sys
def serializedATN():
with StringIO() as buf:
- buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2\t")
- buf.write(".\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7")
- buf.write("\4\b\t\b\3\2\3\2\3\2\3\3\3\3\3\4\3\4\3\5\3\5\3\5\3\6\3")
- buf.write("\6\6\6\36\n\6\r\6\16\6\37\5\6\"\n\6\3\7\3\7\6\7&\n\7\r")
- buf.write("\7\16\7\'\3\b\6\b+\n\b\r\b\16\b,\2\2\t\3\3\5\4\7\5\t\6")
- buf.write("\13\7\r\b\17\t\3\2\6\4\2,-AA\4\2*+~~\6\2\"\"BB}}\177\177")
- buf.write("\6\2\62;C\\aac|\2\61\2\3\3\2\2\2\2\5\3\2\2\2\2\7\3\2\2")
- buf.write("\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r\3\2\2\2\2\17\3\2\2\2\3")
- buf.write("\21\3\2\2\2\5\24\3\2\2\2\7\26\3\2\2\2\t\30\3\2\2\2\13")
- buf.write("!\3\2\2\2\r#\3\2\2\2\17*\3\2\2\2\21\22\7}\2\2\22\23\t")
- buf.write("\2\2\2\23\4\3\2\2\2\24\25\7}\2\2\25\6\3\2\2\2\26\27\7")
- buf.write("\177\2\2\27\b\3\2\2\2\30\31\7\'\2\2\31\32\t\3\2\2\32\n")
- buf.write("\3\2\2\2\33\"\7B\2\2\34\36\n\4\2\2\35\34\3\2\2\2\36\37")
- buf.write("\3\2\2\2\37\35\3\2\2\2\37 \3\2\2\2 \"\3\2\2\2!\33\3\2")
- buf.write("\2\2!\35\3\2\2\2\"\f\3\2\2\2#%\7B\2\2$&\t\5\2\2%$\3\2")
- buf.write("\2\2&\'\3\2\2\2\'%\3\2\2\2\'(\3\2\2\2(\16\3\2\2\2)+\7")
- buf.write("\"\2\2*)\3\2\2\2+,\3\2\2\2,*\3\2\2\2,-\3\2\2\2-\20\3\2")
- buf.write("\2\2\7\2\37!\',\2")
+ buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2\n")
+ buf.write(":\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7")
+ buf.write("\4\b\t\b\4\t\t\t\3\2\3\2\3\2\3\3\3\3\3\4\3\4\3\5\3\5\3")
+ buf.write("\5\3\6\3\6\6\6 \n\6\r\6\16\6!\5\6$\n\6\3\7\3\7\5\7(\n")
+ buf.write("\7\3\7\6\7+\n\7\r\7\16\7,\3\b\3\b\3\b\6\b\62\n\b\r\b\16")
+ buf.write("\b\63\3\t\6\t\67\n\t\r\t\16\t8\2\2\n\3\3\5\4\7\5\t\6\13")
+ buf.write("\7\r\b\17\t\21\n\3\2\7\4\2,-AA\4\2*+}\177\4\2BBaa\7\2")
+ buf.write("\"\"BBaa}}\177\177\5\2\62;C\\c|\2?\2\3\3\2\2\2\2\5\3\2")
+ buf.write("\2\2\2\7\3\2\2\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r\3\2\2\2")
+ buf.write("\2\17\3\2\2\2\2\21\3\2\2\2\3\23\3\2\2\2\5\26\3\2\2\2\7")
+ buf.write("\30\3\2\2\2\t\32\3\2\2\2\13#\3\2\2\2\r%\3\2\2\2\17.\3")
+ buf.write("\2\2\2\21\66\3\2\2\2\23\24\7}\2\2\24\25\t\2\2\2\25\4\3")
+ buf.write("\2\2\2\26\27\7}\2\2\27\6\3\2\2\2\30\31\7\177\2\2\31\b")
+ buf.write("\3\2\2\2\32\33\7\'\2\2\33\34\t\3\2\2\34\n\3\2\2\2\35$")
+ buf.write("\t\4\2\2\36 \n\5\2\2\37\36\3\2\2\2 !\3\2\2\2!\37\3\2\2")
+ buf.write("\2!\"\3\2\2\2\"$\3\2\2\2#\35\3\2\2\2#\37\3\2\2\2$\f\3")
+ buf.write("\2\2\2%*\7B\2\2&(\7a\2\2\'&\3\2\2\2\'(\3\2\2\2()\3\2\2")
+ buf.write("\2)+\t\6\2\2*\'\3\2\2\2+,\3\2\2\2,*\3\2\2\2,-\3\2\2\2")
+ buf.write("-\16\3\2\2\2./\7a\2\2/\61\7a\2\2\60\62\t\6\2\2\61\60\3")
+ buf.write("\2\2\2\62\63\3\2\2\2\63\61\3\2\2\2\63\64\3\2\2\2\64\20")
+ buf.write("\3\2\2\2\65\67\7\"\2\2\66\65\3\2\2\2\678\3\2\2\28\66\3")
+ buf.write("\2\2\289\3\2\2\29\22\3\2\2\2\t\2!#\',\638\2")
return buf.getvalue()
@@ -40,7 +44,8 @@ class TacticNotationsLexer(Lexer):
METACHAR = 4
ATOM = 5
ID = 6
- WHITESPACE = 7
+ SUB = 7
+ WHITESPACE = 8
channelNames = [ u"DEFAULT_TOKEN_CHANNEL", u"HIDDEN" ]
@@ -50,10 +55,11 @@ class TacticNotationsLexer(Lexer):
"'{'", "'}'" ]
symbolicNames = [ "<INVALID>",
- "LGROUP", "LBRACE", "RBRACE", "METACHAR", "ATOM", "ID", "WHITESPACE" ]
+ "LGROUP", "LBRACE", "RBRACE", "METACHAR", "ATOM", "ID", "SUB",
+ "WHITESPACE" ]
ruleNames = [ "LGROUP", "LBRACE", "RBRACE", "METACHAR", "ATOM", "ID",
- "WHITESPACE" ]
+ "SUB", "WHITESPACE" ]
grammarFileName = "TacticNotations.g"
diff --git a/doc/tools/coqrst/notations/TacticNotationsLexer.tokens b/doc/tools/coqrst/notations/TacticNotationsLexer.tokens
index 76ed2b065b..88b38f97a6 100644
--- a/doc/tools/coqrst/notations/TacticNotationsLexer.tokens
+++ b/doc/tools/coqrst/notations/TacticNotationsLexer.tokens
@@ -4,6 +4,7 @@ RBRACE=3
METACHAR=4
ATOM=5
ID=6
-WHITESPACE=7
+SUB=7
+WHITESPACE=8
'{'=2
'}'=3
diff --git a/doc/tools/coqrst/notations/TacticNotationsParser.py b/doc/tools/coqrst/notations/TacticNotationsParser.py
index c7e28af52b..645f078979 100644
--- a/doc/tools/coqrst/notations/TacticNotationsParser.py
+++ b/doc/tools/coqrst/notations/TacticNotationsParser.py
@@ -7,29 +7,31 @@ import sys
def serializedATN():
with StringIO() as buf:
- buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\3\t")
- buf.write("F\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7\4\b")
+ buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\3\n")
+ buf.write("J\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7\4\b")
buf.write("\t\b\4\t\t\t\4\n\t\n\3\2\3\2\3\2\3\3\3\3\5\3\32\n\3\3")
buf.write("\3\7\3\35\n\3\f\3\16\3 \13\3\3\4\3\4\3\4\3\4\3\4\5\4\'")
buf.write("\n\4\3\5\3\5\5\5+\n\5\3\5\3\5\3\5\5\5\60\n\5\3\5\3\5\3")
buf.write("\6\3\6\5\6\66\n\6\3\6\3\6\5\6:\n\6\3\6\3\6\3\7\3\7\3\b")
- buf.write("\3\b\3\t\3\t\3\n\3\n\3\n\2\2\13\2\4\6\b\n\f\16\20\22\2")
- buf.write("\2\2F\2\24\3\2\2\2\4\27\3\2\2\2\6&\3\2\2\2\b(\3\2\2\2")
- buf.write("\n\63\3\2\2\2\f=\3\2\2\2\16?\3\2\2\2\20A\3\2\2\2\22C\3")
- buf.write("\2\2\2\24\25\5\4\3\2\25\26\7\2\2\3\26\3\3\2\2\2\27\36")
- buf.write("\5\6\4\2\30\32\5\f\7\2\31\30\3\2\2\2\31\32\3\2\2\2\32")
- buf.write("\33\3\2\2\2\33\35\5\6\4\2\34\31\3\2\2\2\35 \3\2\2\2\36")
- buf.write("\34\3\2\2\2\36\37\3\2\2\2\37\5\3\2\2\2 \36\3\2\2\2!\'")
- buf.write("\5\20\t\2\"\'\5\16\b\2#\'\5\22\n\2$\'\5\b\5\2%\'\5\n\6")
- buf.write("\2&!\3\2\2\2&\"\3\2\2\2&#\3\2\2\2&$\3\2\2\2&%\3\2\2\2")
- buf.write("\'\7\3\2\2\2(*\7\3\2\2)+\7\7\2\2*)\3\2\2\2*+\3\2\2\2+")
- buf.write(",\3\2\2\2,-\7\t\2\2-/\5\4\3\2.\60\7\t\2\2/.\3\2\2\2/\60")
- buf.write("\3\2\2\2\60\61\3\2\2\2\61\62\7\5\2\2\62\t\3\2\2\2\63\65")
- buf.write("\7\4\2\2\64\66\5\f\7\2\65\64\3\2\2\2\65\66\3\2\2\2\66")
- buf.write("\67\3\2\2\2\679\5\4\3\28:\5\f\7\298\3\2\2\29:\3\2\2\2")
- buf.write(":;\3\2\2\2;<\7\5\2\2<\13\3\2\2\2=>\7\t\2\2>\r\3\2\2\2")
- buf.write("?@\7\6\2\2@\17\3\2\2\2AB\7\7\2\2B\21\3\2\2\2CD\7\b\2\2")
- buf.write("D\23\3\2\2\2\t\31\36&*/\659")
+ buf.write("\3\b\3\t\3\t\5\tD\n\t\3\n\3\n\5\nH\n\n\3\n\2\2\13\2\4")
+ buf.write("\6\b\n\f\16\20\22\2\2\2L\2\24\3\2\2\2\4\27\3\2\2\2\6&")
+ buf.write("\3\2\2\2\b(\3\2\2\2\n\63\3\2\2\2\f=\3\2\2\2\16?\3\2\2")
+ buf.write("\2\20A\3\2\2\2\22E\3\2\2\2\24\25\5\4\3\2\25\26\7\2\2\3")
+ buf.write("\26\3\3\2\2\2\27\36\5\6\4\2\30\32\5\f\7\2\31\30\3\2\2")
+ buf.write("\2\31\32\3\2\2\2\32\33\3\2\2\2\33\35\5\6\4\2\34\31\3\2")
+ buf.write("\2\2\35 \3\2\2\2\36\34\3\2\2\2\36\37\3\2\2\2\37\5\3\2")
+ buf.write("\2\2 \36\3\2\2\2!\'\5\20\t\2\"\'\5\16\b\2#\'\5\22\n\2")
+ buf.write("$\'\5\b\5\2%\'\5\n\6\2&!\3\2\2\2&\"\3\2\2\2&#\3\2\2\2")
+ buf.write("&$\3\2\2\2&%\3\2\2\2\'\7\3\2\2\2(*\7\3\2\2)+\7\7\2\2*")
+ buf.write(")\3\2\2\2*+\3\2\2\2+,\3\2\2\2,-\7\n\2\2-/\5\4\3\2.\60")
+ buf.write("\7\n\2\2/.\3\2\2\2/\60\3\2\2\2\60\61\3\2\2\2\61\62\7\5")
+ buf.write("\2\2\62\t\3\2\2\2\63\65\7\4\2\2\64\66\5\f\7\2\65\64\3")
+ buf.write("\2\2\2\65\66\3\2\2\2\66\67\3\2\2\2\679\5\4\3\28:\5\f\7")
+ buf.write("\298\3\2\2\29:\3\2\2\2:;\3\2\2\2;<\7\5\2\2<\13\3\2\2\2")
+ buf.write("=>\7\n\2\2>\r\3\2\2\2?@\7\6\2\2@\17\3\2\2\2AC\7\7\2\2")
+ buf.write("BD\7\t\2\2CB\3\2\2\2CD\3\2\2\2D\21\3\2\2\2EG\7\b\2\2F")
+ buf.write("H\7\t\2\2GF\3\2\2\2GH\3\2\2\2H\23\3\2\2\2\13\31\36&*/")
+ buf.write("\659CG")
return buf.getvalue()
@@ -46,7 +48,7 @@ class TacticNotationsParser ( Parser ):
literalNames = [ "<INVALID>", "<INVALID>", "'{'", "'}'" ]
symbolicNames = [ "<INVALID>", "LGROUP", "LBRACE", "RBRACE", "METACHAR",
- "ATOM", "ID", "WHITESPACE" ]
+ "ATOM", "ID", "SUB", "WHITESPACE" ]
RULE_top = 0
RULE_blocks = 1
@@ -68,7 +70,8 @@ class TacticNotationsParser ( Parser ):
METACHAR=4
ATOM=5
ID=6
- WHITESPACE=7
+ SUB=7
+ WHITESPACE=8
def __init__(self, input:TokenStream, output:TextIO = sys.stdout):
super().__init__(input, output)
@@ -502,6 +505,9 @@ class TacticNotationsParser ( Parser ):
def ATOM(self):
return self.getToken(TacticNotationsParser.ATOM, 0)
+ def SUB(self):
+ return self.getToken(TacticNotationsParser.SUB, 0)
+
def getRuleIndex(self):
return TacticNotationsParser.RULE_atomic
@@ -518,10 +524,19 @@ class TacticNotationsParser ( Parser ):
localctx = TacticNotationsParser.AtomicContext(self, self._ctx, self.state)
self.enterRule(localctx, 14, self.RULE_atomic)
+ self._la = 0 # Token type
try:
self.enterOuterAlt(localctx, 1)
self.state = 63
self.match(TacticNotationsParser.ATOM)
+ self.state = 65
+ self._errHandler.sync(self)
+ _la = self._input.LA(1)
+ if _la==TacticNotationsParser.SUB:
+ self.state = 64
+ self.match(TacticNotationsParser.SUB)
+
+
except RecognitionException as re:
localctx.exception = re
self._errHandler.reportError(self, re)
@@ -539,6 +554,9 @@ class TacticNotationsParser ( Parser ):
def ID(self):
return self.getToken(TacticNotationsParser.ID, 0)
+ def SUB(self):
+ return self.getToken(TacticNotationsParser.SUB, 0)
+
def getRuleIndex(self):
return TacticNotationsParser.RULE_hole
@@ -555,10 +573,19 @@ class TacticNotationsParser ( Parser ):
localctx = TacticNotationsParser.HoleContext(self, self._ctx, self.state)
self.enterRule(localctx, 16, self.RULE_hole)
+ self._la = 0 # Token type
try:
self.enterOuterAlt(localctx, 1)
- self.state = 65
+ self.state = 67
self.match(TacticNotationsParser.ID)
+ self.state = 69
+ self._errHandler.sync(self)
+ _la = self._input.LA(1)
+ if _la==TacticNotationsParser.SUB:
+ self.state = 68
+ self.match(TacticNotationsParser.SUB)
+
+
except RecognitionException as re:
localctx.exception = re
self._errHandler.reportError(self, re)
diff --git a/doc/tools/coqrst/notations/UbuntuMono-Square.ttf b/doc/tools/coqrst/notations/UbuntuMono-Square.ttf
deleted file mode 100644
index a53a9a0f03..0000000000
--- a/doc/tools/coqrst/notations/UbuntuMono-Square.ttf
+++ /dev/null
Binary files differ
diff --git a/doc/tools/coqrst/notations/fontsupport.py b/doc/tools/coqrst/notations/fontsupport.py
index 3402ea2aaf..a3efd97f5b 100755
--- a/doc/tools/coqrst/notations/fontsupport.py
+++ b/doc/tools/coqrst/notations/fontsupport.py
@@ -63,8 +63,7 @@ def trim_font(fnt):
def center_glyphs(src_font_path, dst_font_path, dst_name):
fnt = trim_font(fontforge.open(src_font_path))
- size = max(max(g.width for g in fnt.glyphs()),
- max(glyph_height(g) for g in fnt.glyphs()))
+ size = max(g.width for g in fnt.glyphs())
fnt.ascent, fnt.descent = size, 0
for glyph in fnt.glyphs():
scale_single_glyph(glyph, size, size)
@@ -77,5 +76,5 @@ if __name__ == '__main__':
from os.path import dirname, join, abspath
curdir = dirname(abspath(__file__))
ubuntumono_path = join(curdir, "UbuntuMono-B.ttf")
- ubuntumono_mod_path = join(curdir, "UbuntuMono-Square.ttf")
- center_glyphs(ubuntumono_path, ubuntumono_mod_path, "UbuntuMono-Square")
+ ubuntumono_mod_path = join(curdir, "CoqNotations.ttf")
+ center_glyphs(ubuntumono_path, ubuntumono_mod_path, "CoqNotations")
diff --git a/doc/tools/coqrst/notations/html.py b/doc/tools/coqrst/notations/html.py
index 44212d7889..87a41cf9f3 100644
--- a/doc/tools/coqrst/notations/html.py
+++ b/doc/tools/coqrst/notations/html.py
@@ -41,9 +41,16 @@ class TacticNotationsToHTMLVisitor(TacticNotationsVisitor):
def visitHole(self, ctx:TacticNotationsParser.HoleContext):
tags.span(ctx.ID().getText()[1:], _class="hole")
+ sub = ctx.SUB()
+ if sub:
+ tags.sub(sub.getText()[1:])
def visitMeta(self, ctx:TacticNotationsParser.MetaContext):
- tags.span(ctx.METACHAR().getText()[1:], _class="meta")
+ txt = ctx.METACHAR().getText()[1:]
+ if (txt == "{") or (txt == "}"):
+ tags.span(txt)
+ else:
+ tags.span(txt, _class="meta")
def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext):
tags.span(" ") # TODO: no need for a <span> here
diff --git a/doc/tools/coqrst/notations/sphinx.py b/doc/tools/coqrst/notations/sphinx.py
index 26a5f69680..e05b834184 100644
--- a/doc/tools/coqrst/notations/sphinx.py
+++ b/doc/tools/coqrst/notations/sphinx.py
@@ -56,19 +56,36 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor):
def visitAtomic(self, ctx:TacticNotationsParser.AtomicContext):
atom = ctx.ATOM().getText()
- return [nodes.inline(atom, atom)]
+ sub = ctx.SUB()
+ node = nodes.inline(atom, atom)
+
+ if sub:
+ sub_index = sub.getText()[2:]
+ node += nodes.subscript(sub_index, sub_index)
+
+ return [node]
def visitHole(self, ctx:TacticNotationsParser.HoleContext):
hole = ctx.ID().getText()
token_name = hole[1:]
node = nodes.inline(hole, token_name, classes=["hole"])
+
+ sub = ctx.SUB()
+ if sub:
+ sub_index = sub.getText()[2:]
+ node += nodes.subscript(sub_index, sub_index)
+
return [addnodes.pending_xref(token_name, node, reftype='token', refdomain='std', reftarget=token_name)]
def visitMeta(self, ctx:TacticNotationsParser.MetaContext):
meta = ctx.METACHAR().getText()
metachar = meta[1:] # remove escape char
token_name = metachar
- return [nodes.inline(metachar, token_name, classes=["meta"])]
+ if (metachar == "{") or (metachar == "}"):
+ classes=[]
+ else:
+ classes=["meta"]
+ return [nodes.inline(metachar, token_name, classes=classes)]
def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext):
return [nodes.Text(" ")]
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..3ff00eaaf3 100644
--- a/doc/tools/coqrst/repl/coqtop.py
+++ b/doc/tools/coqrst/repl/coqtop.py
@@ -41,8 +41,13 @@ 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.args = (args or []) + ["-boot", "-color", "on"] * color
+ BOOT = True
+ if os.getenv('COQBOOT') == "no":
+ BOOT = False
+ 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"] * BOOT + ["-color", "on"] * color
self.coqtop = None
def __enter__(self):
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 14:01:44 +0000