From baa7fe589fc7b5a6aeecfa817e65bef5d122efa8 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 02:01:09 -0400 Subject: [PATCH] chore(hygiene): check that both READMEs list the abstract catalogue #1921 restored the top-level README's "Selected results" after it had fallen five entries behind abstracts/catalogue.json, and abstracts/README.md two behind. Three open abstract candidates (#1904, #1940, #1945) again add a catalogue entry and an abstracts/README.md row but no top-level README line. check_hygiene.py now checks, in its default selection, that README.md and abstracts/README.md each link every catalogue entry's abstract module, with the right relative path, and no abstract module outside the catalogue. CONTRIBUTING.md and the lean-abstract skill state the requirement. Found by auditor-claude-e6cf7b0d-15 (misformalization audit, round 15). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .agents/skills/lean-abstract/SKILL.md | 2 +- CONTRIBUTING.md | 3 ++ scripts/check_hygiene.py | 44 +++++++++++++++++++- scripts/test_check_hygiene.py | 59 +++++++++++++++++++++++++++ 4 files changed, 105 insertions(+), 3 deletions(-) diff --git a/.agents/skills/lean-abstract/SKILL.md b/.agents/skills/lean-abstract/SKILL.md index f1320f1b8..425a8e246 100644 --- a/.agents/skills/lean-abstract/SKILL.md +++ b/.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/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. --- diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 039e08594..e48c366d4 100644 --- a/CONTRIBUTING.md +++ b/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 diff --git a/scripts/check_hygiene.py b/scripts/check_hygiene.py index 10d69c44c..3c1af804d 100755 --- a/scripts/check_hygiene.py +++ b/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/.lean)`) and from `abstracts/README.md` + (`](ComplexityAbstracts/.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(?: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) diff --git a/scripts/test_check_hygiene.py b/scripts/test_check_hygiene.py index ba137a18f..7b516f6af 100644 --- a/scripts/test_check_hygiene.py +++ b/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"})