Merge PR #12224: Support :gdef:`text<term>` syntax (adding "<term>")

Reviewed-by: Zimmi48
Reviewed-by: cpitclaudel

9 files changed, 43 insertions, 24 deletions

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 <https://github.com/coq/coq/pull/12224>`_,
+  by Jim Fehrle and Théo Zimmermann).
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 <term>` 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 <composite>` numbers are the non-prime numbers.
 
 Common mistakes
 ===============
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
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 <term>` 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 <witness>`.  Note that deciding
      whether a type is inhabited is `undecidable
      <https://en.wikipedia.org/wiki/Undecidable_problem>`_.
 
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 <sort>`.
 
 All sorts have a type and there is an infinite well-founded typing
 hierarchy of sorts whose base sorts are :math:`\SProp`, :math:`\Prop`
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 <term>` 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 <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)