Support complete public project-root indexes

.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.<Project>.Imports` per project in
+`LeanPool.lean`. Each generated `LeanPool/<Project>/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

.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

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/<YourProject>/`, 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/<YourProject>/`, 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/<YourProject>/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.)
 

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"

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())

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,

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

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."