[Vilin97]

Why

The docs site hasn't deployed since Oct 13, which is also why the Zulip announcer has posted nothing since (it defers every project whose docs pages 404). Every scheduled docs-publish run on main has failed since #659.

Cold documentation analysis is ~8 h (31,178 modules at ~64/min on one runner) and cold exposition extraction is ~3 h. Both could only finish by carrying progress over between runs, and in practice they almost never did:

• The DocsState and Exposition cache keys hash lakefile.toml (and the exposition fingerprints include it), with no fallback across a change. chore: bump Lean and Mathlib to v4.35.0 #689, Fix proof-length counter including unrelated declarations #712, Make every Lean warning a compile error (warningAsError, like Tau Ceti) #751 and fix(docs): build Tau Ceti before rendering and free docs runner disk #759 each wiped all progress between Nov 3 and Nov 6. Today's main run logged Cache not found for both.
• The docs cursor hashed every pool source plus three helper scripts, so on main any merge reset it to 0.

What changes

Docs (documentation.py, docs-build.yml)

• Completion is recorded per project. Each project's fingerprint covers its sources and Lake's .olean.hash content hashes over its local import closure, read from Lake's setup.json inventories so cross-project imports such as Zeta32 → Zeta5Irrational count. Unchanged projects are never handed to Lake again.
• Only the toolchain, dependency pins, doc-gen pins and link policy restart everything (plus a STATE_VERSION constant). The pool lakefile.toml is out of the checkpoint key, because options reach the docs only through compiled modules.
• A project's fingerprint is taken after its last batch. A real doc-gen run showed Lake can compile a stale module mid-analysis.
• Modules deleted from the pool are pruned from doc-gen's database. Every table cascades from modules. Their doc-data markers are removed too, so a module that comes back is analyzed again rather than trace-skipped.
• Import-order parsing (81 s over all files) now runs only for projects with work left (~3 s typically).

Exposition (extract.py, docs-publish.yml, exposition-verify.yml)

• Per-project fingerprints use compiled-module hashes instead of lakefile.toml.
• The extraction cache can also restore from any earlier generation (Exposition-v1-<os>-). The per-project fingerprints already decide what's valid.

Missing inventories or compiled hashes fall back to the old, conservative behaviour: whole-pool or lakefile hashing.

No checks or gates change. The exposition-verify.yml edit only adds a cache fallback.

Verification

• pytest: 860 passed. 4 tests (test_notice, 3× test_proof_profile) fail identically on origin/main on this machine. New tests cover per-project reuse, importers being re-run, option edits with and without compiled hashes, missing inventories, mid-batch compilation, and pruning with cascade.
• Real end-to-end run with the pinned doc-gen fork on two projects plus the root: cold analysis, then a rerun with 0 modules handed to Lake, then require_complete OK. Deleting AharoniKorman.Counterexample pruned it from every table (foreign_key_check and integrity_check clean, markers gone). Restoring it re-analyzed it (109 declarations back).
• ruff check, ruff format --check, actionlint clean.

Expected effect

The first run after merge is cold once, because the cache key changed. After that, a daily run should only analyze projects touched since the previous run, plus their importers. Splitting the cold path across runners is a separate follow-up.

🤖 Generated with Claude Code

[github-actions]

Proof profile (new / modified Lean files)

No added or modified Lean files under LeanPool/ in this PR. No compile-cost measurements are needed.

Advisory only — never blocks merge.

[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 impact] The PR appears safe to merge; no blocking issue was found.

Summary

The PR keeps completed documentation and exposition work across routine pool changes.

• API docs revisit changed projects and their importers.
• Deleted modules disappear from saved documentation data.
• Exposition extraction reuses projects with matching compiled inputs.

No actionable new issues were found. No previous review threads were supplied.

_{Reviews (2) · Last reviewed commit: "fix: fingerprint documentation companion..." · Reviewed by Greptile}

[Vilin97]

{
"summary": "Technical source review at 6082bc2: the per-project progress, dependency closures, deletion cleanup and completion checks are favorable after the repair. I fixed the fingerprints to include the contents and explicit presence/absence of public, server and private Lean artifacts; a missing cached hash streams the actual artifact, while a missing public artifact keeps the conservative configuration fallback. This closes the demonstrated stale-completion defect. Only four Python files changed in that repair. All 71 focused tests, the original companion-only stale-completion regression and Ruff checks passed; no Lean/doc-gen build or hosted performance claim is inferred. PR767 has two ordinary workflow merge conflicts requiring an explicit integration resolution. Current-head hosted checks and main qualification remain pending. PR770's three pre-existing workflow cache changes also need the separate direct authorization required by the repository rule; PR767's authorization covers PR767 only.",
"assessment": {
"scope": "Per-project documentation and exposition reuse, database pruning, cache fallbacks and regression coverage",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "unchanged",
"risk": "medium",
"assessment_one_sentence": "Per-project reuse retains current-input and completion validation after the companion-artifact repair, with hosted validation and workflow authorization still independent."
},
"verdict": "approve",
"findings": []
}