diff --git a/.github/CODE_QUALITY.md b/.github/CODE_QUALITY.md index c251a113a9..229de263a0 100644 --- a/.github/CODE_QUALITY.md +++ b/.github/CODE_QUALITY.md @@ -18,6 +18,15 @@ Lean Pool uses deterministic CI for mechanical quality checks and LLM review for The Lean workflow runs on Lean, Lake, project metadata, quality-checker, and workflow changes. It restores and saves Lake caches and pulls Mathlib oleans with `lake exe cache get` when the cache is cold. +Lean Pool uses one `public import LeanPool..Imports` per project in +`LeanPool.lean`. Each generated `LeanPool//Imports.lean` publicly imports +the original project entry module and every source under that project, exactly +once and in sorted order. It contains only imports; keep mathematical declarations +and project cards in the existing source files. Run `lake exe mk_all --module` +after adding, removing or moving a source, and commit the project aggregate as +well as the pool index. The quality linter and `mk_all --check` verify complete +public coverage at both levels. The 10,000-line limit still applies to every file. + The generated module-system indexes import every library file, so building them rejects any file missing a `module` header. Regenerate the indexes with `lake exe mk_all --module`. Package-level `requiresModuleSystem = true` also makes Lake warn when a legacy file imports Lean Pool. ### 2. Repository Quality Checker diff --git a/.github/workflows/auto-rebase.yml b/.github/workflows/auto-rebase.yml index f553455e47..f7aa421748 100644 --- a/.github/workflows/auto-rebase.yml +++ b/.github/workflows/auto-rebase.yml @@ -149,11 +149,11 @@ jobs: --base /tmp/base.yml --ours /tmp/ours.yml --theirs /tmp/theirs.yml) git add LeanPool/projects.yml fi - if grep -qx 'LeanPool.lean' conflicts.txt; then + if grep -Eq '^LeanPool(\.lean|/[^/]+/Imports\.lean)$' conflicts.txt; then # Regenerated from the file tree, so the conflict markers sitting # in the checked-out index file are irrelevant. (cd python && uv run python -m lean_pool.rebase index --repo ..) - git add LeanPool.lean + git add LeanPool.lean LeanPool/ fi if git diff --name-only --diff-filter=U | grep -q .; then @@ -168,8 +168,8 @@ jobs: # The index must be correct even when it did not conflict: main may # have added modules this branch has never seen. (cd python && uv run python -m lean_pool.rebase index --repo ..) - if ! git diff --quiet -- LeanPool.lean; then - git add LeanPool.lean + if ! git diff --quiet -- LeanPool.lean LeanPool/; then + git add LeanPool.lean LeanPool/ git commit -m "Regenerate the module index" echo "result=resolved" >> "$GITHUB_OUTPUT" fi diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 33cf9f1382..8a401dcf3e 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -11,7 +11,7 @@ If you would like to withdraw your project from Lean Pool, open an issue. There are two paths: - **Propose a repo.** Open an issue with the GitHub URL and a maintainer can import it. Repos that Reservoir does not index can be added to [`candidates/manual.txt`](candidates/manual.txt). -- **Open a content PR.** Add your project under `LeanPool//`, register it in [`LeanPool/projects.yml`](LeanPool/projects.yml) — the card must declare `provenance` (`human`, `AI`, or `mix`; see below) — and regenerate the index with `lake exe mk_all`. +- **Open a content PR.** Add your project under `LeanPool//`, register it in [`LeanPool/projects.yml`](LeanPool/projects.yml) — the card must declare `provenance` (`human`, `AI`, or `mix`; see below) — and regenerate the indexes with `lake exe mk_all`. Commit `LeanPool//Imports.lean`, which publicly imports every project source, and the single project import added to `LeanPool.lean`. Either way the result must pass CI (build, linters, and quality checks — see [Linting and testing](#linting-and-testing)) and an [LLM review](.github/REVIEW_RULES.md) of fit and significance. Accepted projects must be `sorry`-free, introduce no axioms beyond `Classical.choice`/`propext`/`Quot.sound`, and avoid `unsafe`/`partial`. Each project card must also declare its **provenance** — who wrote the Lean proofs — as `human` (written by people), `AI` (mostly produced by an AI system), or `mix` (both contributed substantially). (Proof profiling via `/profile` is available but informational, not a gate: added files get an absolute profile, while modified files get a base→head compile-cost comparison — useful for checking that a refactor doesn't regress compile time.) diff --git a/lakefile.toml b/lakefile.toml index 5d42a2eff4..9920af1daa 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -30,3 +30,8 @@ name = "Challenge" # the check independent of the statement file. [[lean_lib]] name = "Solution" + +[[lean_exe]] +name = "mk_all" +root = "ProjectIndexes" +srcDir = "scripts" diff --git a/python/lean_pool/indexes.py b/python/lean_pool/indexes.py new file mode 100644 index 0000000000..6b5c9dfb14 --- /dev/null +++ b/python/lean_pool/indexes.py @@ -0,0 +1,172 @@ +"""Generate and validate complete project aggregates without a Lean toolchain.""" + +from __future__ import annotations + +import argparse +import re +import sys +import tomllib +from pathlib import Path + +from lean_pool.exposition.source_text import code_view + +MODULE_HEADER = "module -- shake: keep-all --deprecated_module: ignore\n\n" +AGGREGATE_NAME = "Imports.lean" +GENERATED_MARKER = "-- Generated project imports; run `lake exe mk_all`.\n" +AGGREGATE_HEADER = ( + "/-\nCopyright (c) 2026 Lean Pool contributors. All rights reserved.\n" + "Released under Apache 2.0 license as described in the file LICENSE.\n" + "Authors: Lean Pool contributors\n-/\n" + MODULE_HEADER + GENERATED_MARKER +) +# Removed after the separate content migration has landed. +REQUIRE_PROJECT_ROOTS = False + + +def project_modules(root: Path) -> dict[str, list[str]]: + """Group all source modules by their first component below LeanPool.""" + pool = root / "LeanPool" + projects: dict[str, list[str]] = {} + for path in sorted(pool.rglob("*.lean")): + relative = path.relative_to(pool) + if len(relative.parts) == 2 and path.name == AGGREGATE_NAME: + continue + project = relative.parts[0].removesuffix(".lean") + module = "LeanPool." + ".".join(relative.with_suffix("").parts) + projects.setdefault(project, []).append(module) + return {project: sorted(modules) for project, modules in sorted(projects.items())} + + +def has_project_roots(root: Path) -> bool: + """Detect the migrated layout, including a damaged or conflicted index.""" + return any((root / "LeanPool").glob(f"*/{AGGREGATE_NAME}")) + + +def requires_project_roots(root: Path) -> bool: + """Require the new layout for module-system repositories after migration.""" + if has_project_roots(root): + return True + config = root / "lakefile.toml" + return ( + REQUIRE_PROJECT_ROOTS + and config.exists() + and tomllib.loads(config.read_text(encoding="utf-8")).get( + "requiresModuleSystem" + ) + is True + ) + + +def render_project_indexes(root: Path) -> dict[Path, str]: + """Render exactly one public aggregate per project and a small pool index.""" + projects = project_modules(root) + result = { + root / "LeanPool" / project / AGGREGATE_NAME: AGGREGATE_HEADER + + "".join(f"public import {module}\n" for module in modules) + for project, modules in projects.items() + } + result[root / "LeanPool.lean"] = MODULE_HEADER + "".join( + f"public import LeanPool.{project}.Imports\n" for project in projects + ) + return result + + +def structure_errors(root: Path) -> list[tuple[Path, str]]: + """Reject missing, duplicate, private, stale or cross-project index imports.""" + expected = render_project_indexes(root) + errors = [] + for path, content in expected.items(): + if not path.exists(): + errors.append((path, "missing generated project index")) + elif path.read_text(encoding="utf-8") != content: + errors.append( + ( + path, + "project index must list every source exactly once " + "using sorted public imports", + ) + ) + for path in (root / "LeanPool").glob(f"*/{AGGREGATE_NAME}"): + if path not in expected: + errors.append((path, "project aggregate has no project source files")) + return errors + + +def _generated_aggregate(source: str) -> bool: + """Recognize import-only generated roots, including current merge conflicts.""" + if GENERATED_MARKER not in source: + return False + code = code_view(source) + return all( + not line.strip() + or re.fullmatch(r"\s*module\s*", line) + or re.fullmatch(r"\s*(?:public\s+)?import\s+[\w'.]+\s*", line) + or re.match(r"^(?:<<<<<<<|=======|>>>>>>>|\|{7})(?:\s|$)", line) + for line in code.splitlines() + ) + + +def _write_indexes(contents: dict[Path, str], *, check: bool) -> int: + """Check indexes or update them without overwriting a mathematical source.""" + for path in contents: + if path.name == AGGREGATE_NAME and path.exists(): + if not _generated_aggregate(path.read_text(encoding="utf-8")): + raise ValueError(f"refusing to overwrite source file {path}") + changed = 0 + for path, content in contents.items(): + previous = path.read_text(encoding="utf-8") if path.exists() else None + if previous == content: + continue + changed += 1 + if check: + print(f"{path} is missing or out of date; run `lake exe mk_all`") + else: + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text(content, encoding="utf-8") + print(f"Updated {path}") + return min(changed, 125) if check else 0 + + +def _library_index(root: Path, library: str, *, use_module: bool) -> str: + """Keep the ordinary flat indexes for Challenge and Solution unchanged.""" + existing = root / f"{library}.lean" + source = existing.read_text(encoding="utf-8") if existing.exists() else "" + module_style = use_module or code_view(source).lstrip().startswith("module") + prefix = "public " if module_style else "" + modules = sorted( + library + "." + ".".join(path.relative_to(root / library).with_suffix("").parts) + for path in (root / library).rglob("*.lean") + ) + return (MODULE_HEADER if module_style else "") + "".join( + f"{prefix}import {module}\n" for module in modules + ) + + +def main(argv: list[str] | None = None) -> int: + """Provide the local mk_all CLI, shared with mechanical PR rebases.""" + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--repo", type=Path, default=Path(".")) + parser.add_argument("--check", action="store_true") + parser.add_argument("--module", action="store_true") + parser.add_argument("--project-roots", action="store_true") + parser.add_argument("--lib", choices=("LeanPool", "Challenge", "Solution")) + args = parser.parse_args(argv) + root = args.repo.resolve() + contents = {} + for library in [args.lib] if args.lib else ["LeanPool", "Challenge", "Solution"]: + if library == "LeanPool" and ( + args.project_roots or requires_project_roots(root) + ): + contents.update(render_project_indexes(root)) + else: + contents[root / f"{library}.lean"] = _library_index( + root, library, use_module=args.module + ) + try: + return _write_indexes(contents, check=args.check) + except ValueError as error: + print(error, file=sys.stderr) + return 1 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/python/lean_pool/quality.py b/python/lean_pool/quality.py index 4044e249c0..a99abfda09 100644 --- a/python/lean_pool/quality.py +++ b/python/lean_pool/quality.py @@ -27,6 +27,7 @@ import yaml from lean_pool import challenge +from lean_pool.indexes import requires_project_roots, structure_errors from lean_pool.validation_cache import ValidationCache, pool_units # Derived from the challenge module so the pool gate and the axiom list @@ -1194,6 +1195,16 @@ def _check_project_uniqueness(path: Path, projects: list[Any]) -> list[_QualityE return errors +def _check_project_indexes(root: Path) -> list[_QualityError]: + """Enforce the generated pool index and each complete public project root.""" + if not requires_project_roots(root): + return [] + return [ + _QualityError(path, 1, message + "; run `lake exe mk_all`") + for path, message in structure_errors(root) + ] + + def _check_project_entry_imports( root: Path, projects: list[Any] ) -> list[_QualityError]: @@ -1202,6 +1213,16 @@ def _check_project_entry_imports( if not index_path.exists(): return [] imports = set(_parse_imports(index_path.read_text())) + if requires_project_roots(root): + # Each project root directly imports its registered entry and all sources. + imports = { + imported + for module in imports + if module.endswith(".Imports") + for path in [_module_to_path(root, module)] + if path.exists() + for imported in _parse_imports(path.read_text()) + } entry_modules = { project["entry_module"] for project in projects @@ -1879,6 +1900,7 @@ def run_checks( ) -> list[_QualityError]: """Run all deterministic quality checks.""" checks = [ + _check_project_indexes, _check_reachability, _check_headers, _check_forbidden_lean_text, diff --git a/python/lean_pool/rebase.py b/python/lean_pool/rebase.py index 7594115af7..240de2d59a 100644 --- a/python/lean_pool/rebase.py +++ b/python/lean_pool/rebase.py @@ -6,7 +6,7 @@ ``LeanPool.lean`` The ``mk_all`` index is a sorted list of ``import LeanPool.X`` lines, one - per Lean file in the tree, so it is regenerated rather than merged -- + per project aggregate after migration, regenerated rather than merged -- and, because it is derived purely from the file tree, without needing a Lean toolchain. @@ -32,6 +32,8 @@ import yaml from lean_pool.exposition.source_text import code_view +from lean_pool.indexes import main as regenerate_indexes +from lean_pool.indexes import render_project_indexes, requires_project_roots logger = logging.getLogger(__name__) @@ -63,6 +65,8 @@ def _uses_module_system(source: str) -> bool: def render_index(root: Path) -> str: """Regenerate the ``mk_all`` index from the Lean files on disk.""" + if requires_project_roots(root): + return render_project_indexes(root)[root / INDEX] pool = root / "LeanPool" modules = sorted( "LeanPool." @@ -170,12 +174,17 @@ def merge_registry(base: str, ours: str, theirs: str) -> str: def resolvable(conflicts: list[str]) -> bool: """Whether every conflicted path is one this module can resolve.""" - return bool(conflicts) and set(conflicts) <= RESOLVABLE + return bool(conflicts) and all( + path in RESOLVABLE or re.fullmatch(r"LeanPool/[^/]+/Imports\.lean", path) + for path in conflicts + ) def _command_index(args: argparse.Namespace) -> int: """Rewrite the index from the working tree.""" root = args.repo.resolve() + if requires_project_roots(root): + return regenerate_indexes(["--repo", str(root), "--lib", "LeanPool"]) (root / INDEX).write_text(render_index(root), encoding="utf-8") logger.info("regenerated %s", INDEX) return 0 diff --git a/python/lean_pool/rebase_fastpath.py b/python/lean_pool/rebase_fastpath.py index 2fd9533602..62df9b9682 100644 --- a/python/lean_pool/rebase_fastpath.py +++ b/python/lean_pool/rebase_fastpath.py @@ -23,6 +23,8 @@ from typing import Any from urllib.parse import urlencode +from lean_pool.indexes import requires_project_roots, structure_errors + ARTIFACT = "rebase-project-build" ARCHIVE = f"{ARTIFACT}.tar.gz" MANIFEST = "rebase-build-manifest.json" @@ -233,6 +235,8 @@ def decision( def check_index(root: Path) -> bool: """Check the generated root without starting Lean or downloading Mathlib.""" + if requires_project_roots(root): + return not structure_errors(root) pool = root / "LeanPool" modules = sorted( "LeanPool." diff --git a/python/tests/test_indexes.py b/python/tests/test_indexes.py new file mode 100644 index 0000000000..c8bcb27579 --- /dev/null +++ b/python/tests/test_indexes.py @@ -0,0 +1,181 @@ +"""Check complete project coverage, safe regeneration and public exports.""" + +from pathlib import Path + +import pytest + +from lean_pool import indexes +from lean_pool.quality import _check_project_indexes +from lean_pool.rebase import main as rebase_main +from lean_pool.rebase import render_index, resolvable +from lean_pool.rebase_fastpath import check_index + + +def _sources(root: Path) -> None: + """Create a single-file project and a project with nested source files.""" + (root / "LeanPool/Beta/Nested").mkdir(parents=True) + for name in ("Alpha", "Beta", "Beta/Core", "Beta/Nested/Other"): + (root / f"LeanPool/{name}.lean").write_text("module\n") + (root / "lakefile.toml").write_text("requiresModuleSystem = true\n") + + +def _generate(root: Path) -> None: + """Opt a fixture into the migrated layout using the production CLI.""" + assert ( + indexes.main(["--repo", str(root), "--project-roots", "--lib", "LeanPool"]) == 0 + ) + + +def test_complete_public_indexes(tmp_path: Path) -> None: + """Every source is covered once, including the original entry modules.""" + _sources(tmp_path) + _generate(tmp_path) + assert (tmp_path / "LeanPool.lean").read_text() == ( + indexes.MODULE_HEADER + + "public import LeanPool.Alpha.Imports\n" + + "public import LeanPool.Beta.Imports\n" + ) + assert (tmp_path / "LeanPool/Beta/Imports.lean").read_text() == ( + indexes.AGGREGATE_HEADER + + "public import LeanPool.Beta\n" + + "public import LeanPool.Beta.Core\n" + + "public import LeanPool.Beta.Nested.Other\n" + ) + assert indexes.structure_errors(tmp_path) == [] + assert _check_project_indexes(tmp_path) == [] + assert check_index(tmp_path) + assert render_index(tmp_path) == (tmp_path / "LeanPool.lean").read_text() + assert indexes.main(["--repo", str(tmp_path), "--lib", "LeanPool", "--check"]) == 0 + + +@pytest.mark.parametrize( + "damage", ["missing", "duplicate", "private", "foreign", "math"] +) +def test_rejects_incomplete_or_unsafe_aggregate(tmp_path: Path, damage: str) -> None: + """The quality gate rejects broken public coverage and non-index code.""" + _sources(tmp_path) + _generate(tmp_path) + path = tmp_path / "LeanPool/Beta/Imports.lean" + source = path.read_text() + if damage == "missing": + source = source.replace("public import LeanPool.Beta.Core\n", "") + elif damage == "duplicate": + source += "public import LeanPool.Beta.Core\n" + elif damage == "private": + source = source.replace("public import", "import", 1) + elif damage == "foreign": + source += "public import LeanPool.Alpha\n" + else: + source += "def unexpected := 1\n" + path.write_text(source) + assert _check_project_indexes(tmp_path) + assert not check_index(tmp_path) + assert indexes.main(["--repo", str(tmp_path), "--lib", "LeanPool", "--check"]) > 0 + assert path.read_text() == source + + +def test_rejects_flat_root_and_new_unlisted_source(tmp_path: Path) -> None: + """Reachability alone cannot hide flat imports or incomplete project roots.""" + _sources(tmp_path) + _generate(tmp_path) + (tmp_path / "LeanPool/Beta/New.lean").write_text("module\n") + assert _check_project_indexes(tmp_path) + assert rebase_main(["index", "--repo", str(tmp_path)]) == 0 + assert _check_project_indexes(tmp_path) == [] + (tmp_path / "LeanPool.lean").write_text("public import LeanPool.Beta.New\n") + assert _check_project_indexes(tmp_path) + assert rebase_main(["index", "--repo", str(tmp_path)]) == 0 + assert _check_project_indexes(tmp_path) == [] + + +def test_deleted_aggregates_cannot_restore_flat_layout( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + """After rollout the gate remains mandatory even if every aggregate is deleted.""" + monkeypatch.setattr(indexes, "REQUIRE_PROJECT_ROOTS", True) + _sources(tmp_path) + (tmp_path / "LeanPool.lean").write_text("module\npublic import LeanPool.Alpha\n") + assert _check_project_indexes(tmp_path) + assert indexes.main(["--repo", str(tmp_path), "--lib", "LeanPool"]) == 0 + assert _check_project_indexes(tmp_path) == [] + + +def test_preserves_existing_sources(tmp_path: Path) -> None: + """An existing Imports.lean containing mathematics must never be overwritten.""" + _sources(tmp_path) + path = tmp_path / "LeanPool/Beta/Imports.lean" + source = "module\npublic def existing := 1\n" + path.write_text(source) + assert indexes.main(["--repo", str(tmp_path), "--project-roots"]) == 1 + assert path.read_text() == source + + +def test_mechanical_aggregate_conflict_resolution(tmp_path: Path) -> None: + """Concurrent additions to the same project regenerate their shared root.""" + _sources(tmp_path) + _generate(tmp_path) + path = tmp_path / "LeanPool/Beta/Imports.lean" + path.write_text("<<<<<<< HEAD\n" + path.read_text() + "=======\n>>>>>>> incoming\n") + assert resolvable(["LeanPool.lean", "LeanPool/Beta/Imports.lean"]) + assert not resolvable(["LeanPool/Beta/Core.lean"]) + assert rebase_main(["index", "--repo", str(tmp_path)]) == 0 + assert _check_project_indexes(tmp_path) == [] + + +def test_generator_does_not_delete_declarations(tmp_path: Path) -> None: + """A generated marker cannot authorize overwriting added mathematical code.""" + _sources(tmp_path) + _generate(tmp_path) + path = tmp_path / "LeanPool/Beta/Imports.lean" + source = path.read_text() + "public def unexpected := 1\n" + path.write_text(source) + assert indexes.main(["--repo", str(tmp_path), "--lib", "LeanPool"]) == 1 + assert path.read_text() == source + + +def test_lean_public_exports(tmp_path: Path) -> None: + """A consumer sees entry and nested declarations through only LeanPool.""" + import os + import shutil + import subprocess + + lean = shutil.which("lean") + if lean is None: + pytest.skip("Lean toolchain not installed") + (tmp_path / "LeanPool/Example/Nested").mkdir(parents=True) + sources = { + "LeanPool/Example/Leaf.lean": ( + "module\npublic def answer : Nat := 42\n" + "public theorem leafFact : (1 : Nat) = 1 := rfl\n" + ), + "LeanPool/Example.lean": ( + "module\nimport LeanPool.Example.Leaf\n" + "public def rootAnswer : Nat := answer\n" + ), + "LeanPool/Example/Nested/Other.lean": ( + "module\npublic def nestedAnswer : Nat := 7\n" + ), + } + for name, source in sources.items(): + (tmp_path / name).write_text(source) + _generate(tmp_path) + (tmp_path / "Consumer.lean").write_text( + "module\nimport LeanPool\n" + "public def consumer : Nat := answer + rootAnswer + nestedAnswer\n" + "example : (1 : Nat) = 1 := leafFact\n" + ) + modules = [ + *sources, + "LeanPool/Example/Imports.lean", + "LeanPool.lean", + "Consumer.lean", + ] + for name in modules: + subprocess.run( + [lean, "-o", str(Path(name).with_suffix(".olean")), name], + cwd=tmp_path, + env={**os.environ, "LEAN_PATH": str(tmp_path)}, + check=True, + capture_output=True, + timeout=30, + ) diff --git a/scripts/ProjectIndexes.lean b/scripts/ProjectIndexes.lean new file mode 100644 index 0000000000..b8d6b1f5b4 --- /dev/null +++ b/scripts/ProjectIndexes.lean @@ -0,0 +1,16 @@ +/- +Copyright (c) 2026 Lean Pool contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lean Pool contributors +-/ +import Lean + +/-- Generate complete project indexes, or check them without rewriting files. -/ +def main (args : List String) : IO UInt32 := do + let result ← IO.Process.output { + cmd := "python3" + args := #["scripts/project-indexes.py"] ++ args.toArray + } + IO.print result.stdout + IO.eprint result.stderr + return result.exitCode diff --git a/scripts/project-indexes.py b/scripts/project-indexes.py new file mode 100644 index 0000000000..b13207fbab --- /dev/null +++ b/scripts/project-indexes.py @@ -0,0 +1,10 @@ +"""Run the shared index generator using only the Python standard library.""" + +import sys +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parents[1] / "python")) + +from lean_pool.indexes import main # noqa: E402 + +sys.exit(main())