Support complete public project-root indexes

[Vilin97]

The flat pool index adds one import for every source file and now reaches the 10,000-code-line limit. Add a local lake exe mk_all generator for one public aggregate per project, shared by the quality linter, mechanical rebase helper and rebase build fast path. Project aggregates publicly import the original entry module and every nested source; the pool index imports only these aggregates.

This infrastructure PR preserves flat indexes during rollout. A separate content PR generates the project roots, followed by mandatory enforcement for module-system packages. The generator refuses to overwrite mathematical code, and mechanical rebases also stage regenerated aggregates. Challenge and Solution retain their existing indexes. Existing size, proof, option and branch checks remain intact.

Validation: 561 Python tests passed (2 unrelated optional tests skipped), including a real Lean consumer compiled through both public aggregation layers; Ruff and formatting pass; the local lake exe mk_all --module --check and whole-tree static quality checks pass. No formalization sources changed.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[High risk] Adds project-level index generation and validation to the build system.

The PR appears safe to merge, with non-blocking generator-cleanup and rollout-documentation corrections needed.

Findings

1.  Obsolete aggregates remain unchecked ▶
2.  Instructions describe future behavior ▶

Summary

The PR adds a Python-backed Lake index generator, project-aggregate validation, and rebase support while retaining flat indexes until a separate migration. The generator does not handle obsolete aggregates, and the contribution instructions describe the future layout as though it were already active.

_{Reviews (1) · Last reviewed commit: "Support complete public project-root ind..."}

[greptile-apps]

Obsolete aggregates remain unchecked

When a project's last source file is removed, the expected output no longer includes its Imports.lean. This loop only visits expected files, so regeneration leaves the old aggregate in place and mk_all --check passes, even though the quality gate rejects it. Handling obsolete generated aggregates in both modes would keep the generator and its check consistent.

Knowledge Base Used: Python maintenance tooling

Note: If this suggestion doesn't match your team's coding style, reply to this and let me know. I'll remember it for next time!

[greptile-apps]

Instructions describe future behavior

This tells contributors that ordinary lake exe mk_all generates a new project's Imports.lean, but the generator still defaults to flat indexes until a project aggregate already exists. Contributors following these steps cannot produce the requested file; adding just one aggregate manually makes validation require aggregates for every project. Please describe the staged rollout and the explicit migration command instead.

Knowledge Base Used: Python maintenance tooling