Speed up exposition extraction and preserve completed work

[Vilin97]

Exposition can spend hours scanning elaborated commands because the embedded-name visitor expands shared Lean expression subtrees at every occurrence. Failed or timed-out extraction batches also discard completed projects from the hosted cache, so retries repeat that work.

Visit each expression node once with Lean's memoized traversal, preserving embedded-name membership. Save fingerprinted, digest-verified project outputs after unsuccessful batches, use unique cache keys for each attempt, and prune older main caches only after a replacement saves successfully. Builder, UI and test changes no longer invalidate extraction caches. Record completed-project progress atomically and log extractor phase timings to diagnose remaining slow projects.

The real Lake build, baseline-214 minimal-file verification, two extraction workers and two verification workers remain intact. This does not precompile a checker or add project-check parallelism.

Validation:

• Full Python suite: 688 passed, 2 skipped; focused final extraction/Lean/workflow checks: 35 passed. Ruff, formatting, actionlint and diff checks passed.
• Pinned Lean regression compares name sets with the previous traversal, covers supported expression/name constructors, and detects repeated expansion of shared nodes. It fails against the previous extractor (262,144 duplicate names) and passes with this change.
• Before/after extraction on a real Lean fixture preserves declaration records and semantic command data; generated minimal files are byte-identical and compile with pinned Lean.
• Failed-batch recovery reuses completed siblings, rejects failed/corrupt output, preserves previously published combined output, and reproduces forced-cold output. Progress is recorded while a sibling is still running.
• Synthetic shared-expression benchmark: 5,461 ms before, 1 ms after. Whole-pool hosted performance and the cause of the remaining slow NFWeakPartition extraction are not yet confirmed.

[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] Changes build cache keys and extraction parallelism logic.

The PR appears safe to merge; both previous findings are addressed and no new actionable issue was found.

Summary

This PR speeds up embedded-name extraction and preserves completed projects across failed extraction batches.

• Shared Lean expressions are visited once.
• Each hosted cache attempt gets a unique key; failed batches can save completed work.
• The latest changes put the Lean regression in required CI and extend failure reports to the full extraction run.

_{Reviews (2) · Last reviewed commit: "Fix exposition failure diagnostics and e..." · Reviewed by Greptile}

[Vilin97]

🤖 LLM review — refactor (gpt-6.1-sol)

Reviewed head: 2c9833a63aca25004a3b3f48e5df8c7ed4d57f22

Verdict: 🛑 request_changes

This refactors exposition extraction to traverse shared expressions with Lean’s memoized visitor, retain completed project caches after failed batches, and write atomic progress diagnostics. The implementation improves the extraction pipeline: 59 targeted Python checks passed, the pinned-Lean regression passed directly, and a small Lean fixture preserved declaration records and semantic command data against the baseline. Two maintenance gaps remain: CI does not enforce the Lean regression, and some failures leave misleading progress status. Hosted timeout recovery was not exercised.

Aspect	Value
Scope	extractor performance and cache recovery
Introduces tech debt	🛑 yes
Maintainability	✅ improved
Brittleness	✅ more_robust
Risk	🟡 medium

The traversal and cache changes improve maintainability, but enforce the Lean regression in CI and cover the full run with failure reporting before merging.

Findings (2)

• unenforced-regression — python/tests/test_exposition_lean_extract.py:28
  The Python CI job collects this test without installing pinned Lean, while the jobs that install Lean select only test_ci_pr_build.py and test_indexes.py with the test_lake_ filter. A green CI run can therefore skip the new name-preservation and shared-expression regression entirely. Add an explicit invocation after Lean installation with LEAN_POOL_REQUIRE_TEST_TOOLCHAIN=1 so future traversal changes and toolchain bumps must exercise this oracle.
• misleading-diagnostics — python/lean_pool/exposition/extract.py:257
  The failure handler covers only the futures loop. Project discovery, fingerprinting, combine, and prune_cache can fail after the report has been marked in_progress without ever recording failed. I reproduced this with a missing entry module and a publication error after both projects completed. Wrap discovery through publication and pruning in the failure handler, retaining completed results, and test an exception outside the futures loop.

---

Tokens: 1,395,041 in / 12,835 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $5.7727 (Standard API equivalent; uncached input) (long-context rate)
Automated review against .github/REFACTOR_REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
request_changes is an ask, not a close: of the reviewer's past request_changes verdicts, 39% were merged after a human looked. Read the findings before acting on the verdict.

[Vilin97]

Source review: the extraction and dependency changes are acceptable with the two small repairs included at this reviewed head.

• Failure reporting covers discovery, fingerprinting, combined-output publication and cache pruning. Completed project diagnostics survive a failure, and a secondary timings-write error cannot replace the original exception.
• The real Lean extractor/oracle test now lives in test_ci_pr_build.py as test_lake_exposition_embedded_names_preserve_semantics_without_dag_replay, selected by the existing required pinned-Lean CI lane. The redundant standalone wrapper is removed.

Local validation of the exact repaired source passed 29 extraction tests and 2 selected Lean tests, with zero failures or skips. The Lean test compiled the actual extractor and exercised the small semantic oracle and shared-expression regression. Ruff check and format check passed on all three modified Python files. Independent source review also found both reported issues addressed.

The dependency review checks the generated canonical dependency sets; it does not claim identical ordering or multiplicity in raw intermediate JSON. Failure diagnostics remain best effort if their destination is unwritable, and the repair does not promise a transaction across both combined outputs.

Required checks must pass at the published head before normal protected integration. No workflow, gate, Lean extractor or Lean fixture was changed by this repair.