From 7cac115647723f8261b7aabf8094572227b25c43 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 18 May 2020 18:55:59 +0200 Subject: Bump minimal versions of refman dependencies. Fixes #11936. Co-authored-by: Jim Fehrle --- .gitlab-ci.yml | 2 +- dev/ci/docker/bionic_coq/Dockerfile | 7 ++++--- doc/README.md | 8 ++++---- .../11-infrastructure-and-dependencies/12224-gdef_alias.rst | 6 ++++++ doc/sphinx/conf.py | 2 +- 5 files changed, 16 insertions(+), 9 deletions(-) create mode 100644 doc/changelog/11-infrastructure-and-dependencies/12224-gdef_alias.rst diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index f26804e120..fc0cdebcf0 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -18,7 +18,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2020-05-06-V70" + CACHEKEY: "bionic_coq-V2020-05-18-V3" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 9ee6496ee5..51a602303a 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2020-05-06-V70" +# CACHEKEY: "bionic_coq-V2020-05-18-V3" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -14,12 +14,13 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ # Dependencies of stdlib and sphinx doc texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \ xindy python3-pip python3-setuptools python3-pexpect python3-bs4 \ + fonts-freefont-otf \ # Dependencies of source-doc and coq-makefile texlive-science tipa # More dependencies of the sphinx doc -RUN pip3 install sphinx==1.8.0 sphinx_rtd_theme==0.2.5b2 \ - antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0 +RUN pip3 install sphinx==2.3.1 sphinx_rtd_theme==0.4.3 \ + antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.2 # We need to install OPAM 2.0 manually for now. RUN wget https://github.com/ocaml/opam/releases/download/2.0.6/opam-2.0.6-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam diff --git a/doc/README.md b/doc/README.md index e749bcf5d1..8e1bc85c49 100644 --- a/doc/README.md +++ b/doc/README.md @@ -30,12 +30,12 @@ To produce the complete documentation in HTML, you will need Coq dependencies listed in [`INSTALL.md`](../INSTALL.md). Additionally, the Sphinx-based reference manual requires Python 3, and the following Python packages: - - sphinx >= 1.8.0 - - sphinx_rtd_theme >= 0.2.5b2 + - sphinx >= 2.3.1 + - sphinx_rtd_theme >= 0.4.3 - beautifulsoup4 >= 4.0.6 - antlr4-python3-runtime >= 4.7.1 - pexpect >= 4.2.1 - - sphinxcontrib-bibtex >= 0.4.0 + - sphinxcontrib-bibtex >= 0.4.2 To install them, you should first install pip and setuptools (for instance, with `apt install python3-pip python3-setuptools` on Debian / Ubuntu) then run: @@ -68,7 +68,7 @@ install them with: Or if you want to use less disk space: apt install texlive-latex-extra texlive-fonts-recommended texlive-xetex \ - latexmk xindy + latexmk xindy fonts-freefont-otf Compilation ----------- diff --git a/doc/changelog/11-infrastructure-and-dependencies/12224-gdef_alias.rst b/doc/changelog/11-infrastructure-and-dependencies/12224-gdef_alias.rst new file mode 100644 index 0000000000..35a618ea8d --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/12224-gdef_alias.rst @@ -0,0 +1,6 @@ +- **Changed:** + Minimal versions of dependencies for building the reference manual: + now requires Sphinx 2.3.1+, sphinx_rtd_theme 0.4.3+ and + sphinxcontrib-bibtex 0.4.2+ + (`#12224 `_, + by Jim Fehrle and Théo Zimmermann). diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 4136b406de..fabf7a519f 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -46,7 +46,7 @@ with open("refman-preamble.rst") as s: # -- General configuration ------------------------------------------------ # If your documentation needs a minimal Sphinx version, state it here. -needs_sphinx = '1.8.0' +needs_sphinx = '2.3.1' # Add any Sphinx extension module names here, as strings. They can be # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom -- cgit v1.2.3 From ae208f062d15773781cb600e9a7b2c44de25caf9 Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Thu, 30 Apr 2020 16:51:08 -0700 Subject: Support :gdef:`text ` syntax (adding "") --- doc/sphinx/README.rst | 7 +++++-- doc/tools/coqrst/coqdomain.py | 31 ++++++++++++++++++++----------- 2 files changed, 25 insertions(+), 13 deletions(-) diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index e20469bb8b..f91874d74d 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -359,11 +359,14 @@ In addition to the objects and directives above, the ``coqrst`` Sphinx plugin de and reference its tokens using ``:token:`…```. ``:gdef:`` Marks the definition of a glossary term inline in the text. Matching :term:`XXX` - constructs will link to it. The term will also appear in the Glossary Index. + constructs will link to it. Use the form :gdef:`text ` to display "text" + for the definition of "term", such as when "term" must be capitalized or plural + for grammatical reasons. The term will also appear in the Glossary Index. - Example:: + Examples:: A :gdef:`prime` number is divisible only by itself and 1. + :gdef:`Composite ` numbers are the non-prime numbers. Common mistakes =============== diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index df11960403..e59f694aa7 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -27,13 +27,13 @@ from docutils.parsers.rst.roles import code_role #, set_classes 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, get_node_location from sphinx.directives import ObjectDescription from sphinx.domains import Domain, ObjType, Index -from sphinx.domains.std import token_xrefs +from sphinx.errors import ExtensionError +from sphinx.roles import XRefRole +from sphinx.util.docutils import ReferenceRole +from sphinx.util.logging import getLogger, get_node_location +from sphinx.util.nodes import set_source_info, set_role_source_info, make_refnode from . import coqdoc from .repl import ansicolors @@ -1162,25 +1162,34 @@ GrammarProductionRole.role_name = "production" def GlossaryDefRole(typ, rawtext, text, lineno, inliner, options={}, content=[]): """Marks the definition of a glossary term inline in the text. Matching :term:`XXX` - constructs will link to it. The term will also appear in the Glossary Index. + constructs will link to it. Use the form :gdef:`text ` to display "text" + for the definition of "term", such as when "term" must be capitalized or plural + for grammatical reasons. The term will also appear in the Glossary Index. - Example:: + Examples:: A :gdef:`prime` number is divisible only by itself and 1. + :gdef:`Composite ` numbers are the non-prime numbers. """ #pylint: disable=dangerous-default-value, unused-argument env = inliner.document.settings.env std = env.domaindata['std']['objects'] - key = ('term', text) + m = ReferenceRole.explicit_title_re.match(text) + if m: + (text, term) = m.groups() + text = text.strip() + else: + term = text + key = ('term', term) if key in std: MSG = 'Duplicate object: {}; other is at {}' - msg = MSG.format(text, env.doc2path(std[key][0])) + msg = MSG.format(term, env.doc2path(std[key][0])) inliner.document.reporter.warning(msg, line=lineno) - targetid = nodes.make_id('term-{}'.format(text)) + targetid = nodes.make_id('term-{}'.format(term)) std[key] = (env.docname, targetid) - target = nodes.target('', '', ids=[targetid], names=[text]) + target = nodes.target('', '', ids=[targetid], names=[term]) inliner.document.note_explicit_target(target) node = nodes.inline(rawtext, '', target, nodes.Text(text), classes=['term-defn']) set_role_source_info(inliner, lineno, node) -- cgit v1.2.3 From c1125bda507137c35400808c6de19acfcece0ec7 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Sat, 16 May 2020 16:19:59 +0200 Subject: Use the new gdef alt-text feature in the refman. --- doc/sphinx/language/core/basic.rst | 2 +- doc/sphinx/language/core/sorts.rst | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 250a0f0326..68900aa0be 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -267,7 +267,7 @@ rest of the |Coq| manual: :term:`terms ` and :term:`types Intuitively, types may be viewed as sets containing terms. We say that a type is :gdef:`inhabited` if it contains at least one term (i.e. if we can find a term which is associated with this - type). We call such terms :gdef:`witness`\es. Note that deciding + type). We call such terms :gdef:`witnesses `. Note that deciding whether a type is inhabited is `undecidable `_. diff --git a/doc/sphinx/language/core/sorts.rst b/doc/sphinx/language/core/sorts.rst index 8307a02d6d..03581b95dd 100644 --- a/doc/sphinx/language/core/sorts.rst +++ b/doc/sphinx/language/core/sorts.rst @@ -22,7 +22,7 @@ Sorts | @universe_expr universe_expr ::= @universe_name {? + @num } -The types of types are called :gdef:`sort`\s. +The types of types are called :gdef:`sorts `. All sorts have a type and there is an infinite well-founded typing hierarchy of sorts whose base sorts are :math:`\SProp`, :math:`\Prop` -- cgit v1.2.3