feat: Added possibility for shared numbering of theorems. (#164)

douden · Ljon4ik4 · web-flow · commit 27f52c699d4f · 2026-01-24T23:47:14.000+01:00
* feat: Added possibility for shared numbering of theorems, fixing issue #64 (#161) Added optioin to have directives share numbering. Reflected also in docs. * Add config validation Introduces a check_config_values function to validate Sphinx configuration values at runtime, ensuring correct types and defaults for proof-related settings. --------- Co-authored-by: Leonid Ryvkin <ryvkin@gmx.com>
diff --git a/docs/source/conf.py b/docs/source/conf.py
@@ -56,3 +56,5 @@
 # MyST Parser Configuration
 
 myst_enable_extensions = ["dollarmath", "amsmath"]
+
+prf_realtyp_to_countertyp = {}
diff --git a/docs/source/options.md b/docs/source/options.md
@@ -31,6 +31,61 @@ sphinx:
 
 Add `proof_minimal_theme = True` to your `conf.py`
 
+## Shared numbering
+
+By default, each type of (prf-)directive has their own numbering and counter. This can be changed by setting the option `prf_realtyp_to_countertyp` to a dictionary associating to a directive which the counter of which directive it should use.
+
+### Sphinx Project
+
+In `conf.py`, e.g. to have a shared counter for all directives:
+
+```
+prf_realtyp_to_countertyp = {
+    "axiom": "theorem",
+    "theorem": "theorem",
+    "lemma": "theorem",
+    "algorithm": "theorem",
+    "definition": "theorem",
+    "remark": "theorem",
+    "conjecture": "theorem",
+    "corollary": "theorem",
+    "criterion": "theorem",
+    "example": "theorem",
+    "property": "theorem",
+    "observation": "theorem",
+    "proposition": "theorem",
+    "assumption": "theorem",
+    "notation": "theorem",
+}
+```
+
+In the following case, the directives `lemma`, `conjecture`, `corollary` and `proposition` will share the counter with `theorem`, while `axiom` and `assumption` will share the counter with `definition`. All other directives would use their original counter.
+
+
+```
+prf_realtyp_to_countertyp = {
+    "lemma": "theorem",
+    "conjecture": "theorem",
+    "corollary": "theorem",
+    "proposition": "theorem",
+    "axiom": "definition",
+    "assumption": "definition",
+}
+```
+
+````{warning}
+The association of a counter to a directive is not transitive: Let us consider the following configuration:
+
+```
+prf_realtyp_to_countertyp = {
+    "lemma": "theorem",
+    "conjecture": "lemma",
+}
+```
+
+The `lemma` and `theorem` directives share a counter, however the `conjecture` directive has a separate counter (the `lemma` counter which is **not** used by `lemma` directives).
+````
+
 ## Title format
 
 By default, the directive titles are formatted as `Name x.y.z (Title)`, where `Name` is the name of the directive (e.g., Proof, Theorem, Definition), `x.y.z` is the numbering of the directive, and `Title` is the optional title provided by the user.
diff --git a/sphinx_proof/__init__.py b/sphinx_proof/__init__.py
@@ -102,11 +102,13 @@ def copy_asset_files(app: Sphinx, exc: Union[bool, Exception]):
 def setup(app: Sphinx) -> Dict[str, Any]:
 
     app.add_config_value("proof_minimal_theme", False, "html")
+    app.add_config_value("prf_realtyp_to_countertyp", {}, "html")
     app.add_config_value("proof_title_format", " (%t)", "html")
-    app.add_config_value("proof_number_weight", "", "env")
-    app.add_config_value("proof_title_weight", "", "env")
+    app.add_config_value("proof_number_weight", "", "html")
+    app.add_config_value("proof_title_weight", "", "html")
 
     app.add_css_file("proof.css")
+    app.connect("config-inited", check_config_values)
     app.connect("build-finished", copy_asset_files)
     app.connect("config-inited", init_numfig)
     app.connect("env-purge-doc", purge_proofs)
@@ -142,3 +144,64 @@ def setup(app: Sphinx) -> Dict[str, Any]:
         "parallel_read_safe": True,
         "parallel_write_safe": True,
     }
