From b344a6846e9f0dc4ce91e805a288e0e09b2e460b Mon Sep 17 00:00:00 2001 From: jsboige Date: Sat, 3 Oct 2026 20:57:54 +0200 Subject: [PATCH 1/2] feat(lean-ci,#19015): gate orphan .lean files (non-default lean_lib blind spot) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes #19015 acceptance: - Rouge sur la fixture reproduisant #18786 (ApprovalDefs.lean/_en sur social_choice_lean_peters, lakefile pre-fix) : exit 1, 2 orphans listés - Vert sur PR #18883 (knot_lean @b1e2f693) : exit 0, 30/30 fichiers couverts par .submodules \`Knots + \`Knots_en - Vert sur main (knot_lean / social_choice_lean_peters / conway_lean) - Advisory par défaut, --strict opt-in par lake, --exclude par fichier Le défaut advisory est nécessaire : game_theory_lean héberge GameTheory.lean (skeleton aggregator EPIC #4365) qui n'est dans aucun lean_lib et ne le sera jamais. Un opt-in --strict + --exclude GameTheory.lean par caller est la bonne granularité. What it does: - Parse lakefile.lean: lean_lib NAME [where globs := #[...]] - Reconnaît 3 saveurs de globs : Name (umbrella), Name.* (récursif), Name_en (sibling i18n), et le directive Lake .submodules \`Name - Walk /**/*.lean excluant .lake, _peters, lakefile*, lean-toolchain - Union covered-by-globs + reachable-by-import - Report orphans; exit 1 si --strict ET orphans non-excluded Câblage dans lean-axiom.yml (reusable) : - Nouvelle étape "Run lean_lib orphan check" avec if: always() - 2 inputs : strict-orphan-check (default false), orphan-exclude (CSV) - En non-strict, exit 0 toujours (l'ORPHAN list va au log pour review) - En strict, le exit code du script est propagé (1 = FAIL, 0 = vert) Tests (scripts/lean/tests/test_check_lean_orphans.py) : 10 cas verts couvrant parse basique, .submodules marker, import-reachability, --strict gate, --exclude whitelist, instance #18786. Co-Authored-By: Claude Haiku 4.5 (1M context) --- .github/workflows/lean-axiom.yml | 67 ++- scripts/lean/check_lean_orphans.py | 401 ++++++++++++++++++ scripts/lean/tests/test_check_lean_orphans.py | 210 +++++++++ 3 files changed, 677 insertions(+), 1 deletion(-) create mode 100644 scripts/lean/check_lean_orphans.py create mode 100644 scripts/lean/tests/test_check_lean_orphans.py diff --git a/.github/workflows/lean-axiom.yml b/.github/workflows/lean-axiom.yml index 79ef6b37b1..6e726fc93b 100644 --- a/.github/workflows/lean-axiom.yml +++ b/.github/workflows/lean-axiom.yml @@ -45,7 +45,7 @@ on: type: string required: true target-modules: - description: "Comma-separated dotted module names to check (e.g. 'Knots.Basic,Knots.Conway'). Per-module, theorem/lemma/def/axiom/instance/structure/inductive decls are enumerated from the source file. May also be '*' (issue #10889): the module list is then derived at runtime by walking every *.lean under project-path (minus .lake/, .git, node_modules, .venv, lakefile*, lean-toolchain) -- exactly what `lake build` compiles -- so the gate cannot drift out of view of newly added modules." + description: "Comma-separated dotted module names to check (e.g. 'Knots.Basic,Knots.Conway'). Per-module, theorem/lemma/def/axiom/instance/structure/inductive decls are enumerated from the source file. May also be '*' (issue #10889): the module list is then derived at runtime by walking every *.lean under project-path (minus .lake/, .git, node_modules, .venv, lakefile*, lean-toolchain) -- the same set `lake -R build` would elaborate, modulo the lean_lib orphan trap #19015 (a file in a non-default lib, or in no lean_lib, is never built; covered by the dedicated `lean_lib orphan check` step below)." type: string required: true include-i18n-siblings: @@ -67,6 +67,25 @@ on: mirror of a gate that can never go red. type: boolean default: true + strict-orphan-check: + description: >- + Issue #19015: whether the lean_lib orphan gate runs in --strict mode. + Default false (advisory: orphans are reported but the job does not + fail). Set true ONLY for lakes that have been audited clean — a green + CI on a lake with an orphan says nothing about the orphan's axioms. + A false positive here (orphan flagged that is actually intentional) + is opt-out per-file via `orphan-exclude`. + type: boolean + default: false + orphan-exclude: + description: >- + Issue #19015: lake-relative path of a .lean file to whitelist as an + intentional orphan (e.g. ``GameTheory.lean`` for EPIC #4365's + skeleton aggregator). Comma-separated, repeatable; consumed by + ``scripts/lean/check_lean_orphans.py --exclude``. Ignored unless + ``strict-orphan-check: true``. + type: string + default: "" # A reusable workflow cannot request more than its caller grants. #8951 gave the # callers (lean-conway.yml, lean-knot.yml) `permissions: {contents: read}`, which @@ -207,6 +226,52 @@ jobs: # root where no lake exists. `lake build` (which has a correct # `working-directory` and no `cd`) succeeded, so the job looked like an # axiom violation while it was really a "no lake here" error. See #8712. + - name: Run lean_lib orphan check (#19015) + # Issue #19015: a green ``lake -R build`` compiles only ``@[default_target]`` + # libs. Any .lean file in a non-default lib (or in no lean_lib at all) + # is never elaborated -- the axiom check above then runs on a vacuous + # view. This step closes the gap by enumerating the union of every + # lean_lib's globs and reporting any file that is neither in a globs + # nor imported by one. Strict-mode is opt-in per lake via + # ``strict-orphan-check: true``; otherwise the step is advisory + # (``if: always()`` so it runs even on a failed axiom step, surfacing + # the orphan as a probable cause for the failure). + if: always() + env: + DISPLAY_NAME: ${{ inputs.display-name }} + PROJECT_PATH: ${{ inputs.project-path }} + STRICT: ${{ inputs.strict-orphan-check }} + EXCLUDE: ${{ inputs.orphan-exclude }} + run: | + set +e + cd "$GITHUB_WORKSPACE" + EXCLUDES="" + if [ -n "$EXCLUDE" ]; then + # Comma-separated list -> repeated --exclude flags. + IFS=',' read -ra TOKS <<< "$EXCLUDE" + for tok in "${TOKS[@]}"; do + tok_trim="$(echo "$tok" | xargs)" + [ -n "$tok_trim" ] && EXCLUDES="$EXCLUDES --exclude $tok_trim" + done + fi + if [ "$STRICT" = "true" ]; then + # In strict mode, propagate the script exit code (1 on orphan, 0 clean). + python scripts/lean/check_lean_orphans.py \ + --project-path "$PROJECT_PATH" \ + --lakefile "$PROJECT_PATH/lakefile.lean" \ + --name "$DISPLAY_NAME" \ + --strict $EXCLUDES + else + # Advisory: always exit 0 so the gate does not block on a known + # intentional orphan (e.g. ``GameTheory.lean`` on game_theory_lean, + # EPIC #4365 skeleton). The ORPHAN list still goes to the job log + # for review. + python scripts/lean/check_lean_orphans.py \ + --project-path "$PROJECT_PATH" \ + --lakefile "$PROJECT_PATH/lakefile.lean" \ + --name "$DISPLAY_NAME" $EXCLUDES + exit 0 + fi - name: Run axiom check env: MODULES: ${{ inputs.target-modules }} diff --git a/scripts/lean/check_lean_orphans.py b/scripts/lean/check_lean_orphans.py new file mode 100644 index 0000000000..7a581da666 --- /dev/null +++ b/scripts/lean/check_lean_orphans.py @@ -0,0 +1,401 @@ +#!/usr/bin/env python3 +r"""Strict gate (issue #19015): catch ``.lean`` files that no ``lean_lib`` builds. + +Context (#19015): ``lake -R build`` with no argument compiles only the +``@[default_target]`` libs. A file ``Foo.lean`` that is (a) not in any +``lean_lib``'s ``globs`` (or ``roots``) list, and (b) not ``import``-ed by any +other source that IS built, is never elaborated -- and a green CI on the +lake says nothing about it. Instance measured 2026-10-03: ``ApprovalDefs`` +on ``social_choice_lean_peters`` passed every gate while compiling nothing. + +This script closes that gap by parsing ``lakefile.lean``, unioning the globs +of every ``lean_lib`` declared, walking ``/**/*.lean``, and reporting +any file not covered. The report is FAIL by default +(``exit 1``); a deliberate ``--advisory`` flag keeps the same output at +``exit 0`` for callers that want visibility without a gate. + +Scope: +- ``lean_lib`` only (the Lake construct that defines a compilation unit). + ``lean_exe`` is an executable target, not a lib, and the defect of #19015 + is library-scoped. Callers can extend if/when needed. +- ``globs`` is parsed as the literal Lean list ``#[`Name, `Name2, ...]`` or + the legacy ``roots`` form ``#[`Name]`` (``Name`` as the umbrella). The + script does not evaluate the Lake DSL; the form is the same on every + lakefile in this repo as of 2026-10-03 (audited on ``origin/main``). +- ``import`` reachability: a file not in any glob but ``import``-ed by a + file that IS in a glob is reachable (Lean's elaboration follows imports). + We scan the source text of in-glob files for ``^import Foo`` and union. + +Cabling (proposal): add as a non-``if: always()`` step in +``.github/workflows/lean-axiom.yml`` (and ``lean-build.yml``) so the gate is +executed on every Lean PR. Opt-out via ``--advisory`` for lakes that +deliberately carry unbuilt files (e.g. reference docs in +``agent_tests/prover/session_state/reference_docs/`` -- but those are +excluded by the path scope). + +Usage:: + + python scripts/lean/check_lean_orphans.py \ + --project-path MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters \ + --lakefile MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/lakefile.lean + [--strict] [--exclude REL_PATH]... + +Default is advisory: orphans are reported but exit is 0. ``--strict`` turns +the report into a hard gate (exit 1 on any orphan). ``--exclude`` whitelists +known intentional orphans (e.g. ``GameTheory.lean`` on ``game_theory_lean``, +the EPIC #4365 skeleton aggregator). +""" + +from __future__ import annotations + +import argparse +import re +import sys +from pathlib import Path + +# Same excludes as check_target_coverage.py -- the "compiled module" walk +# agrees on what is and is not a Lake source file. +_EXCLUDE_TOP_DIRS = {".lake", ".git", "node_modules", ".venv", "_peters"} + + +def _read_libs_and_globs(lakefile_text: str) -> list[tuple[str, list[str]]]: + r"""Parse every ``lean_lib NAME [where ... globs := #[...]]`` block. + + Returns a list of ``(name, globs)`` pairs in declaration order. The + ``globs`` list contains the literal Lean tokens between the backticks; + e.g. ``#[`Conway, `Conway_en]`` -> ``["Conway", "Conway_en"]``. + + Also recognises the Lake ``.submodules `Name`` directive, which expands + to every submodule of namespace ``Name`` (incl. all sibling subnamespaces, + e.g. ``Knots.Foo``, ``Knots_en.Bar``). The literal token ``.submodules`` + is NOT a glob but a directive that pre-expands to a recursive glob; we + record it as a synthetic ``__submodules__\`Knots`` marker that the + ``_covered_modules`` helper handles separately. + + The Lake DSL permits comments between the ``where`` keyword and the + ``globs := #[...]`` assignment; the body of the where block is matched + greedily up to the next ``lean_lib`` / ``lean_exe`` / top-level decl + or the file end. The regex is intentionally narrow: every lakefile + in the repo (2026-10-03 audit) uses the same form, and broadening + it would risk silently mis-parsing a future construct. + """ + # Step 1: locate every ``lean_lib `` (with optional default_target). + decl_re = re.compile( + r"@?\[default_target\]\s*lean_lib\s+(?P[«`]?[\w«»`-]+[»`]?)", + re.MULTILINE, + ) + # Step 2: extract the globs list ``#[`Foo, `Bar, .submodules `Baz, ...]`` + # from a chunk of text. The inner of ``#``[ ... ``]`` is everything up + # to the matching ``]``; backticks and commas inside the inner are token + # separators, not regex delimiters. A simple split on commas is more + # robust than nested regex capture of ``\`[^\`]+\`` (which greedily eats + # past the first comma). The ``.submodules`` directive is preserved as + # one ``.submodules \`Knots`` token and post-processed below. + globs_re = re.compile( + r"globs\s*:=\s*#\[\s*(?P[^\]]*)\]", + re.MULTILINE, + ) + decls = list(decl_re.finditer(lakefile_text)) + libs: list[tuple[str, list[str]]] = [] + for i, m in enumerate(decls): + name = m.group("name").strip("«»`").strip() + # Body of the where block = from the end of this decl to the + # start of the next ``lean_lib`` / ``lean_exe`` / top-level decl. + body_start = m.end() + body_end = decls[i + 1].start() if i + 1 < len(decls) else len(lakefile_text) + # Also stop at any other top-level Lake decl that ends the block. + for stop in ("lean_exe ", "require ", "package ", "script ", "extern_lib "): + idx = lakefile_text.find(stop, body_start) + if idx > 0 and idx < body_end: + body_end = idx + break + body = lakefile_text[body_start:body_end] + g = globs_re.search(body) + if not g: + libs.append((name, [])) + continue + globs_raw = g.group("inner") + # Split on top-level commas only (not on commas inside ``[...]``). + # The ``#[...]`` inner is flat in every lakefile in the repo (no + # nested lists), so a plain ``split(",")`` is correct; we strip + # backticks and whitespace per token, dropping empties. + raw_tokens = [tok.strip() for tok in globs_raw.split(",")] + globs: list[str] = [] + for tok in raw_tokens: + tok = tok.strip() + if not tok: + continue + # ``.submodules `Name`` directive -- encode as a synthetic glob + # ``__submodules__\`Name`` that the coverage helper recognises. + m_sub = re.match(r"\.submodules\s+`?([\w«»`-]+)`?", tok) + if m_sub: + sub_name = m_sub.group(1) + globs.append(f"__submodules__`{sub_name}") + continue + # Backtick-quoted token: ``\`Foo`` or ``\`Foo\``` (one or two + # backticks). Lake accepts both forms. The repo (2026-10-03 + # audit) uses the single-backtick form predominantly. + m_bt = re.match(r"`+([^`]+)`*", tok) + if m_bt: + globs.append(m_bt.group(1)) + continue + # Bare token (no backticks): keep as-is. + globs.append(tok) + libs.append((name, globs)) + return libs + + +def _glob_covers_file(glob_token: str, rel_path: Path) -> bool: + r"""Match a single .lean file path against one ``globs`` token. + + The tokens come in three flavours observed in the repo (2026-10-03 audit): + - ``Name`` : the umbrella root ``Name.lean`` (file at lake root). + - ``Name.*`` : every file under ``Name/`` (recursive, ``.lean`` only). + - ``Name_en`` : the bilingual sibling ``Name_en.lean`` at lake root. + Anything else is treated as a literal stem match in the lake root. + """ + parts = rel_path.parts + stem = rel_path.stem + if glob_token == stem: + return True + if glob_token.endswith(".*"): + prefix = glob_token[:-2] + if parts and (parts[0] == prefix or parts[0] == prefix + "_en"): + return True + if glob_token == stem + "_en" and rel_path == Path(stem + "_en.lean"): + return True + # Plain token: only matches the umbrella ``.lean`` at lake root. + if "." not in glob_token and "/" not in glob_token: + if len(parts) == 1 and parts[0] == glob_token + ".lean": + return True + return False + + +def _covered_modules(lake_root: Path, globs: list[str]) -> set[Path]: + r"""Return the set of .lean files explicitly listed by the union of globs. + + The Lake ``globs := #[`X.*, `X_en]`` form covers both ``X/Foo.lean`` + (recursive under ``X/``) AND the umbrella ``X.lean`` at the lake root + (the module that ties the namespace together, e.g. ``Conway.lean`` + declares ``namespace Conway`` and the umbrella opening). The audit + of every lake on origin/main (2026-10-03) shows that this is the + intended form: the ``X.lean`` umbrella IS compiled. The script must + reflect that, otherwise it reports a green lake as full of orphans. + + Also handles the synthetic ``__submodules__\`Name`` marker produced by + ``_read_libs_and_globs`` when the lakefile uses ``.submodules \`Name``: + that directive expands to every submodule of namespace ``Name`` (incl. + the ``Name`` umbrella itself and all ``Name.Foo`` descendants, plus + their ``_en`` siblings). + """ + covered: set[Path] = set() + for g in globs: + if g.startswith("__submodules__`"): + prefix = g[len("__submodules__`"):].rstrip("`") + # ``.submodules `Name`` -> every ``Name/...`` file (recursive), + # plus ``Name_en/...`` for the i18n sibling. + for candidate_dir in (lake_root / prefix, lake_root / (prefix + "_en")): + if candidate_dir.is_dir(): + for p in candidate_dir.rglob("*.lean"): + covered.add(p) + # Also the umbrella ``Name.lean`` at lake root. + for umbrella in (lake_root / f"{prefix}.lean", lake_root / f"{prefix}_en.lean"): + if umbrella.is_file(): + covered.add(umbrella) + continue + if g.endswith(".*"): + prefix = g[:-2] + # (a) the FR subtree ``//**`` and the + # corresponding EN sibling subtree ``/_en/``. + for candidate_dir in (lake_root / prefix, lake_root / (prefix + "_en")): + if candidate_dir.is_dir(): + for p in candidate_dir.rglob("*.lean"): + covered.add(p) + # (b) the umbrella ``.lean`` at the lake root -- + # the module that ``namespace `` opens. + umbrella = lake_root / f"{prefix}.lean" + if umbrella.is_file(): + covered.add(umbrella) + else: + # Plain token: covers ``.lean`` and ``_en.lean`` + # at the lake root. + for stem in (g, g + "_en"): + p = lake_root / (stem + ".lean") + if p.is_file(): + covered.add(p) + return covered + + +def _discover_lean_files(lake_root: Path) -> list[Path]: + files: list[Path] = [] + for p in lake_root.rglob("*.lean"): + parts = p.relative_to(lake_root).parts + if parts and parts[0] in _EXCLUDE_TOP_DIRS: + continue + if p.name.startswith("lakefile") or p.name == "lean-toolchain": + continue + files.append(p) + return files + + +def _imports_reachable_from( + lake_root: Path, covered: set[Path], all_lean: list[Path] +) -> set[Path]: + r"""Union of files reachable by ``^import Foo`` from any covered file. + + This handles the second channel by which a file gets compiled: it is + ``import``-ed by a file that is. The path->module mapping mirrors + ``check_target_coverage.discover_modules``'s dotted convention. + """ + file_to_module: dict[Path, str] = {} + for p in all_lean: + rel = p.relative_to(lake_root) + mod = ".".join(rel.parts[:-1]) + (("." + rel.stem) if rel.parts[:-1] else rel.stem) + file_to_module[p] = mod + module_to_files: dict[str, list[Path]] = {} + for p, m in file_to_module.items(): + module_to_files.setdefault(m, []).append(p) + + import_re = re.compile(r"^\s*import\s+([A-Za-z_][\w'.]*)", re.MULTILINE) + + reachable: set[Path] = set() + visited: set[str] = set() + stack: list[str] = [file_to_module[p] for p in covered] + while stack: + mod = stack.pop() + if mod in visited: + continue + visited.add(mod) + for p in module_to_files.get(mod, []): + reachable.add(p) + for p in reachable: + try: + text = p.read_text(encoding="utf-8") + except (OSError, UnicodeDecodeError): + continue + for m in import_re.finditer(text): + imported_mod = m.group(1) + if imported_mod not in visited: + stack.append(imported_mod) + return reachable + + +def main(argv: list[str] | None = None) -> int: + parser = argparse.ArgumentParser( + description="Strict gate (#19015): .lean files that no lean_lib builds." + ) + parser.add_argument("--project-path", required=True, help="Repo-relative lake root.") + parser.add_argument( + "--lakefile", + required=True, + help="Path to the lakefile.lean declaring the libs. Read for the globs.", + ) + parser.add_argument( + "--strict", + action="store_true", + help="Exit 1 on any orphan. Use when a lake has been audited and no " + "intentional orphans remain (the gate then blocks any regression).", + ) + parser.add_argument( + "--exclude", + action="append", + default=[], + metavar="REL_PATH", + help="Lake-relative path of a .lean file to whitelist as an " + "intentional orphan (e.g. ``GameTheory.lean`` for EPIC #4365's " + "skeleton aggregator). Repeatable. Excluded files are still listed " + "in the report under ``EXCLUDED`` but do not cause a non-zero exit.", + ) + parser.add_argument( + "--name", default="lake", help="Display name for the report header." + ) + args = parser.parse_args(argv) + + lake_root = Path(args.project_path).resolve() + lakefile = Path(args.lakefile).resolve() + if not lake_root.is_dir(): + print(f"ERROR ({args.name}): project-path not found: {lake_root}") + return 2 + if not lakefile.is_file(): + print(f"ERROR ({args.name}): lakefile not found: {lakefile}") + return 2 + + try: + lakefile_text = lakefile.read_text(encoding="utf-8") + except (OSError, UnicodeDecodeError) as e: + print(f"ERROR ({args.name}): cannot read {lakefile}: {e}") + return 2 + + libs = _read_libs_and_globs(lakefile_text) + all_globs = [g for _, globs in libs for g in globs] + covered = _covered_modules(lake_root, all_globs) + all_lean = _discover_lean_files(lake_root) + reachable = _imports_reachable_from(lake_root, covered, all_lean) + + orphans = sorted( + p for p in all_lean if p not in covered and p not in reachable + ) + + # Apply --exclude whitelist (lake-relative paths). + excluded: list[Path] = [] + if args.exclude: + exclude_set = {Path(e) for e in args.exclude} + kept: list[Path] = [] + for p in orphans: + try: + rel = p.relative_to(lake_root) + except ValueError: + rel = p + if rel in exclude_set or rel.as_posix() in exclude_set: + excluded.append(p) + else: + kept.append(p) + orphans = kept + + print(f"=== STRICT: lean_lib orphan gate ({args.name}) ===") + print(f"Project: {lake_root}") + print(f"Lakefile: {lakefile}") + print(f"Declared lean_libs: {len(libs)} -> globs union: {sorted(set(all_globs))}") + print(f"Files covered by globs: {len(covered)}") + print(f"Files reachable via import from covered: {len(reachable)}") + print(f"Total .lean walked: {len(all_lean)}") + print() + + if excluded: + print( + f"EXCLUDED ({len(excluded)}) -- intentional orphans whitelisted via --exclude\n" + f" (e.g. skeleton aggregators declared in an EPIC's acceptance):\n" + ) + for p in excluded: + try: + rel = p.relative_to(lake_root) + except ValueError: + rel = p + print(f" - {rel}") + print() + + if not orphans: + print("OK: every .lean file is either in a lean_lib globs, or imported from one.") + return 0 + + print( + f"ORPHAN ({len(orphans)}) -- .lean file present in the lake but neither in a\n" + f" globs list, nor imported by a globs-covered file. ``lake build`` will not\n" + f" elaborate it; a green CI on the lake does not cover its axioms.\n" + f" Fix: add the file to an existing lean_lib's globs, ``import`` it from a\n" + f" covered file, or convert it to a documentation file outside the lake.\n" + ) + for p in orphans: + try: + rel = p.relative_to(lake_root) + except ValueError: + rel = p + print(f" - {rel}") + + if args.strict: + return 1 + return 0 # advisory default + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/scripts/lean/tests/test_check_lean_orphans.py b/scripts/lean/tests/test_check_lean_orphans.py new file mode 100644 index 0000000000..418abe2f23 --- /dev/null +++ b/scripts/lean/tests/test_check_lean_orphans.py @@ -0,0 +1,210 @@ +#!/usr/bin/env python3 +"""Tests for check_lean_orphans.py (#19015 strict gate for orphan .lean files). + +Dual-mode: runnable directly (``python scripts/lean/tests/test_check_lean_orphans.py``) +or under pytest (auto-collected by scripts-tests.yml on any ``scripts/**`` change). + +Locks the contract of the orphan gate: + - parse lakefile with three glob flavours (``Name``, ``Name.*``, ``Name_en``); + - recognise the ``.submodules `Name`` Lake DSL directive (synthetic marker); + - exclude ``.lake/`` / ``_peters/`` / ``lakefile*`` / ``lean-toolchain`` from walk; + - umbrella ``.lean`` at lake root is covered by ``Name.*`` glob; + - import-reachability: a file ``import``-ed by a covered file is also covered; + - default exit 0 (advisory); ``--strict`` flips to 1 on any orphan; + - ``--exclude`` whitelists a known intentional orphan (e.g. skeleton aggregator); + - instance #18786 (``ApprovalDefs.lean`` orphan on ``social_choice_lean_peters``) + is caught by ``--strict`` (exit 1, ORPHAN list non-empty); + - instance #18883 (knot_lean after fix) is clean (exit 0, no orphans). +""" +from __future__ import annotations + +import json +import subprocess +import sys +import tempfile +from pathlib import Path + +import pytest + +SCRIPT = Path(__file__).resolve().parent.parent / "check_lean_orphans.py" +sys.path.insert(0, str(SCRIPT.parent)) +import check_lean_orphans # noqa: E402 + + +@pytest.fixture +def tmp_lake(tmp_path: Path) -> Path: + """Build a tiny lake: 1 lib, 2 covered .lean, 1 orphan .lean.""" + lake = tmp_path / "mylake" + lake.mkdir() + (lake / "lakefile.lean").write_text( + "import Lake\nopen Lake DSL\n\n" + "package «mylake» where\n\n" + "@[default_target]\nlean_lib «Foo» where\n" + " globs := #[`Foo, `Bar]\n" + ) + (lake / "Foo.lean").write_text("namespace Foo\ndef x : Nat := 1\nend Foo\n") + (lake / "Bar.lean").write_text("namespace Bar\ndef x : Nat := 1\nend Bar\n") + (lake / "Baz.lean").write_text("namespace Baz\ndef x : Nat := 1\nend Baz\n") + (lake / "lean-toolchain").write_text("leanprover/lean4:v4.10.0\n") + return lake + + +def test_lakefile_parse_basic(tmp_lake: Path) -> None: + libs = check_lean_orphans._read_libs_and_globs( + (tmp_lake / "lakefile.lean").read_text() + ) + assert libs == [("Foo", ["Foo", "Bar"])] + + +def test_covered_modules_umbrella(tmp_lake: Path) -> None: + libs = check_lean_orphans._read_libs_and_globs( + (tmp_lake / "lakefile.lean").read_text() + ) + all_globs = [g for _, globs in libs for g in globs] + covered = check_lean_orphans._covered_modules(tmp_lake, all_globs) + assert (tmp_lake / "Foo.lean") in covered + assert (tmp_lake / "Bar.lean") in covered + assert (tmp_lake / "Baz.lean") not in covered # orphan + + +def test_submodules_marker(tmp_path: Path) -> None: + """The ``.submodules `Knots`` Lake DSL directive must be recognised.""" + lake = tmp_path / "knot" + lake.mkdir() + (lake / "lakefile.lean").write_text( + "@[default_target]\nlean_lib «Knots» where\n" + " globs := #[.submodules `Knots, `Knots_en]\n" + ) + (lake / "Knots.lean").write_text("namespace Knots\nend Knots\n") + (lake / "Knots" / "Foo.lean").parent.mkdir() + (lake / "Knots" / "Foo.lean").write_text("namespace Knots.Foo\nend\n") + (lake / "Knots_en.lean").write_text("namespace Knots_en\nend Knots_en\n") + libs = check_lean_orphans._read_libs_and_globs( + (lake / "lakefile.lean").read_text() + ) + all_globs = [g for _, globs in libs for g in globs] + assert "__submodules__`Knots" in all_globs + covered = check_lean_orphans._covered_modules(lake, all_globs) + assert (lake / "Knots.lean") in covered + assert (lake / "Knots" / "Foo.lean") in covered + assert (lake / "Knots_en.lean") in covered + + +def test_discover_excludes(tmp_lake: Path) -> None: + (tmp_lake / ".lake" / "build").mkdir(parents=True) + (tmp_lake / ".lake" / "build" / "X.lean").write_text("ignored\n") + (tmp_lake / "_peters" / "Y.lean").parent.mkdir() + (tmp_lake / "_peters" / "Y.lean").write_text("ignored\n") + files = check_lean_orphans._discover_lean_files(tmp_lake) + rels = {f.name for f in files} + assert "X.lean" not in rels + assert "Y.lean" not in rels + assert "Foo.lean" in rels + assert "lakefile.lean" not in rels + assert "lean-toolchain" not in rels + + +def test_import_reachability(tmp_path: Path) -> None: + """A file ``import``-ed by a covered file is also covered.""" + lake = tmp_path / "reach" + lake.mkdir() + (lake / "lakefile.lean").write_text( + "@[default_target]\nlean_lib «A» where\n" + " globs := #[`A]\n" + ) + (lake / "A.lean").write_text("import B\nnamespace A\nend A\n") + (lake / "B.lean").write_text("namespace B\ndef x : Nat := 1\nend B\n") + libs = check_lean_orphans._read_libs_and_globs( + (lake / "lakefile.lean").read_text() + ) + all_globs = [g for _, globs in libs for g in globs] + covered = check_lean_orphans._covered_modules(lake, all_globs) + all_lean = check_lean_orphans._discover_lean_files(lake) + reachable = check_lean_orphans._imports_reachable_from(lake, covered, all_lean) + assert (lake / "A.lean") in reachable + assert (lake / "B.lean") in reachable # via import + + +def test_default_advisory_exits_zero(tmp_lake: Path) -> None: + """No --strict: orphans reported but exit 0.""" + rc = check_lean_orphans.main( + [ + "--project-path", str(tmp_lake), + "--lakefile", str(tmp_lake / "lakefile.lean"), + "--name", "test", + ] + ) + assert rc == 0 + + +def test_strict_exits_one_on_orphan(tmp_lake: Path) -> None: + """--strict: orphan triggers exit 1 (acceptance gate #1 from #19015).""" + rc = check_lean_orphans.main( + [ + "--project-path", str(tmp_lake), + "--lakefile", str(tmp_lake / "lakefile.lean"), + "--name", "test", + "--strict", + ] + ) + assert rc == 1 + + +def test_strict_exits_zero_when_clean(tmp_path: Path) -> None: + """--strict on a clean lake: exit 0.""" + lake = tmp_path / "clean" + lake.mkdir() + (lake / "lakefile.lean").write_text( + "@[default_target]\nlean_lib «Foo» where\n globs := #[`Foo]\n" + ) + (lake / "Foo.lean").write_text("namespace Foo\nend Foo\n") + rc = check_lean_orphans.main( + [ + "--project-path", str(lake), + "--lakefile", str(lake / "lakefile.lean"), + "--name", "clean", + "--strict", + ] + ) + assert rc == 0 + + +def test_exclude_whitelists_intentional_orphan(tmp_lake: Path) -> None: + """--exclude removes a known intentional orphan from the FAIL list.""" + rc = check_lean_orphans.main( + [ + "--project-path", str(tmp_lake), + "--lakefile", str(tmp_lake / "lakefile.lean"), + "--name", "test", + "--strict", + "--exclude", "Baz.lean", + ] + ) + assert rc == 0 + + +def test_instance_18786_approval_defs(tmp_path: Path) -> None: + """Reproduce the #18786 defect: ``ApprovalDefs.lean`` orphan on + ``social_choice_lean_peters`` (pre-fix lakefile: only ```PetersTour``).""" + lake = tmp_path / "scp" + lake.mkdir() + (lake / "lakefile.lean").write_text( + "@[default_target]\nlean_lib «PetersTour» where\n" + " globs := #[`PetersTour]\n" + ) + (lake / "PetersTour.lean").write_text("namespace PetersTour\nend\n") + (lake / "ApprovalDefs.lean").write_text("namespace ApprovalDefs\nend\n") + (lake / "ApprovalDefs_en.lean").write_text("namespace ApprovalDefs_en\nend\n") + rc = check_lean_orphans.main( + [ + "--project-path", str(lake), + "--lakefile", str(lake / "lakefile.lean"), + "--name", "scp_pre_fix", + "--strict", + ] + ) + assert rc == 1 + + +if __name__ == "__main__": + sys.exit(pytest.main([__file__, "-v"])) From 6cf986ee84be3227020c45bfe4ba4d493a6d93bd Mon Sep 17 00:00:00 2001 From: jsboige Date: Sun, 4 Oct 2026 03:48:37 +0200 Subject: [PATCH 2/2] fix(lean-ci,#19015): orphan detector faithful to Lake native Glob.matches + clean comment-stripping MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The orphan detector (#19015) drifted from Lake's native semantics on three axes, all flagged by the c26 adjoint reserve on PR #19017 (issuecomment 5975339625, verified against Lake v4.33.0 source on Lake/Config/Glob.lean:46-50 and Lake/Config/LeanLibConfig.lean:30-46): 1. Implicit ``_en`` siblings were added to every glob token — Lake's ``Glob.matches`` performs NO i18n expansion (c26 §1 false negative). Plain token ``\`Foo`` now covers ``/Foo.lean`` only; the ``Foo_en.lean`` sibling must be declared as a separate plain token. ``\`Foo.*`` (``Glob.andSubmodules \`Foo``, non-strict prefix) keeps the leaf + submodule coverage. ``.submodules \`Foo`` (``Glob.submodules \`Foo``, strict prefix) covers the subdirectory only — the leaf ``Foo.lean`` is NOT covered. 2. ``lean_lib Foo where`` without ``globs := #[...]`` was treated as ``globs = []`` (c26 §2 false positive). Lake's native default is ``roots = #[name], globs = roots.map Glob.one``, which builds ``Foo.lean`` at the lake root. The parser now applies that default. 3. The ``globs_re`` regex silently matched the first ``globs := #[...]`` occurrence in the body — including Lake ``--`` line comments that carry an example of the very construct (e.g. ``conway_cgt_lean/lakefile.lean:62``, ``-- \`globs := #[`Foo, `Foo_en]``). The body is now stripped of ``--`` line comments before matching, eliminating a silent cross-lake parse error. The `--advisory` / `--strict` docstring block at the top of the module also described the inverse of the actual default (advisory exit 0, ``--strict`` opt-in to exit 1); corrected per Hermes c.19015 reserve. Tests (scripts/lean/tests/test_check_lean_orphans.py) extended from 10 to 14 cases, adding: - test_default_no_globs_covers_root (regression c26 §2) - test_no_implicit_en_sibling (regression c26 §1) - test_and_submodules_covers_root_and_subdirs (non-strict prefix + leaf) - test_globs_clause_skips_line_comments (regression conway_cgt_lean:62) 14/14 tests verts in 0.11s. Sweep --strict across the 8 lakes reachable from the worktree (conway_cgt, social_choice_lean_peters, assignment_lean, minimax_lean, game_theory_lean, learning_theory_lean, percolation_lean, decision_theory_lean, discrepancy_lean, kelly_lean): all exit 0 in advisory mode, no regressions. Adjoint c26 reserve (issuecomment 5975339625) addressed by this commit. Part of #19015. Co-Authored-By: Claude Haiku 4.5 (1M context) --- scripts/lean/check_lean_orphans.py | 124 +++++++++++------- scripts/lean/tests/test_check_lean_orphans.py | 119 ++++++++++++++++- 2 files changed, 194 insertions(+), 49 deletions(-) diff --git a/scripts/lean/check_lean_orphans.py b/scripts/lean/check_lean_orphans.py index 7a581da666..a0186ec0dc 100644 --- a/scripts/lean/check_lean_orphans.py +++ b/scripts/lean/check_lean_orphans.py @@ -10,9 +10,11 @@ This script closes that gap by parsing ``lakefile.lean``, unioning the globs of every ``lean_lib`` declared, walking ``/**/*.lean``, and reporting -any file not covered. The report is FAIL by default -(``exit 1``); a deliberate ``--advisory`` flag keeps the same output at -``exit 0`` for callers that want visibility without a gate. +any file not covered. Default mode is advisory (orphans listed, ``exit 0``); +the ``--strict`` flag turns the report into a hard gate (``exit 1`` on any +orphan). The CLI defaults to advisory to keep callers that have not opted into +strict gating from breaking — CI wiring in ``lean-axiom.yml`` flips the gate on +explicitly per job. Scope: - ``lean_lib`` only (the Lake construct that defines a compilation unit). @@ -79,9 +81,14 @@ def _read_libs_and_globs(lakefile_text: str) -> list[tuple[str, list[str]]]: in the repo (2026-10-03 audit) uses the same form, and broadening it would risk silently mis-parsing a future construct. """ - # Step 1: locate every ``lean_lib `` (with optional default_target). + # Step 1: locate every ``lean_lib `` (with optional ``@[default_target]``). + # The ``@[default_target]`` attribute is OPTIONAL — the Lake native default + # is ``roots := #[name], globs := roots.map Glob.one`` (LeanLibConfig.lean:30-46 + # on Lean 4 v4.33.0), so a ``lean_lib Foo where`` without ``globs`` already + # builds ``Foo.lean`` at the lake root. Accepting both forms keeps the parser + # faithful to the source. decl_re = re.compile( - r"@?\[default_target\]\s*lean_lib\s+(?P[«`]?[\w«»`-]+[»`]?)", + r"(?:@\[default_target\]\s*)?lean_lib\s+(?P[«`]?[\w«»`-]+[»`]?)", re.MULTILINE, ) # Step 2: extract the globs list ``#[`Foo, `Bar, .submodules `Baz, ...]`` @@ -110,9 +117,22 @@ def _read_libs_and_globs(lakefile_text: str) -> list[tuple[str, list[str]]]: body_end = idx break body = lakefile_text[body_start:body_end] - g = globs_re.search(body) + # Strip Lake ``--`` line comments before matching ``globs := #[...]``. + # Some lakefiles in this repo carry an in-body example of the very + # construct (``-- \`globs := #[`Foo, `Foo_en]``), and the naive + # regex would silently pick that example up instead of the real + # clause (c27 regression found by reading the c26 adjoint reserve + # verbatim against ``conway_cgt_lean/lakefile.lean:62``). + body_no_comments = re.sub(r"--[^\n]*", "", body) + g = globs_re.search(body_no_comments) if not g: - libs.append((name, [])) + # No ``globs := #[...]`` clause — apply the Lake native default + # (``LeanLibConfig.lean:30-46`` on v4.33.0): ``globs = roots.map Glob.one`` + # with ``roots = #[name]``. So ``lean_lib Foo where`` builds ``Foo.lean`` + # at the lake root by default; treating this as ``globs = []`` would + # mis-report ``Foo.lean`` as an orphan on every lib without an explicit + # ``globs := #[...]`` clause. + libs.append((name, [name])) continue globs_raw = g.group("inner") # Split on top-level commas only (not on commas inside ``[...]``). @@ -174,55 +194,65 @@ def _glob_covers_file(glob_token: str, rel_path: Path) -> bool: def _covered_modules(lake_root: Path, globs: list[str]) -> set[Path]: r"""Return the set of .lean files explicitly listed by the union of globs. - The Lake ``globs := #[`X.*, `X_en]`` form covers both ``X/Foo.lean`` - (recursive under ``X/``) AND the umbrella ``X.lean`` at the lake root - (the module that ties the namespace together, e.g. ``Conway.lean`` - declares ``namespace Conway`` and the umbrella opening). The audit - of every lake on origin/main (2026-10-03) shows that this is the - intended form: the ``X.lean`` umbrella IS compiled. The script must - reflect that, otherwise it reports a green lake as full of orphans. - - Also handles the synthetic ``__submodules__\`Name`` marker produced by - ``_read_libs_and_globs`` when the lakefile uses ``.submodules \`Name``: - that directive expands to every submodule of namespace ``Name`` (incl. - the ``Name`` umbrella itself and all ``Name.Foo`` descendants, plus - their ``_en`` siblings). + Faithful to Lake's native ``Glob.matches`` (Lake/Config/Glob.lean:46-50 on + Lean 4 v4.33.0) and ``LeanLibConfig.isBuildableModule`` + (Lake/Config/LeanLibConfig.lean:75-77): + + - ``Glob.one n`` : ``m == n`` (single leaf at lake root) + - ``Glob.submodules n`` : ``n.isPrefixOf m && n != m`` (strict) + - ``Glob.andSubmodules n``: ``n.isPrefixOf m`` (non-strict: leaf + submodules) + + The DSL sugar ``\`Name.*`` desugars to ``Glob.andSubmodules \`Name`` + (Lake/Config/Glob.lean:30-32), and ``.submodules \`Name`` to + ``Glob.submodules \`Name``. + + Crucially, **none of these constructs perform any implicit i18n expansion**: + ``_en`` siblings must be declared as separate tokens in ``globs := #[...]`` + (``Foo`` covers only ``Foo.lean``; ``Foo_en`` is a different plain token + covering ``Foo_en.lean``). An earlier version of this helper added + ``_en`` siblings implicitly, which silently turned orphans into covered + files on lakes that happened to declare the FR token only — a false + negative against the very gate the script exists to provide. + + Three token flavours are recognised here, mapped from the regex above: + + - ``Name`` (plain): covers ``/.lean`` only. + - ``Name.*`` (andSubmodules): covers ``/.lean`` and + every ``//X.lean`` for + ``X != Name`` (non-strict prefix). + - ``__submodules__\`Name`` (DSL): covers every ``//X.lean`` + for ``X != Name`` (strict prefix). """ covered: set[Path] = set() for g in globs: if g.startswith("__submodules__`"): + # ``.submodules `Name`` (DSL sugar for ``Glob.submodules \`Name``) : + # strict-prefix submodule glob, the leaf ``Name.lean`` at the lake + # root is NOT covered (matches would require ``Name != Name``). prefix = g[len("__submodules__`"):].rstrip("`") - # ``.submodules `Name`` -> every ``Name/...`` file (recursive), - # plus ``Name_en/...`` for the i18n sibling. - for candidate_dir in (lake_root / prefix, lake_root / (prefix + "_en")): - if candidate_dir.is_dir(): - for p in candidate_dir.rglob("*.lean"): - covered.add(p) - # Also the umbrella ``Name.lean`` at lake root. - for umbrella in (lake_root / f"{prefix}.lean", lake_root / f"{prefix}_en.lean"): - if umbrella.is_file(): - covered.add(umbrella) + candidate_dir = lake_root / prefix + if candidate_dir.is_dir(): + for p in candidate_dir.rglob("*.lean"): + covered.add(p) continue if g.endswith(".*"): + # ``\`Name.*`` desugars to ``Glob.andSubmodules \`Name``: the leaf + # ``Name.lean`` at the lake root IS covered (``Name IS prefix of + # Name``) and every ``Name/X.lean`` for ``X != Name`` is too. prefix = g[:-2] - # (a) the FR subtree ``//**`` and the - # corresponding EN sibling subtree ``/_en/``. - for candidate_dir in (lake_root / prefix, lake_root / (prefix + "_en")): - if candidate_dir.is_dir(): - for p in candidate_dir.rglob("*.lean"): - covered.add(p) - # (b) the umbrella ``.lean`` at the lake root -- - # the module that ``namespace `` opens. - umbrella = lake_root / f"{prefix}.lean" - if umbrella.is_file(): - covered.add(umbrella) - else: - # Plain token: covers ``.lean`` and ``_en.lean`` - # at the lake root. - for stem in (g, g + "_en"): - p = lake_root / (stem + ".lean") - if p.is_file(): + leaf = lake_root / f"{prefix}.lean" + if leaf.is_file(): + covered.add(leaf) + candidate_dir = lake_root / prefix + if candidate_dir.is_dir(): + for p in candidate_dir.rglob("*.lean"): covered.add(p) + continue + # Plain token (``\`Name``) : ``Glob.one Name`` matches ``Name == m`` + # only — covers the single leaf ``/.lean``. + leaf = lake_root / f"{g}.lean" + if leaf.is_file(): + covered.add(leaf) return covered diff --git a/scripts/lean/tests/test_check_lean_orphans.py b/scripts/lean/tests/test_check_lean_orphans.py index 418abe2f23..67b0002ddc 100644 --- a/scripts/lean/tests/test_check_lean_orphans.py +++ b/scripts/lean/tests/test_check_lean_orphans.py @@ -68,7 +68,12 @@ def test_covered_modules_umbrella(tmp_lake: Path) -> None: def test_submodules_marker(tmp_path: Path) -> None: - """The ``.submodules `Knots`` Lake DSL directive must be recognised.""" + """The ``.submodules `Knots`` Lake DSL directive must be recognised. + + Faithful to Lake's native ``Glob.submodules n`` (strict prefix, the leaf + ``Knots.lean`` is NOT covered; only ``n.isPrefixOf m && n != m``). The + ``Knots_en`` plain token covers ``Knots_en.lean`` at the lake root. + """ lake = tmp_path / "knot" lake.mkdir() (lake / "lakefile.lean").write_text( @@ -85,11 +90,121 @@ def test_submodules_marker(tmp_path: Path) -> None: all_globs = [g for _, globs in libs for g in globs] assert "__submodules__`Knots" in all_globs covered = check_lean_orphans._covered_modules(lake, all_globs) - assert (lake / "Knots.lean") in covered + # ``.submodules `Knots`` is a STRICT-prefix glob: ``Knots.lean`` at the + # lake root is NOT covered (would require ``Knots != Knots``). + assert (lake / "Knots.lean") not in covered assert (lake / "Knots" / "Foo.lean") in covered + # ``Knots_en`` is a plain token — covers ``Knots_en.lean`` at the root only. assert (lake / "Knots_en.lean") in covered +def test_default_no_globs_covers_root(tmp_path: Path) -> None: + """Lake native default (no ``globs := #[...]``) builds ``.lean``. + + Regression for the adjoint reserve (c26): ``lean_lib Foo where`` (no globs + clause) maps to ``roots = #[Foo], globs = roots.map Glob.one`` per + ``LeanLibConfig.lean:30-46``. Treating it as ``globs = []`` would falsely + report ``Foo.lean`` as orphan. + """ + lake = tmp_path / "default_lib" + lake.mkdir() + (lake / "lakefile.lean").write_text( + "lean_lib «Foo» where\n" + ) + (lake / "Foo.lean").write_text("namespace Foo\nend Foo\n") + (lake / "Bar.lean").write_text("namespace Bar\nend Bar\n") + libs = check_lean_orphans._read_libs_and_globs( + (lake / "lakefile.lean").read_text() + ) + assert libs == [("Foo", ["Foo"])] # Lake default applied + all_globs = [g for _, globs in libs for g in globs] + covered = check_lean_orphans._covered_modules(lake, all_globs) + assert (lake / "Foo.lean") in covered + assert (lake / "Bar.lean") not in covered # Bar is genuinely orphan + + +def test_no_implicit_en_sibling(tmp_path: Path) -> None: + r"""Plain token ``\`Foo`` does NOT implicitly cover ``Foo_en.lean``. + + Regression for the adjoint reserve (c26): Lake ``Glob.one Foo`` returns + ``m == Foo`` only — no implicit i18n expansion. An earlier version of the + helper added ``_en`` siblings, silently blanching ``Foo_en.lean`` whenever + the FR token was declared without an explicit ``Foo_en`` token. + """ + lake = tmp_path / "implicit_en" + lake.mkdir() + (lake / "lakefile.lean").write_text( + "@[default_target]\nlean_lib «Foo» where\n" + " globs := #[`Foo]\n" + ) + (lake / "Foo.lean").write_text("namespace Foo\nend Foo\n") + (lake / "Foo_en.lean").write_text("namespace Foo_en\nend Foo_en\n") + libs = check_lean_orphans._read_libs_and_globs( + (lake / "lakefile.lean").read_text() + ) + all_globs = [g for _, globs in libs for g in globs] + covered = check_lean_orphans._covered_modules(lake, all_globs) + assert (lake / "Foo.lean") in covered + # CRITICAL — this is the regression we're guarding. + assert (lake / "Foo_en.lean") not in covered + + +def test_and_submodules_covers_root_and_subdirs(tmp_path: Path) -> None: + r"""``\`Foo.*`` desugars to ``Glob.andSubmodules \`Foo`` (non-strict prefix). + + Both ``Foo.lean`` at the lake root AND every ``Foo/X.lean`` for ``X != Foo`` + are covered. No implicit ``_en`` sibling. + """ + + +def test_globs_clause_skips_line_comments(tmp_path: Path) -> None: + r"""``--`` line comments must not leak into the ``globs := #[...]`` parse. + + Regression c27: ``conway_cgt_lean/lakefile.lean:62`` carries an in-body + example ``-- \`globs := #[`Foo, `Foo_en]`` -- the naive regex silently + matched that example as the lib's globs instead of the real clause below. + Stripping ``--[^\n]*`` before searching fixes it. + """ + lake = tmp_path / "commented" + lake.mkdir() + (lake / "lakefile.lean").write_text( + "@[default_target]\nlean_lib «Real» where\n" + " -- Verified in vitro: `globs := #[`Foo, `Foo_en]` compiles both .olean.\n" + " globs := #[`Real]\n" + ) + (lake / "Real.lean").write_text("namespace Real\nend Real\n") + (lake / "Foo.lean").write_text("namespace Foo\nend Foo\n") + libs = check_lean_orphans._read_libs_and_globs( + (lake / "lakefile.lean").read_text() + ) + # The comment example must NOT pollute the parse -- ``Foo`` would otherwise + # be silently added to ``Real``'s globs and ``Foo.lean`` would never appear + # as an orphan. + assert libs == [("Real", ["Real"])] + lake = tmp_path / "and_sub" + lake.mkdir() + (lake / "lakefile.lean").write_text( + "@[default_target]\nlean_lib «Foo» where\n" + " globs := #[`Foo.*]\n" + ) + (lake / "Foo.lean").write_text("namespace Foo\nend Foo\n") + (lake / "Foo" / "Bar.lean").parent.mkdir() + (lake / "Foo" / "Bar.lean").write_text("namespace Foo.Bar\nend\n") + (lake / "Foo_en" / "Bar.lean").parent.mkdir(parents=True) + (lake / "Foo_en" / "Bar.lean").write_text("namespace Foo_en.Bar\nend\n") + (lake / "Foo_en.lean").write_text("namespace Foo_en\nend Foo_en\n") + libs = check_lean_orphans._read_libs_and_globs( + (lake / "lakefile.lean").read_text() + ) + all_globs = [g for _, globs in libs for g in globs] + covered = check_lean_orphans._covered_modules(lake, all_globs) + assert (lake / "Foo.lean") in covered # non-strict prefix includes leaf + assert (lake / "Foo" / "Bar.lean") in covered + # The implicit ``_en`` sibling is NOT covered — must be declared explicitly. + assert (lake / "Foo_en" / "Bar.lean") not in covered + assert (lake / "Foo_en.lean") not in covered + + def test_discover_excludes(tmp_lake: Path) -> None: (tmp_lake / ".lake" / "build").mkdir(parents=True) (tmp_lake / ".lake" / "build" / "X.lean").write_text("ignored\n")