From 127b3e2f34392ea6c95cffdc9ee5ef8d71c774b3 Mon Sep 17 00:00:00 2001 From: karnseth Date: Thu, 29 Oct 2026 07:15:22 -0400 Subject: [PATCH] fix(hygiene): validate reference-style documentation links --- scripts/check_hygiene.py | 41 ++++++++++++-- scripts/test_check_hygiene.py | 100 ++++++++++++++++++++++++++++++++++ 2 files changed, 135 insertions(+), 6 deletions(-) diff --git a/scripts/check_hygiene.py b/scripts/check_hygiene.py index ac26787d77..10d69c44c3 100755 --- a/scripts/check_hygiene.py +++ b/scripts/check_hygiene.py @@ -8,16 +8,19 @@ 3. Every `set_option maxHeartbeats` or `set_option maxRecDepth` has an explanatory comment on the same line, within the preceding 3 lines, or (for `set_option ... in`) on the next line, where Mathlib's `linter.style.maxHeartbeats` expects it. -4. Docstrings in `Complexity/` contain only root-qualified or external inline Markdown links +4. Docstrings in `Complexity/` contain only root-qualified or external Markdown links (`[text](target)`, where external means `http://` or `https://` and anchors start with `#`, matching `doc-gen4`'s `extendLink`) and root-qualified slash-containing `.lean` code tokens (`Complexity/.../*.lean`, `Cslib/...`, `Mathlib/...`) in inline code spans and fenced Lean code blocks. `Complexity/...` targets are checked for file existence on disk; dependency roots (`Cslib/`, `Mathlib/`, `Batteries/`) are checked on disk when `.lake/packages` is present locally and by root prefix in CI (where `check_hygiene.py` runs before `.lake` is restored) or for - toolchain roots (`Std/`, `Init/`, `Lean/`). Reference-link definitions (`[label]: target`) and - indented (4-space) code blocks are not scanned; `scripts/check_docs.py` in `docs.yml` remains the - full HTML backstop. + toolchain roots (`Std/`, `Init/`, `Lean/`). Reference-link definitions (`[label]: target`, with + an optional single-line title and the destination on the same or next line) use the same + target check. + Citation-shaped labels followed by a bare prose word remain citation prose. + Nested block-container definitions and indented (4-space) code blocks are not scanned; + `scripts/check_docs.py` in `docs.yml` remains the full HTML backstop. 5. (Default selection only.) `references.bib` keys are unique and its entries are sorted by key, both compared case-insensitively as BibTeX does, so that PRs adding entries rarely conflict. 6. Every citation key in a docstring is a `references.bib` key. A citation is a bracketed segment @@ -94,7 +97,13 @@ r"|(?P(?[^>\s]+)>|(?P[^)\s\"']+))" r"(?:\s+(?:\"[^\"]*\"|'[^']*'|\([^)\n]*\)))?\s*\))" - r"|(?P`+)(?P.+?)(?`+)(?P(?:(?!\n[ \t]*\n)[\s\S])+?)(?(?:\\.|[^\[\]\\\n])+)\]:[ \t]*(?:\n[ ]{0,3})?" + r"(?:<(?P[^<>\n]*)>|(?P[^\s<>]+))" + r"(?:[ \t]+(?:\"[^\"\n]*\"|'[^'\n]*'|\([^)\n]*\)))?[ \t]*$", + re.M, ) WHITESPACE_RUN_RE = re.compile(r"\S+") # The shape of every `references.bib` key except the year-less `MilewskiDao`. @@ -185,7 +194,7 @@ def validate_doc_module_path(part: str, root: pathlib.Path) -> str | None: def validate_doc_markdown_target(target: str, root: pathlib.Path) -> str | None: - """Validate a Markdown link target `[text](target)` in a `Complexity/` docstring.""" + """Validate an inline or reference Markdown link target in a `Complexity/` docstring.""" if target.startswith(("https://", "http://", "#")): return None path_part, _, _ = target.partition("#") @@ -265,6 +274,26 @@ def check_docstring_links(raw: str, rel: pathlib.Path, root: pathlib.Path) -> li errors.append( f"{rel}:{line_no}: invalid docstring module path `{tok}` ({reason})" ) + # Reference definitions inside inline code, math or escaped brackets are examples, + # not links. Preserve offsets while hiding them from the line-based scan below. + mask_span(chars, m.start(), m.end()) + for m in DOC_REFERENCE_RE.finditer(masked_doc): + label_start = m.start() + len(m[0]) - len(m[0].lstrip(" ")) + if chars[label_start] != "[": + continue + target = m.group("angle_target") + if target is None: + target = m.group("target") + # A citation sentence may wrap just after "[Key, locator]: if". Preserve + # citation prose, but still validate explicit angle/path/URL destinations. + if target.isalpha() and docstring_citations("[" + m.group("label") + "]"): + continue + reason = validate_doc_markdown_target(target, root) + if reason: + line_no = raw.count("\n", 0, doc_start + m.start()) + 1 + errors.append( + f"{rel}:{line_no}: invalid docstring Markdown link target `{target}` ({reason})" + ) return errors diff --git a/scripts/test_check_hygiene.py b/scripts/test_check_hygiene.py index eac1a2bb3c..ba137a18fd 100644 --- a/scripts/test_check_hygiene.py +++ b/scripts/test_check_hygiene.py @@ -384,6 +384,106 @@ def test_docstring_markdown_links_and_module_paths_from_1358_and_1367(self) -> N ) self.assertEqual(check_hygiene.check_file(fixed_1367, root=self.root), []) + def test_docstring_reference_link_targets(self) -> None: + self.write("Complexity/Init.lean", "module\n-- upstream: candidate\n") + bad_targets = ( + "/Complexity/Init.lean", # The reference-link gap reported in #1616. + "Complexity/Init.lean", + "Init.html", + "Complexity/Missing.html#result", + "Complexity/../Init.html", + "mailto:example@example.com", + ) + for target in bad_targets: + for destination in (target, f"<{target}>"): + with self.subTest(destination=destination): + p = self.write( + "Complexity/Reference.lean", + "module\n-- upstream: candidate\n/-!\nSee [consumer][adjacency].\n\n" + f"[adjacency]: {destination} 'Consumer'\n-/\n", + ) + errors = check_hygiene.check_file(p, root=self.root) + self.assertEqual(len(errors), 1, errors) + self.assertIn( + f"Complexity/Reference.lean:6: invalid docstring Markdown link target `{target}`", + errors[0], + ) + + good = self.write( + "Complexity/Reference.lean", + "module\n-- upstream: candidate\n/-!\n" + "See [consumer][module], [external] and [anchor][].\n\n" + "[module]: Complexity/Init.html#result \"Init\"\n" + " [external]: (Paper)\n" + " [anchor]: #result\n" + "[dependency]: Mathlib/Data/Nat/Basic.html\n" + "[next-line]:\n \n" + "-/\n", + ) + self.assertEqual(check_hygiene.check_file(good, root=self.root), []) + + def test_reference_definitions_ignore_code_math_escapes_and_citation_prose(self) -> None: + p = self.write( + "Complexity/ReferenceExamples.lean", + "module\n-- upstream: candidate\n/-!\n" + "```markdown\n[example]: Missing.html\n```\n" + "`[inline]: Missing.html`\n" + "`multiline\n[code]: Missing.html\n`\n" + "$$\n[math]: Missing.html\n$$\n" + "\\[escaped]: Missing.html\n" + " [indented]: Missing.html\n" + "`x`[not-a-definition]: Missing.html\n" + "[AroraBarak09]: for each input, the theorem applies.\n" + "[real]: Missing.html\n-/\n", + ) + errors = check_hygiene.check_file(p, root=self.root) + self.assertEqual(len(errors), 1, errors) + self.assertIn("invalid docstring Markdown link target `Missing.html`", errors[0]) + self.assertIn(":18:", errors[0]) + + def test_wrapped_citation_prose_is_not_a_reference_destination(self) -> None: + p = self.write( + "Complexity/CitationProse.lean", + "module\n-- upstream: candidate\n/-!\n" + "[AroraBarak09, Theorem 1]: if\n" + "the hypothesis holds, the conclusion follows.\n\n" + "[AroraBarak09]: the\n" + "first part of the result.\n\n" + "[AroraBarak09]: /Complexity/Init.lean\n" + "[AroraBarak09]: \n" + "[ordinary-label]: Missing\n-/\n", + ) + errors = check_hygiene.check_file(p, root=self.root) + self.assertEqual(len(errors), 3, errors) + self.assertIn("`/Complexity/Init.lean`", errors[0]) + self.assertIn("`Missing`", errors[1]) + self.assertIn("`Missing`", errors[2]) + + def test_unmatched_backtick_does_not_hide_links_or_citations_in_later_paragraphs(self) -> None: + doc = "Literal unmatched ` in prose.\n\n[broken]: Missing.html\n\n[Unknown2026]\n\nLater `code`." + p = self.write( + "Complexity/Paragraphs.lean", + "module\n-- upstream: candidate\n/-!\n" + doc + "\n-/\n", + ) + errors = check_hygiene.check_file(p, root=self.root) + self.assertEqual(len(errors), 1, errors) + self.assertIn("`Missing.html`", errors[0]) + self.assertEqual([key for _, key in check_hygiene.docstring_citations(doc)], + ["Unknown2026"]) + + def test_reference_definition_next_line_and_dependency_existence(self) -> None: + self.write(".lake/packages/mathlib/Mathlib/Existing.lean", "module\n") + p = self.write( + "Complexity/Reference.lean", + "module\n-- upstream: candidate\n/-!\n" + "[missing]:\n \n" + "[existing]: Mathlib/Existing.html\n-/\n", + ) + errors = check_hygiene.check_file(p, root=self.root) + self.assertEqual(len(errors), 1, errors) + self.assertIn("Complexity/Reference.lean:4:", errors[0]) + self.assertIn("target dependency module `Mathlib/Missing.lean` does not exist", errors[0]) + def test_docstring_nonexistent_complexity_module_or_fenced_code_path_fails(self) -> None: p = self.write( "Complexity/MissingTarget.lean",