chore(hygiene): check that both READMEs list the abstract catalogue

.agents/skills/lean-abstract/SKILL.md

@@ -23,7 +23,7 @@ Formal abstracts and their bridges live in the dedicated `ComplexityAbstracts` L
 - **Abstract module**: `abstracts/ComplexityAbstracts/<Topic>Abstract.lean`
 - **Audit helper**: [Check.lean](../../../abstracts/ComplexityAbstracts/Check.lean) (`#check_abstract`)
 
-Import new `*Abstract.lean` modules from [ComplexityAbstracts.lean](../../../abstracts/ComplexityAbstracts.lean). The test driver imports that library, so `lake test --wfail --iofail` builds and audits every abstract in CI. Keep regression tests in `ComplexityTests/Abstracts/`; Lake's `ComplexityTests.+` glob discovers new modules automatically. Existing abstracts retain their `ComplexityTests.Abstracts.*` declaration namespaces for compatibility; new abstracts may use `ComplexityAbstracts.*`. Catalogue entries specify `namespace` when it differs from their module name.
+Import new `*Abstract.lean` modules from [ComplexityAbstracts.lean](../../../abstracts/ComplexityAbstracts.lean). The test driver imports that library, so `lake test --wfail --iofail` builds and audits every abstract in CI. Keep regression tests in `ComplexityTests/Abstracts/`; Lake's `ComplexityTests.+` glob discovers new modules automatically. Existing abstracts retain their `ComplexityTests.Abstracts.*` declaration namespaces for compatibility; new abstracts may use `ComplexityAbstracts.*`. Catalogue entries specify `namespace` when it differs from their module name. List each selected entry in the top-level `README.md` selected results and in the table of `abstracts/README.md`; `scripts/check_hygiene.py` checks that both READMEs link exactly the catalogue's abstract modules.
 
 ---
 

CONTRIBUTING.md

@@ -239,6 +239,9 @@ models, encodings, hypotheses, bounds and limitations. The library contains many
 selection is an editorial decision, not an automatic consequence of adding a theorem. A headline
 must establish a substantial full endpoint with conventional semantics and nonvacuous premises.
 Keep incomplete endpoints in `ROADMAP.md` and credit mathematical and formalization sources.