+
+
+def check_config_values(app: Sphinx, config: Config) -> None:
+    """Check configuration values."""
+    # Check if proof_minimal_theme is boolean
+    if not isinstance(config.proof_minimal_theme, bool):
+        logger.warning(
+            "'proof_minimal_theme' config value must be a boolean. "
+            "Using default value False."
+        )
+        config.proof_minimal_theme = False
+
+    # Check of prf_realtyp_to_countertyp is a dictionary
+    if not isinstance(config.prf_realtyp_to_countertyp, dict):
+        logger.warning(
+            "'prf_realtyp_to_countertyp' config value must be a dictionary. "
+            "Using default empty dictionary."
+        )
+        config.prf_realtyp_to_countertyp = {}
+    # Check if each key and each value in prf_realtyp_to_countertyp
+    # is a valid proof type
+    for key, value in config.prf_realtyp_to_countertyp.items():
+        if key not in PROOF_TYPES:
+            logger.warning(
+                f"Key '{key}' in 'prf_realtyp_to_countertyp' is not "
+                "a valid proof type. "
+                "It will be removed."
+            )
+            del config.prf_realtyp_to_countertyp[key]
+        elif value not in PROOF_TYPES:
+            logger.warning(
+                f"Value '{value}' in 'prf_realtyp_to_countertyp' is not "
+                "a valid proof type. It will be removed."
+            )
+            del config.prf_realtyp_to_countertyp[key]
+    # Check if proof_title_format is a string
+    if not isinstance(config.proof_title_format, str):
+        logger.warning(
+            "'proof_title_format' config value must be a string."
+            "Using default value ' (%t)'."
+        )
+        config.proof_title_format = " (%t)"
+    elif "%t" not in config.proof_title_format:
+        logger.warning(
+            "'proof_title_format' config value must contain the "
+            "substring '%t' to print a title."
+        )
+    # Check if proof_number_weight is a string
+    if not isinstance(config.proof_number_weight, str):
+        logger.warning(
+            "'proof_number_weight' config value must be a string. "
+            "Using default value ''."
+        )
+        config.proof_number_weight = ""
+    # Check if proof_title_weight is a string
+    if not isinstance(config.proof_title_weight, str):
+        logger.warning(
+            "'proof_title_weight' config value must be a string. "
+            "Using default value ''."
+        )
+        config.proof_title_weight = ""
diff --git a/sphinx_proof/directive.py b/sphinx_proof/directive.py
@@ -20,6 +20,25 @@
 logger = logging.getLogger(__name__)
 
 
+DEFAULT_REALTYP_TO_COUNTERTYP = {
+    "axiom": "axiom",
+    "theorem": "theorem",
+    "lemma": "lemma",
+    "algorithm": "algorithm",
+    "definition": "definition",
+    "remark": "remark",
+    "conjecture": "conjecture",
+    "corollary": "corollary",
+    "criterion": "criterion",
+    "example": "example",
+    "property": "property",
+    "observation": "observation",
+    "proposition": "proposition",
+    "assumption": "assumption",
+    "notation": "notation",
+}
+
+
 class ElementDirective(SphinxDirective):
     """A custom Sphinx Directive"""
 
@@ -36,13 +55,16 @@ class ElementDirective(SphinxDirective):
 
     def run(self) -> List[Node]:
         env = self.env
-        typ = self.name.split(":")[1]
+        realtyp = self.name.split(":")[1]
+        countertyp = env.config.prf_realtyp_to_countertyp.get(
+            realtyp, DEFAULT_REALTYP_TO_COUNTERTYP[realtyp]
+        )
         serial_no = env.new_serialno()
         if not hasattr(env, "proof_list"):
             env.proof_list = {}
 
         # If class in options add to class array
-        classes, class_name = ["proof", typ], self.options.get("class", [])
+        classes, class_name = ["proof", realtyp], self.options.get("class", [])
         if class_name:
             classes.extend(class_name)
 
@@ -53,15 +75,15 @@ def run(self) -> List[Node]:
             node_id = f"{label}"
         else:
             self.options["noindex"] = True
