diff --git a/scripts/check_docs.py b/scripts/check_docs.py index 4764acaa1..4fd3bde4a 100644 --- a/scripts/check_docs.py +++ b/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: diff --git a/scripts/test_check_docs.py b/scripts/test_check_docs.py index 3b5b3679b..c4ed2a17d 100644 --- a/scripts/test_check_docs.py +++ b/scripts/test_check_docs.py @@ -478,6 +478,62 @@ def test_legacy_local_only_external_targets_manifest_is_upgraded_or_rejected(sel f'specialize_all', ) + 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"), '
') + prefixes = ("./", check_docs.API_DOCS_URL, check_docs.MATHLIB_DOCS_URL) + links = [f'{name}.rec' + 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'{name}.rec' + 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), '
') + 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'bad') + 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"), '
') + self.write(self.page("Complexity"), 'rec') + self.write(self.docs / "declarations/declaration-data.bmp", json.dumps(self.index)) + check_docs.trim_output() + self.assertEqual(self.page("Complexity").read_text(), + f'rec') + def test_trim_remaps_moved_and_falls_back_for_omitted_published_declarations(self): self.index["modules"]["Mathlib.LinearAlgebra.Matrix.Defs"] = { "importedBy": ["Complexity.Current"],