fix(docs): redirect omitted recursors to their indexed types

scripts/check_docs.py

@@ -309,6 +309,26 @@ def rewrite_external_dependency_links(docs, index, external_pages):
         if (docs / rel).is_file():
             local_anchors_by_page[rel].update(page_anchors(docs / rel, anchor_cache))
 
+    def recursor_parent_fragment(norm, fragment):
+        """Link omitted generated recursors to their indexed inductive/structure parent."""
+        if not fragment:
+            return fragment
+        anchor = unquote(fragment)
+        if anchor in local_anchors_by_page.get(norm, ()):
+            return fragment
+        parent, _, suffix = anchor.rpartition(".")
+        info = index.get("declarations", {}).get(parent, {})
+        if suffix != "rec" or info.get("kind") not in ("inductive", "structure"):
+            return fragment
+        parent_link = urlsplit(info.get("docLink", ""))
+        if (
+            normalize_doc_relpath(unquote(parent_link.path)) == norm
+            and unquote(parent_link.fragment) == parent
+            and parent in local_anchors_by_page.get(norm, ())
+        ):
+            return parent_link.fragment
+        return fragment
+
     for page in sorted(docs.rglob("*.html")):
         if not page.is_file():
             continue
@@ -368,6 +388,8 @@ def replace_href(match):
                             f"Broken dependency link in {rel_page}: {rel_target}")
                     if (docs / norm).is_file():
                         local_anchors_by_page[norm].update(page_anchors(docs / norm, anchor_cache))
+                    fragment = recursor_parent_fragment(norm, fragment)
+                    anchor = unquote(fragment) if fragment else None
                     if fragment and (norm, anchor) not in KERNEL_RECURSOR_ANCHORS:
                         require(anchor in local_anchors_by_page[norm],
                                 f"Broken dependency anchor in {rel_page}: {norm}#{anchor}")
@@ -396,6 +418,7 @@ def replace_href(match):
                     f"Broken dependency link in {rel_page}: {norm}")
             if (docs / norm).is_file():
                 local_anchors_by_page[norm].update(page_anchors(docs / norm, anchor_cache))
+            fragment = recursor_parent_fragment(norm, fragment)
             if fragment:
                 anchor = unquote(fragment)
                 if (norm, anchor) not in KERNEL_RECURSOR_ANCHORS:

scripts/test_check_docs.py

@@ -478,6 +478,62 @@ def test_legacy_local_only_external_targets_manifest_is_upgraded_or_rejected(sel
             f'<a href="{check_docs.MATHLIB_DOCS_URL}Mathlib/Tactic/TautoSet.html">specialize_all</a>',
         )
 
+    def test_trim_redirects_omitted_recursors_to_the_documented_type(self):
+        self.index["modules"]["Init.Core"] = {}
+        self.index["declarations"]["Sum"] = {
+            "docLink": "./Init/Core.html#Sum", "kind": "inductive",
+        }
+        self.index["declarations"]["Prod"] = {
+            "docLink": "./Init/Core.html#Prod", "kind": "structure",
+        }
+        self.write(self.page("Init.Core"), '<div id="Sum"></div><div id="Prod"></div>')
+        prefixes = ("./", check_docs.API_DOCS_URL, check_docs.MATHLIB_DOCS_URL)
+        links = [f'<a href="{prefix}Init/Core.html#{name}.rec">{name}.rec</a>'
+                 for prefix in prefixes for name in ("Sum", "Prod")]
+        self.write(self.page("Complexity"), "\n".join(links))
+        self.write(self.docs / "declarations/declaration-data.bmp", json.dumps(self.index))
+
+        check_docs.trim_output()
+        with redirect_stdout(io.StringIO()):
+            check_docs.check_output()
+        expected = "\n".join(
+            f'<a href="{check_docs.MATHLIB_DOCS_URL}Init/Core.html#{name}">{name}.rec</a>'
+            for _ in prefixes for name in ("Sum", "Prod")
+        )
+        self.assertEqual(self.page("Complexity").read_text(), expected)
+        check_docs.trim_output()
+        self.assertEqual(self.page("Complexity").read_text(), expected)
+
+    def test_trim_recursor_fallback_rejects_unproved_targets(self):
+        for module in ("Init.Core", "Init.Other"):
+            self.index["modules"][module] = {}
+            self.write(self.page(module), '<div id="Sum"></div><div id="ordinary"></div>')
+        self.index["declarations"]["Sum"] = {
+            "docLink": "./Init/Core.html#Sum", "kind": "inductive",
+        }
+        self.index["declarations"]["ordinary"] = {
+            "docLink": "./Init/Core.html#ordinary", "kind": "def",
+        }
+        self.write(self.docs / "declarations/declaration-data.bmp", json.dumps(self.index))
+        for target in ("Init/Core.html#Missing.rec", "Init/Core.html#ordinary.rec",
+                       "Init/Core.html#Sum.missing", "Init/Other.html#Sum.rec"):
+            with self.subTest(target=target):
+                self.write(self.page("Complexity"), f'<a href="./{target}">bad</a>')
+                with self.assertRaisesRegex(ValueError, "Broken dependency anchor"):
+                    check_docs.trim_output()
+
+    def test_trim_preserves_a_documented_recursor_anchor(self):
+        self.index["modules"]["Init.Core"] = {}
+        self.index["declarations"]["Sum"] = {
+            "docLink": "./Init/Core.html#Sum", "kind": "inductive",
+        }
+        self.write(self.page("Init.Core"), '<div id="Sum"></div><div id="Sum.rec"></div>')
+        self.write(self.page("Complexity"), '<a href="./Init/Core.html#Sum.rec">rec</a>')
+        self.write(self.docs / "declarations/declaration-data.bmp", json.dumps(self.index))
+        check_docs.trim_output()
+        self.assertEqual(self.page("Complexity").read_text(),
+                         f'<a href="{check_docs.MATHLIB_DOCS_URL}Init/Core.html#Sum.rec">rec</a>')
+
     def test_trim_remaps_moved_and_falls_back_for_omitted_published_declarations(self):
         self.index["modules"]["Mathlib.LinearAlgebra.Matrix.Defs"] = {
             "importedBy": ["Complexity.Current"],