fix: parse exposition declarations without replaying proofs

[Vilin97]

Summary

• parse each module against its compiled environment while elaborating only context commands that affect parser or command scope
• detect every compiled declaration from module metadata and skip its elaboration, including private/generated declarations absent from the exposition graph
• document why declaration bodies must not be replayed

Motivation

The extractor previously used IO.processCommands over source whose compiled declarations were already imported. Public declarations failed quickly as already declared, but private declarations received fresh internal names and their bodies ran again. Expensive kernel certificates in FrameBoosters.lean therefore took minutes a second time during documentation extraction and prompted a content workaround that exposed implementation declarations.

Validation

• lake env lean scripts/exposition/Extract.lean
• Ruff, formatting, and all 328 Python tests
• custom-notation and complex-wrapper modules: old/new dump and command files byte-identical
• main's private FrameBoosters project environment: old extractor 695.31s, latest extractor about 6s; dump and command files byte-identical
• full local 4.34 pool extraction: 66,970 declarations and 3,136 module command tables
• current-head Lean Action CI, documentation, and exhaustive minimal-file verification all green
• real CI full-pool declaration extraction completed in 21m58s and generated the exposition site successfully
• proof profile expected-skipped because no pooled Lean source changed
• latest-head LLM review expected-skipped as non-content; Greptile 5/5 with no findings

[Vilin97]

/profile

[greptile-apps]

Greptile Summary

The PR changes exposition extraction to parse modules against their compiled environments without re-elaborating existing declarations, avoiding duplicate execution of private declaration bodies.

• Adds range-based detection of compiled declarations and a selective frontend parsing loop.
• Continues elaborating context and notation commands needed by subsequent parsing.
• Updates the exposition schema documentation and generated project notice.

Confidence Score: 5/5

The PR appears safe to merge.

No blocking failure remains.

Important Files Changed

Filename	Overview
scripts/exposition/Extract.lean	Replaces full command processing with selective parsing and context elaboration while skipping declarations already present in the imported environment.
python/lean_pool/exposition/SCHEMA.md	Documents the extractor’s new parse-without-declaration-replay behavior and its rationale for private declarations.
NOTICE	Adds generated attribution entries for two pooled projects.

Flowchart

%%{init: {'theme': 'neutral'}}%%
flowchart TD
  A[Load compiled module environment] --> B[Parse next source command]
  B --> C{Contains compiled declaration?}
  C -->|No| D[Elaborate context command]
  C -->|Yes| E{Defines notation or parser syntax?}
  E -->|Yes| D
  E -->|No| F[Skip declaration elaboration]
  D --> G[Record parsed syntax]
  F --> G
  G --> H{Terminal command?}
  H -->|No| B
  H -->|Yes| I[Classify commands and emit JSON]

Loading

_{Reviews (4): Last reviewed commit: "Clarify exposition parser initialization" | Re-trigger Greptile}

[Vilin97]

/profile

[github-actions]

🤖 LLM review — not a content PR (skipped)

Reviewed head: 9b4195299b5def26300bb020de081510644c3b22

No model review: this PR changes Lean only outside LeanPool/, Challenge/, and Solution/, so there is no project, challenge, or solution here to judge. The build, linters, and quality gates still apply as usual.

---

Skip rule: the fit-and-significance review is for content PRs. Tooling and CI changes that happen to touch a .lean file are not graded as mathematical contributions.

[Vilin97]

/review

[Vilin97]

/profile

[Vilin97]

/review