Require project entry files and reduce CI restore disk usage

[Vilin97]

Documentation extraction stops when a project lacks LeanPool/<Project>.lean, while build restoration runs out of disk by retaining the downloaded ZIP, a second compressed archive, the old build, and the staged build. Require every top-level project entry file and make it import its registered entry, directly or transitively; recognize wrappers within a nested registered entry's project namespace. Stream the ZIP payload into decompression, and share unchanged cached files with staging through hard links.

Install the staged build only after manifest, archive-path, compression, and ZIP integrity checks finish; restore archived timestamps and permissions after installation. Reject duplicate archive paths before they can overwrite a shared cached file. The missing PolylogIntegrals entry file was fixed separately in #608.

Validation:

• uv run --group test pytest: 623 passed, 2 skipped.
• uv run ruff check and uv run ruff format --check pass.
• Static repository quality checks pass on this branch.
• Regression tests reject missing or empty project wrappers and accept direct or transitive imports of a nested registered entry. Artifact tests cover unchanged-file disk sharing, metadata preservation, duplicate paths, streamed gzip/zstd downloads without a second archive, corrupt-payload fallback, and temporary-file cleanup.

[greptile-apps]

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

[Medium risk] Adds validation rules for project structure and optimizes build cache reuse.

The import parser needs fixing before merging because the new check can block valid project wrappers.

Findings

1.  Valid wrappers fail CI ▶

Summary

The PR requires top-level project entry files and checks that they import nested registered entries. It also streams downloaded build archives and shares unchanged cached files while staging.

• Both previous unnumbered findings are addressed: the metadata test checks permissions and a strict timestamp tolerance, and empty wrappers are rejected.
• The new wrapper check still rejects valid multi-module import lines.

_{Reviews (2) · Last reviewed commit: "Require wrappers to import their registe..." · Reviewed by Greptile}

[Vilin97]

Review of commit 7984b9f.

[P2] Make the required wrapper compatible with nested registered entries.

For a card whose entry_module is LeanPool.MyProj.Internal, the new check requires LeanPool/MyProj.lean. Adding that wrapper satisfies the new check, but _check_top_level_project_modules still compares top-level modules against the exact registered entry set and reports top-level project module LeanPool.MyProj missing from projects.yml. This leaves a supported nested entry unable to satisfy both checks. The new test checks only the missing-wrapper case.

Recognize the wrapper for its registered project namespace and add a positive test for the repaired nested layout, or explicitly migrate nested registrations to the wrapper. Avoid registering the same project twice. #608 already migrates its card and is not this counterexample.

Validation: reproduced the before/after conflict using the four relevant exact pure functions in an isolated fixture. This was not a full quality-check or CI run. The streamed restore changes have no additional blocking finding in the static review.

Follow-up on commit b316973: the posted P2 is addressed in the updated source. Top-level wrappers now match the registered project namespace, and a nested registered entry must be reachable through its wrapper. Five isolated fixtures using the exact updated quality functions pass: direct entry, nested entry, transitive nested import, rejection of an unreachable nested entry, and rejection of an unregistered top-level module. This tests the targeted namespace and reachability repair; the shared registry reader, whole quality run, full CI, and streamed artifact restoration are outside this follow-up result.