Support in-line glossary definitions and references with an index

[jfehrle]

Here's an alternate implementation of a glossary. This has inline definitions (:gdef:) showing in italic and references (:gref:) and a Glossary Page index. An alternative to #12114. Look at the beginning of the implicit arguments section of the Gallina extensions chapter. And the new index.

What do you think?

[Zimmi48]

I like the result but I'm a bit uncomfortable reinventing an existing feature rather than just extending it. Wouldn't there be a way to get the same result but by piggy-backing on the current glossary infrastructure (in particular reusing :term: instead of :gref:) like prodn and :n: piggy-back on the existing token mechanism (so that :production: and :token: remain available and compatible)?

Ultimately this is more the area of expertise of @cpitclaudel than mine.

[cpitclaudel]

The implementation looks reasonable, but I would have reused the existing glossary objects; basically you want to define glossary entries inline, right?

[Zimmi48]

The implementation looks reasonable, but I would have reused the existing glossary objects; basically you want to define glossary entries inline, right?

AFAIU, that + a specific index of glossary objects.

[jfehrle]

It's easy to switch to using :term: instead of :gref:.

I'd like to generate the glossary index using data from the std domain instead of coq so that entries defined in glossary directives will also appear in the index. However, I'm having trouble figuring out a clean way to get access to document or env in CoqSubdomainsIndex.generate. Any ideas for a clean way I can access one of those?

For consistency, I think it makes more sense to have the glossary index defined in the coq domain rather then std even if the data comes from std.

Also FWIW note that the general index (coming from std) is formatted differently and in some ways better than the other indexes. Might be nice to eventually apply the general index format to the others.

[jfehrle]

Updated.

[jfehrle]

Not sure why saved_env is None in the build contrary to the message it prints. It works fine locally for HTML. Could Dune be doing the build with multiple processes? I don't recall if the pdf build worked for the prior version of the code. Any suggestions?

[Zimmi48]

For the record, the build succeeded with Dune and failed with make. Parallel builds have been disabled for the documentation with both build systems.

[Zimmi48]

@cpitclaudel Can you be the assignee for this PR?

[jfehrle]

This version works. I tried to avoid the global by adding env as a argument to CoqSubdomainsIndex.__init__, but the object is constructed in the Sphinx code where I can't add an argument.

I'll squash and remove the implicit-arguments.rst changes later.

[jfehrle]

The implementation looks reasonable, but I would have reused the existing glossary objects; basically you want to define glossary entries inline, right?

AFAIU, that + a specific index of glossary objects.

That's correct.

[jfehrle]

Changed the global to a static field of CoqDomain. A bit cleaner.

[Zimmi48]

@jfehrle The output contains a bunch of warnings that were not there before:

The iterable returned by Node.traverse() will become an iterator instead of a list in
Docutils > 0.16.

RemovedInSphinx20Warning: app.info() is now deprecated. Use sphinx.util.logging instead.

[jfehrle]

I don't see these messages locally when I build using make. I do see them in the dune:refman job for this PR, but I also see them in that job for #11718, which has no significant changes to .py files though a minor change to conf.py (removing a few items from nitpick_ignore). So looks like these messages are not specific to this PR.

Seems like the most likely explanation is a change in docutils, perhaps in Sphinx and/or Sphinx parameters.

A few other thoughts toward understanding the Node.traverse() messages: Clearly the message is from docutils. I see for classifier in reversed(node.parent.traverse(nodes.classifier)): in the routine apply_source_workaround in util/nodes.py but on line 151, not line 94 in my docutils version 0.15.2. This is in the function apply_source_workaround that's called from ApplySourceWorkaround.apply. That class is called by setup in sphinx/transforms/__init__.py: app.add_transform(ApplySourceWorkaround)`.

AFAICT it's not something we can fix by changing the Python code in our source tree.

[Zimmi48]

OK sorry for the false alarm.

[Zimmi48]

ping @cpitclaudel: I feel like you are much more qualified than I am to review this PR.

[cpitclaudel]

OK, I'll read through it today or tomorrow, I hope.

[jfehrle]

@cpitclaudel I'll need to make a 1-2 line fix to support cross-file hyperlinks for terms with spaces in them. Just need to map the space to something else, like a dash.

[cpitclaudel]

@cpitclaudel I'll need to make a 1-2 line fix to support cross-file hyperlinks for terms with spaces in them. Just need to map the space to something else, like a dash.

Doesn't the standard Sphinx url escaping do this?

[jfehrle]

Doesn't the standard Sphinx url escaping do this?

Actually doesn't matter; the link names Sphinx generates for a :term: substitute dashes for spaces. If we want them to find our :gdef: definitions then gdef has to do this as well.

It's a one line fix. Squashed, removed the examples in the rst files and updated.

[Zimmi48]

@jfehrle You need to apply this patch:

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 0802b5d0b4..e20469bb8b 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -358,6 +358,13 @@ In addition to the objects and directives above, the ``coqrst`` Sphinx plugin de
     <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_
     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.
+
+    Example::
+
+       A :gdef:`prime` number is divisible only by itself and 1.
+
 Common mistakes
 ===============

[jfehrle]

@Zimmi48 Yeah, I removed too much last night, thanks. But it was easier to use doc/tools/coqrst/regen_readme.py, I've not applied patches before.

Updated.

[cpitclaudel]

Looks good. I just have one doubt about capturing env and adding the glossary as an index of the Coq domain.

[cpitclaudel]

Actually doesn't matter; the link names Sphinx generates for a :term: substitute dashes for spaces. If we want them to find our :gdef: definitions then gdef has to do this as well. It's a one line fix. Squashed, removed the examples in the rst files and updated.

I expect Sphinx uses nodes.make_id internally, and that's what we should do to (it escapes more than spaces)

[jfehrle]

Updated.

[cpitclaudel]

Thanks, looks great this way. Should I merge?

[Zimmi48]

I think so, and this will allow me to not depend on any other PR in #12172.