-            label = f"{typ}-{serial_no}"
-            node_id = f"{typ}-{serial_no}"
+            label = f"{realtyp}-{serial_no}"
+            node_id = f"{realtyp}-{serial_no}"
         ids = [node_id]
 
         # Duplicate label warning
         if not label == "" and label in env.proof_list.keys():
             path = env.doc2path(env.docname)[:-3]
             other_path = env.doc2path(env.proof_list[label]["docname"])
-            msg = f"duplicate {typ} label '{label}', other instance in {other_path}"
+            msg = f"duplicate {realtyp} label '{label}', other instance in {other_path}"
             logger.warning(msg, location=path, color="red")
 
         title_text = ""
@@ -72,13 +94,13 @@ def run(self) -> List[Node]:
 
         textnodes, messages = self.state.inline_text(title_text, self.lineno)
 
-        section = nodes.section(classes=[f"{typ}-content"], ids=["proof-content"])
+        section = nodes.section(classes=[f"{realtyp}-content"], ids=["proof-content"])
         self.state.nested_parse(self.content, self.content_offset, section)
 
         if "nonumber" in self.options:
             node = unenumerable_node()
         else:
-            node_type = NODE_TYPES[typ]
+            node_type = NODE_TYPES[countertyp]
             node = node_type()
 
         node.document = self.state.document
@@ -90,17 +112,18 @@ def run(self) -> List[Node]:
         node["classes"].extend(classes)
         node["title"] = title_text
         node["label"] = label
-        node["type"] = typ
+        node["countertype"] = countertyp
+        node["realtype"] = realtyp
 
         env.proof_list[label] = {
             "docname": env.docname,
-            "type": typ,
+            "countertype": countertyp,
+            "realtype": realtyp,
             "ids": ids,
             "label": label,
             "prio": 0,
             "nonumber": True if "nonumber" in self.options else False,
         }
-
         return [node]
 
 
@@ -117,16 +140,16 @@ class ProofDirective(SphinxDirective):
     }
 
     def run(self) -> List[Node]:
-        typ = self.name.split(":")[1]
+        realtyp = self.name.split(":")[1]
 
         # If class in options add to class array
-        classes, class_name = ["proof", typ], self.options.get("class", [])
+        classes, class_name = ["proof", realtyp], self.options.get("class", [])
         if class_name:
             classes.extend(class_name)
 
-        section = nodes.admonition(classes=classes, ids=[typ])
+        section = nodes.admonition(classes=classes, ids=[realtyp])
 
-        self.content[0] = "{}. ".format(typ.title()) + self.content[0]
+        self.content[0] = "{}. ".format(realtyp.title()) + self.content[0]
         self.state.nested_parse(self.content, 0, section)
 
         node = proof_node()
diff --git a/sphinx_proof/domain.py b/sphinx_proof/domain.py
@@ -45,7 +45,7 @@ def generate(self, docnames=None) -> Tuple[Dict[str, Any], bool]:
             return content, True
 
         proofs = self.domain.env.proof_list
-        # {'theorem-0': {'docname': 'start/overview', 'type': 'theorem', 'ids': ['theorem-0'], 'label': 'theorem-0', 'prio': 0, 'nonumber': False}} # noqa: E501
+        # {'theorem-0': {'docname': 'start/overview', 'realtype': 'theorem', 'countertype': 'theorem', 'ids': ['theorem-0'], 'label': 'theorem-0', 'prio': 0, 'nonumber': False}} # noqa: E501
 
         # name, subtype, docname, typ, anchor, extra, qualifier, description
         for anchor, values in proofs.items():
@@ -57,7 +57,7 @@ def generate(self, docnames=None) -> Tuple[Dict[str, Any], bool]:
                     anchor,
                     values["docname"],
                     "",
-                    values["type"],
+                    values["realtype"],
                 )
             )
 
