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",