Merge PR #7556: Add a setting to warn about empty object in the refman

5 files changed, 152 insertions, 3 deletions

diff --git a/Makefile.doc b/Makefile.doc
index 41ae11b86..4670c79ec 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -55,7 +55,7 @@ endif
 
 sphinx: $(SPHINX_DEPS)
 	$(SHOW)'SPHINXBUILD doc/sphinx'
-	$(HIDE)COQBIN="$(PWD)/bin" $(SPHINXBUILD) -W -b html $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/html
+	$(HIDE)COQBIN="$(abspath bin)" $(SPHINXBUILD) -W -b html $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/html
 	@echo
 	@echo "Build finished. The HTML pages are in $(SPHINXBUILDDIR)/html."
 
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 5f2f21f2b..3036fac81 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -22,6 +22,7 @@ Our Coq domain define multiple `objects`_.  Each object has a *signature* (think
       matching :n:`@pattern` in the current goal.
 
       .. exn:: Too few occurrences
+         :undocumented:
 
 Objects are automatically collected into indices, and can be linked to using the role version of the object's directive. For example, you could link to the tactic variant above using ``:tacv:`simpl_at```, and to its exception using ``:exn:`Too few occurrences```.
 
@@ -31,6 +32,8 @@ Names (link targets) are auto-generated for most simple objects, though they can
 - Vernacs (commands) have their name set to the first word of their signature.  For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```.
 - Vernac variants, tactic notations, and tactic variants do not have a default name.
 
+Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms).  Undocumented objects should have the `:undocumented:` flag instead, as shown above.
+
 Notations
 ---------
 
@@ -291,6 +294,64 @@ 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:`…```.
 
+Common mistakes
+===============
+
+Improper nesting
+----------------
+
+DO
+  .. code::
+
+     .. cmd:: Foo @bar
+
+        Foo the first instance of :token:`bar`\ s.
+
+        .. cmdv:: Foo All
+
+           Foo all the :token:`bar`\ s in
+           the current context
+
+DON'T
+  .. code::
+
+     .. cmd:: Foo @bar
+
+     Foo the first instance of :token:`bar`\ s.
+
+     .. cmdv:: Foo All
+
+     Foo all the :token:`bar`\ s in
+     the current context
+
+You can set the ``report_undocumented_coq_objects`` setting in ``conf.py`` to ``"info"`` or ``"warning"`` to get a list of all Coq objects without a description.
+
+Overusing ``:token:``
+---------------------
+
+DO
+  .. code::
+
+     This is equivalent to :n:`Axiom @ident : @term`.
+
+DON'T
+  .. code::
+
+     This is equivalent to ``Axiom`` :token`ident` : :token:`term`.
+
+Omitting annotations
+--------------------
+
+DO
+  .. code::
+
+     .. tacv:: assert @form as @intro_pattern
+
+DON'T
+  .. code::
+
+     .. tacv:: assert form as intro_pattern
+
 Tips and tricks
 ===============
 
diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst
index 203251abf..f90efa995 100644
--- a/doc/sphinx/README.template.rst
+++ b/doc/sphinx/README.template.rst
@@ -22,6 +22,7 @@ Our Coq domain define multiple `objects`_.  Each object has a *signature* (think
       matching :n:`@pattern` in the current goal.
 
       .. exn:: Too few occurrences
+         :undocumented:
 
 Objects are automatically collected into indices, and can be linked to using the role version of the object's directive. For example, you could link to the tactic variant above using ``:tacv:`simpl_at```, and to its exception using ``:exn:`Too few occurrences```.
 
@@ -31,6 +32,8 @@ Names (link targets) are auto-generated for most simple objects, though they can
 - Vernacs (commands) have their name set to the first word of their signature.  For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```.
 - Vernac variants, tactic notations, and tactic variants do not have a default name.
 
+Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms).  Undocumented objects should have the `:undocumented:` flag instead, as shown above.
+
 Notations
 ---------
 
@@ -83,6 +86,64 @@ In addition to the objects and directives above, the ``coqrst`` Sphinx plugin de
 
 [ROLES]
 
+Common mistakes
+===============
+
+Improper nesting
+----------------
+
+DO
+  .. code::
+
+     .. cmd:: Foo @bar
+
+        Foo the first instance of :token:`bar`\ s.
+
+        .. cmdv:: Foo All
+
+           Foo all the :token:`bar`\ s in
+           the current context
+
+DON'T
+  .. code::
+
+     .. cmd:: Foo @bar
+
+     Foo the first instance of :token:`bar`\ s.
+
+     .. cmdv:: Foo All
+
+     Foo all the :token:`bar`\ s in
+     the current context
+
+You can set the ``report_undocumented_coq_objects`` setting in ``conf.py`` to ``"info"`` or ``"warning"`` to get a list of all Coq objects without a description.
+
+Overusing ``:token:``
+---------------------
+
+DO
+  .. code::
+
+     This is equivalent to :n:`Axiom @ident : @term`.
+
+DON'T
+  .. code::
+
+     This is equivalent to ``Axiom`` :token`ident` : :token:`term`.
+
+Omitting annotations
+--------------------
+
+DO
+  .. code::
+
+     .. tacv:: assert @form as @intro_pattern
+
+DON'T
+  .. code::
+
+     .. tacv:: assert form as intro_pattern
+
 Tips and tricks
 ===============
 
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 1f7dd9d68..f65400e88 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -51,6 +51,10 @@ extensions = [
     'coqrst.coqdomain'
 ]
 
+# Change this to "info" or "warning" to get notifications about undocumented Coq
+# objects (objects with no contents).
+report_undocumented_coq_objects = None
+
 # Add any paths that contain templates here, relative to this directory.
 templates_path = ['_templates']
 
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 606d725bf..8d6e23764 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -97,8 +97,10 @@ 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
     }
 
     def _subdomain(self):
@@ -160,6 +162,24 @@ class CoqObject(ObjectDescription):
             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 run(self):
+        self._warn_if_undocumented()
+        return super().run()
+
 class PlainObject(CoqObject):
     """A base class for objects whose signatures should be rendered literally."""
     def _render_signature(self, signature, signode):
@@ -1036,4 +1056,7 @@ def setup(app):
     app.add_stylesheet("notations.css")
     app.add_stylesheet("pre-text.css")
 
+    # Tell Sphinx about extra settings
+    app.add_config_value("report_undocumented_coq_objects", None, 'env')
+
     return {'version': '0.1', "parallel_read_safe": True}