fix(hygiene): check reference-style documentation links

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<link>(?<!!)\[(?:`+[^`\n]*`+|\\.|[^\[\]`\\])*\]\(\s*"
     r"(?:<(?P<angle_target>[^>\s]+)>|(?P<target>[^)\s\"']+))"
     r"(?:\s+(?:\"[^\"]*\"|'[^']*'|\([^)\n]*\)))?\s*\))"
-    r"|(?P<code_fence>`+)(?P<code>.+?)(?<!`)(?P=code_fence)(?!`)"
+    r"|(?P<code_fence>`+)(?P<code>(?:(?!\n[ \t]*\n)[\s\S])+?)(?<!`)(?P=code_fence)(?!`)"
+)
+DOC_REFERENCE_RE = re.compile(
+    r"^[ ]{0,3}\[(?P<label>(?:\\.|[^\[\]\\\n])+)\]:[ \t]*(?:\n[ ]{0,3})?"
+    r"(?:<(?P<angle_target>[^<>\n]*)>|(?P<target>[^\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
 
 

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]: <https://example.com/paper.pdf> (Paper)\n"
+            "   [anchor]: #result\n"
+            "[dependency]: Mathlib/Data/Nat/Basic.html\n"
+            "[next-line]:\n  <Complexity/Init.html>\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]: <Missing>\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   <Mathlib/Missing.html>\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",