Cache exposition extraction and reuse Lean CI builds for docs

[Vilin97]

Recent documentation runs spent 137–146 minutes re-extracting every exposition project, plus 88–101 minutes rebuilding documentation data when caches were evicted. Two per-commit Lean caches were about 5 GiB each against the repository's 10 GB cache limit.

This change:

• Caches each project's isolated extraction using source, transitive-import, dependency, and extractor fingerprints. It validates both JSONL files, handles deleted projects, and publishes per-project timings and logs.
• Publishes the completed Lean build as a short-lived artifact for docs and exposition verification. Consumers match the CI event/head and verify the Git tree and build configuration; missing or incompatible artifacts fall back to the normal Lake build.
• Separates stable toolchain/Mathlib caches from per-commit pool builds, updates all consumers, and removes exposition's dependency on Mathlib docInfo. Preflight and Mathlib docInfo restore only dependencies.

All projects and existing proof, warning, lint, quality, minimal-file, and documentation checks still run. A separate prerequisite commit removes stale attribution entries for the already-deleted ForwardEuler and SpecialNumbers projects and regenerates NOTICE, fixing the existing Python test failure on main.

Validation: 427 Python tests pass; Ruff lint/format, actionlint across all workflows, ShellCheck, and git diff --check pass. A real SumDifferenceExponent build/extraction produced identical output hashes on cold, cached, and forced-refresh runs. Its cached read took <1 ms versus 5–13 seconds for extraction. Packaging/restoring the real Lean build preserves a successful incremental lake build. The live GitHub lookup selected the expected current PR CI run.

The first run must seed the new cache namespaces. Full-pool savings should be measured after the main-branch cache is populated; the small-project timing is not a full-CI benchmark. See python/ci-performance.md for evidence, cache ownership, fallback behavior, and diagnostics.

Separate infrastructure follow-up to #415; no formalization files are 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.

The implementation has no newly identified correctness defect, but the unresolved repository-authorization concern for the workflow changes should still be addressed before merging.

Findings

1.  Unauthorized CI Gate Changes ▶

Summary

This PR separates stable Lean dependency caches from pool-build caches, reuses compatible CI build artifacts in documentation jobs, and adds validated per-project exposition extraction caching.

• Packages and verifies compiled Lean builds before documentation reuse, with ordinary Lake builds retained as fallback.
• Fingerprints project sources, transitive imports, configuration, and extraction tooling before reusing JSONL outputs.
• Updates documentation, exposition verification, challenge verification, and proof-profile workflows to use the new cache namespaces.
• Adds regression and cache-contract coverage plus operational documentation.

_{Reviews (8) · Last reviewed commit: "Merge remote-tracking branch 'origin/mai..."}

[Vilin97]

Approved at 03004ec580 (infrastructure review, 2026-09-18).

Scope. Non-content CI/tooling change, correctly separated from content: five workflows, two new Python modules (ci_artifacts.py, exposition/extract.py), three test modules, a thin shell shim, and a design note. No gate, linter, quality check, or branch-protection rule is weakened — every existing build, warning-scan, lint, quality, minimal-file, and documentation validation step still runs.

What I checked.

• Cache split. LeanDependencies-v1 (elan + .lake/packages, keyed by toolchain+manifest, saved only on main after a successful Mathlib cache install and only on a miss) and LeanPoolBuild-v1 (.lake/build, keyed by build inputs + SHA with a prefix fallback). Producers and consumers agree across all five workflows; test_ci_cache_contract.py pins that contract.
• Build reuse. Docs/exposition/verify jobs ask the Lean CI run for the same event and head SHA for its lean-pool-build artifact, verify a manifest whose tree hash must equal HEAD^{tree} of the consuming checkout (so a different PR merge base falls back), reject any archive member outside .lake/build or any link, extract with the data filter, and fall back to the ordinary Lake build on any miss, timeout, or API error. Lake still checks traces afterwards. This restores oleans that the same PR's CI compiled — no new trust boundary beyond compiling PR code, which these jobs already do.
• Exposition cache. Per-project fingerprints cover project sources, Lake's transitive-import inventory (whole-pool hash on a missing/invalid inventory), toolchain/manifest/lakefile, and the extractor itself; outputs are validated and hashed before publication, assembled in index order, and stale generations pruned. Greptile's one finding (an empty JSONL passing validation and being cached) was real; it is fixed in 2de83bac with a regression test, and the thread is resolved.
• Tests and CI. Ruff, format, and the full pytest suite pass; actionlint and SHA-pinning pass; the modified Lean CI ran in sharded mode on this head with all shards, assembly (Build project), separation, and documentation preflight green, which also exercises the new pack step.

Residual risk, non-blocking. The first main run after merge seeds the new cache namespaces cold; docs jobs may wait up to two hours for a CI artifact before falling back, bounded by --wait-seconds. Both are documented in python/ci-performance.md.

Merging by protected squash.