+List every selected entry in the top-level README's selected results and in the table of
+[abstracts/README.md](abstracts/README.md); `scripts/check_hygiene.py` checks both lists against
+the catalogue.
 
 Follow [the abstract requirements](AGENTS.md#curated-formal-abstracts) for impact assessment,
 source layout, independent review and `#check_abstract` audits. These apply to affected claims

scripts/check_hygiene.py

@@ -38,16 +38,21 @@
    Inline and multiline settings and decimal/hexadecimal numerals are checked. With the default
    selection, an entry whose file no longer needs it (no budget above the default, or a cap above the largest
    budget) is reported as stale, so the allowlist only shrinks as budgets are reduced (#1528).
+8. (Default selection only.) Every `abstracts/catalogue.json` entry is linked from the top-level
+   `README.md` (`](abstracts/ComplexityAbstracts/<Name>.lean)`) and from `abstracts/README.md`
+   (`](ComplexityAbstracts/<Name>.lean)`), and neither README links an abstract module that the
+   catalogue does not select (#1921).
 
 Opt-in heuristic checks:
-8. (`--check-simp`) Flag non-terminal bare `simp` tactics in `-- upstream: candidate` modules
+9. (`--check-simp`) Flag non-terminal bare `simp` tactics in `-- upstream: candidate` modules
    under Complexity/.
-9. (`--max-lines N`) Flag Lean files exceeding N lines.
+10. (`--max-lines N`) Flag Lean files exceeding N lines.
 """
 
 from __future__ import annotations
 
 import argparse
+import json
 import pathlib
 import re
 import sys
@@ -537,6 +542,40 @@ def check_bibliography(text: str, rel: str = "references.bib") -> list[str]:
     return errors
 
 
+# Each README with the prefix of its links to abstract modules.
+ABSTRACT_READMES = (("README.md", "abstracts/"), ("abstracts/README.md", ""))
+# A Markdown link to an abstract module (not to a bridge or a shared foundation).
+ABSTRACT_LINK_RE = re.compile(
+    r"\]\((?P<target>(?:abstracts/)?ComplexityAbstracts/[A-Za-z0-9_]+Abstract\.lean)\)")
+
+
+def check_abstract_readmes(root: pathlib.Path = ROOT) -> list[str]:
+    """Both READMEs link exactly the abstract modules that the catalogue selects."""
+    rel_catalogue = "abstracts/catalogue.json"
+    try:
+        entries = json.loads((root / rel_catalogue).read_text(encoding="utf-8"))["entries"]
+        sources = {entry["module"].replace(".", "/") + ".lean": entry["id"] for entry in entries}
+    except (OSError, ValueError, KeyError, TypeError, AttributeError) as err:
+        return [f"{rel_catalogue}: cannot read the catalogue entries ({err})"]
+    errors: list[str] = []
+    for rel, prefix in ABSTRACT_READMES:
+        try:
+            text = (root / rel).read_text(encoding="utf-8")
+        except OSError as err:
+            errors.append(f"{rel}: cannot read ({err})")
+            continue
+        linked = {m.group("target") for m in ABSTRACT_LINK_RE.finditer(text)}
+        for source, entry_id in sources.items():
+            if prefix + source not in linked:
+                errors.append(f"{rel}: catalogue entry `{entry_id}` is not listed; add a line "
+                              f"linking `{prefix}{source}`")
+        for target in sorted(linked):
+            if not target.startswith(prefix) or target[len(prefix):] not in sources:
+                errors.append(f"{rel}: links `{target}`, which is not a catalogue entry of "
+                              f"`{rel_catalogue}` (or uses the wrong relative path)")
+    return errors
+
+
 def check_paths(
     paths: list[pathlib.Path],
     root: pathlib.Path = ROOT,
@@ -603,6 +642,7 @@ def main() -> int:
     if not args.paths:
         errors += check_bibliography(bibliography)
         errors += check_heartbeat_allowlist_stale(heartbeat_caps)
+        errors += check_abstract_readmes()
     if errors:
         for err in errors:
             print(f"ERROR: {err}", file=sys.stderr)

scripts/test_check_hygiene.py

@@ -2,6 +2,7 @@
 
 from __future__ import annotations
 
+import json
 import pathlib
 import subprocess
 import sys
@@ -559,6 +560,64 @@ def test_repository_bibliography_is_sorted(self) -> None:
         self.assertEqual(check_hygiene.check_bibliography(text), [])
 
 
+class AbstractReadmeTests(unittest.TestCase):
+    def setUp(self) -> None:
+        tmp = tempfile.TemporaryDirectory()
+        self.addCleanup(tmp.cleanup)
+        self.root = pathlib.Path(tmp.name)
+        (self.root / "abstracts").mkdir()
+        catalogue = {"entries": [
+            {"id": "a", "module": "ComplexityAbstracts.AAbstract"},
+            {"id": "b", "module": "ComplexityAbstracts.BAbstract"},
+        ]}
+        (self.root / "abstracts/catalogue.json").write_text(json.dumps(catalogue),
+                                                            encoding="utf-8")
+
+    def write_readmes(self, top: str, abstracts: str) -> None:
+        (self.root / "README.md").write_text(top, encoding="utf-8")
+        (self.root / "abstracts/README.md").write_text(abstracts, encoding="utf-8")
+
+    def test_every_entry_listed_passes(self) -> None:
+        self.write_readmes(
+            "* [A](abstracts/ComplexityAbstracts/AAbstract.lean)\n"
+            "* [B](abstracts/ComplexityAbstracts/BAbstract.lean); see also "
+            "[A](abstracts/ComplexityAbstracts/AAbstract.lean) and the shared "
+            "[encoding](abstracts/ComplexityAbstracts/Encoding.lean).\n",
+            "| [A](ComplexityAbstracts/AAbstract.lean) |\n"
+            "| [B](ComplexityAbstracts/BAbstract.lean) |\n",
+        )
+        self.assertEqual(check_hygiene.check_abstract_readmes(self.root), [])
+
+    def test_missing_stale_and_misrooted_links_fail(self) -> None:
+        self.write_readmes(
+            "* [A](abstracts/ComplexityAbstracts/AAbstract.lean)\n"
+            "* [C](abstracts/ComplexityAbstracts/CAbstract.lean)\n",
+            "| [A](ComplexityAbstracts/AAbstract.lean) |\n"
+            "| [B](abstracts/ComplexityAbstracts/BAbstract.lean) |\n",
+        )
+        self.assertEqual(check_hygiene.check_abstract_readmes(self.root), [
+            "README.md: catalogue entry `b` is not listed; add a line linking "
+            "`abstracts/ComplexityAbstracts/BAbstract.lean`",
+            "README.md: links `abstracts/ComplexityAbstracts/CAbstract.lean`, which is not a "
+            "catalogue entry of `abstracts/catalogue.json` (or uses the wrong relative path)",
+            "abstracts/README.md: catalogue entry `b` is not listed; add a line linking "
+            "`ComplexityAbstracts/BAbstract.lean`",
+            "abstracts/README.md: links `abstracts/ComplexityAbstracts/BAbstract.lean`, which is "
+            "not a catalogue entry of `abstracts/catalogue.json` (or uses the wrong relative path)",
+        ])
+
+    def test_malformed_catalogue_fails(self) -> None:
+        (self.root / "abstracts/catalogue.json").write_text('{"entries": [{"id": "a"}]}',
+                                                            encoding="utf-8")
+        self.write_readmes("", "")
+        errors = check_hygiene.check_abstract_readmes(self.root)
+        self.assertEqual(len(errors), 1)
+        self.assertTrue(errors[0].startswith("abstracts/catalogue.json: cannot read"))
+
+    def test_repository_readmes_list_the_catalogue(self) -> None:
+        self.assertEqual(check_hygiene.check_abstract_readmes(), [])
+
+
 class CitationTests(unittest.TestCase):
     keys = frozenset({"AroraBarak09", "Ilango2020FOCS", "Sipser2013"})