@@ -157,11 +157,12 @@ def resolve_xref(
             if target in contnode[0]:
                 number = ""
                 if not env.proof_list[target]["nonumber"]:
-                    typ = env.proof_list[target]["type"]
+                    countertyp = env.proof_list[target]["countertype"]
                     number = ".".join(
-                        map(str, env.toc_fignumbers[todocname][typ][target])
+                        map(str, env.toc_fignumbers[todocname][countertyp][target])
                     )
-                title = nodes.Text(f"{translate(match['type'].title())} {number}")
+                type_title = translate(match["realtype"].title())
+                title = nodes.Text(f"{type_title} {number}")
             # builder, fromdocname, todocname, targetid, child, title=None
             return make_refnode(builder, fromdocname, todocname, target, title)
         else:
diff --git a/sphinx_proof/nodes.py b/sphinx_proof/nodes.py
@@ -13,6 +13,11 @@
 from sphinx.writers.latex import LaTeXTranslator
 from sphinx.locale import get_translation
 
+
+from sphinx.util import logging
+
+logger = logging.getLogger(__name__)
+
 MESSAGE_CATALOG_NAME = "proof"
 _ = get_translation(MESSAGE_CATALOG_NAME)
 
@@ -31,17 +36,18 @@ def visit_enumerable_node(self, node: Node) -> None:
 
 
 def depart_enumerable_node(self, node: Node) -> None:
-    typ = node.attributes.get("type", "")
+    countertyp = node.attributes.get("countertype", "")
+    realtyp = node.attributes.get("realtype", "")
     if isinstance(self, LaTeXTranslator):
-        number = get_node_number(self, node, typ)
+        number = get_node_number(self, node, countertyp)
         idx = list_rindex(self.body, latex_admonition_start) + 2
-        self.body.insert(idx, f"{typ.title()} {number}")
+        self.body.insert(idx, f"{realtyp.title()} {number}")
         self.body.append(latex_admonition_end)
     else:
         # Find index in list of 'Proof #'
-        number = get_node_number(self, node, typ)
-        idx = self.body.index(f"{typ} {number} ")
-        self.body[idx] = f"{_(typ.title())} {number} "
+        number = get_node_number(self, node, countertyp)
+        idx = self.body.index(f"{countertyp} {number} ")
+        self.body[idx] = f"{_(realtyp.title())} {number} "
         self.body.append("</div>")
 
 
@@ -55,18 +61,18 @@ def visit_unenumerable_node(self, node: Node) -> None:
 
 
 def depart_unenumerable_node(self, node: Node) -> None:
-    typ = node.attributes.get("type", "")
+    realtyp = node.attributes.get("realtype", "")
     title = node.attributes.get("title", "")
     if isinstance(self, LaTeXTranslator):
         idx = list_rindex(self.body, latex_admonition_start) + 2
-        self.body.insert(idx, f"{typ.title()}")
+        self.body.insert(idx, f"{realtyp.title()}")
         self.body.append(latex_admonition_end)
     else:
         if title == "":
             idx = list_rindex(self.body, '<p class="admonition-title">') + 1
         else:
             idx = list_rindex(self.body, title)
-        element = f"<span>{_(typ.title())} </span>"
+        element = f"<span>{_(realtyp.title())} </span>"
         self.body.insert(idx, element)
         self.body.append("</div>")
 
@@ -79,10 +85,10 @@ def depart_proof_node(self, node: Node) -> None:
     pass
 
 
-def get_node_number(self, node: Node, typ) -> str:
+def get_node_number(self, node: Node, countertyp) -> str:
     """Get the number for the directive node for HTML."""
     ids = node.attributes.get("ids", [])[0]
-    key = typ
+    key = countertyp
     if isinstance(self, LaTeXTranslator):
         docname = find_parent(self.builder.env, node, "section")
         fignumbers = self.builder.env.toc_fignumbers.get(
@@ -91,7 +97,7 @@ def get_node_number(self, node: Node, typ) -> str:
     else:
         fignumbers = self.builder.fignumbers
         if self.builder.name == "singlehtml":
-            key = "%s/%s" % (self.docnames[-1], typ)
+            key = "%s/%s" % (self.docnames[-1], countertyp)
     number = fignumbers.get(key, {}).get(ids, ())
     return ".".join(map(str, number))
 
