From eef38afd3d52aaca830edca1fa6ad426126fcd0f Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Thu, 13 Aug 2026 09:46:47 -0700 Subject: [PATCH 1/4] Avoid replaying declarations during exposition extraction --- python/lean_pool/exposition/SCHEMA.md | 13 ++++--- scripts/exposition/Extract.lean | 56 ++++++++++++++++++++++++--- 2 files changed, 59 insertions(+), 10 deletions(-) diff --git a/python/lean_pool/exposition/SCHEMA.md b/python/lean_pool/exposition/SCHEMA.md index c88f30ab55..0481903575 100644 --- a/python/lean_pool/exposition/SCHEMA.md +++ b/python/lean_pool/exposition/SCHEMA.md @@ -117,11 +117,14 @@ Link recipes: `doi` → `https://doi.org/`, `arxiv` → ### Minimal-Lean-file fields (schema 1.3) The minimal-file pipeline follows LMLExposition's methodology (Rémy -Degenne, github.com/LeanMachineLearning/exposition): the extractor -re-elaborates every module against the loaded environment and classifies -each top-level command from its real `Syntax`, so the builder replays -byte-exact source with pre-computed surgery edits instead of textual -heuristics. +Degenne, github.com/LeanMachineLearning/exposition): the extractor parses +every module against its loaded environment and classifies each top-level +command from its real `Syntax`, so the builder replays byte-exact source +with pre-computed surgery edits instead of textual heuristics. It elaborates +context commands that can change parser or command scope, but not declaration +commands: those declarations are already present in the imported environment, +and elaborating a `private` declaration would create a fresh internal name and +execute its body a second time. The shard carries `commit` (raw-source fetches pin to it) and a `moduleData` array parallel to `modules`: diff --git a/scripts/exposition/Extract.lean b/scripts/exposition/Extract.lean index 97391c189d..f74eb31b7b 100644 --- a/scripts/exposition/Extract.lean +++ b/scripts/exposition/Extract.lean @@ -331,10 +331,11 @@ namespace Exposition.Commands /-! Per-module command classification for the minimal-file builder, ported from LMLExposition's `Extract.lean` (Rémy Degenne, after Matthew Ballard's -`EmitStandalone.lean`). Each source file is re-elaborated against the loaded -environment (`IO.processCommands`; declarations fail fast with "already -declared", which is expected and ignored) to recover per-command `Syntax` -and byte ranges. The output is one JSON line per module describing every +`EmitStandalone.lean`). Each source file is parsed against the loaded +environment to recover per-command `Syntax` and byte ranges. Context commands +are re-elaborated because they can extend the parser or change its scope; +declaration commands are not, because their compiled declarations are already +in the environment. The output is one JSON line per module describing every declaration command (with byte-exact `sorry`-surgery edits) and every context command (`namespace`/`open`/`variable`/notation/...), which the client-side builder assembles into standalone files. @@ -569,6 +570,46 @@ def syntacticDeps (env : Environment) (stx : Syntax) (self : Array Name) acc := acc.insert candidate return acc.toArray +/-- True when `stx` contains the source range of an exposed declaration. +Declaration ranges come from the imported environment, so this recognizes +wrapper commands (`open ... in`, `mutual`, attributes, and so on) without +trying to duplicate Lean's declaration-command taxonomy. -/ +def containsDeclaration (declPos : Std.HashMap Nat (Array Name)) (stx : Syntax) : Bool := + match stx.getPos?, stx.getTailPos? with + | some start, some stop => + declPos.any fun pos _ => start.byteIdx ≤ pos && pos < stop.byteIdx + | _, _ => false + +/-- Parse a module while elaborating only commands that can affect the parser +or command scope. The module's compiled environment is already loaded, so +elaborating declarations is both redundant and incorrect for this use: public +declarations merely fail as already declared, while `private` declarations get +fresh internal names and may execute their proof terms again. Context commands +must still be elaborated so later commands see local notation, namespaces, +variables, options, and sections exactly as the original source did. -/ +partial def parseCommands (declPos : Std.HashMap Nat (Array Name)) : + Frontend.FrontendM Unit := do + Frontend.updateCmdPos + let cmdState ← Frontend.getCommandState + let inputCtx ← Frontend.getInputContext + let parserState ← Frontend.getParserState + let scope := cmdState.scopes.head! + let parserContext := { + env := cmdState.env + options := scope.opts + currNamespace := scope.currNamespace + openDecls := scope.openDecls + } + let (stx, nextParserState, messages) := + Parser.parseCommand inputCtx parserContext parserState cmdState.messages + modify fun state => { state with commands := state.commands.push stx } + Frontend.setParserState nextParserState + Frontend.setMessages messages + unless containsDeclaration declPos stx && !isNotationCmdKind stx.getKind do + Frontend.elabCommandAtFrontend stx + unless Parser.isTerminalCommand stx do + parseCommands declPos + /-- Processes one module source: classifies each command and emits the JSON entry list. `declPos` maps range-start byte indices to exposed declaration names (several may share one range start); `notationKindsAt` maps range-start byte indices to pool parser-kind @@ -583,7 +624,12 @@ def processFile (env : Environment) (source : String) (filePath : String) let inputCtx := Parser.mkInputContext source filePath let (_, parserState, messages) ← Parser.parseHeader inputCtx let cmdState := Command.mkState env messages {} - let s ← IO.processCommands inputCtx parserState cmdState + let initialState : Frontend.State := { + commandState := cmdState + parserState + cmdPos := parserState.pos + } + let (_, s) ← (parseCommands declPos).run { inputCtx } |>.run initialState let mut entries : Array Json := #[] let mut nsPrefixStack : Array Name := #[Name.anonymous] for stx in s.commands do From b0e1cab2eacb8297bef3250d6120fe020fdc54d8 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Thu, 13 Aug 2026 09:54:44 -0700 Subject: [PATCH 2/4] chore: refresh generated notice --- NOTICE | 2 ++ 1 file changed, 2 insertions(+) diff --git a/NOTICE b/NOTICE index 106e7eb290..d999c81d97 100644 --- a/NOTICE +++ b/NOTICE @@ -61,6 +61,7 @@ Apache License, Version 2.0, and are redistributed here under the same license. LeanPool/Erdos367 https://github.com/scottdhughes/erdos367 LeanPool/Erdos403 https://github.com/gotrevor/erdos-403 LeanPool/Erdos865 https://github.com/mrricky22/erdos-865-lean + LeanPool/Erdos97ConvexOctagon https://github.com/lyfar/erdos-97-octagon-lean LeanPool/ErdosMoser https://github.com/lyfar/erdos-moser-distinct-subset-sums-lean LeanPool/ErdosTuzaValtr https://github.com/jcpaik/erdos-tuza-valtr LeanPool/EventStructures https://github.com/vikraman/event-structures @@ -78,6 +79,7 @@ Apache License, Version 2.0, and are redistributed here under the same license. LeanPool/Incompleteness https://github.com/FormalizedFormalLogic/Incompleteness LeanPool/IsTranscendentalPi https://github.com/samuelborza/IsTranscendentalPi LeanPool/Isoperimetric https://github.com/hojonathanho/isoperimetric + LeanPool/JacobianDiffgeo https://github.com/rkirov/jacobian-fable LeanPool/JohnsonLindenstraussLean https://github.com/claytomode/johnson-lindenstrauss-lean LeanPool/KrafftSieve https://github.com/ElNando888/KrafftSieve LeanPool/Lean4GlCoalgebras https://github.com/mgignoux/lean4-gl-coalgebras From bc27053d03e11d63d25a95ba70166f7a1404bef8 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Thu, 13 Aug 2026 10:00:26 -0700 Subject: [PATCH 3/4] Skip every compiled declaration during exposition parsing --- scripts/exposition/Extract.lean | 34 ++++++++++++++++++++++----------- 1 file changed, 23 insertions(+), 11 deletions(-) diff --git a/scripts/exposition/Extract.lean b/scripts/exposition/Extract.lean index f74eb31b7b..2d4a1d8c48 100644 --- a/scripts/exposition/Extract.lean +++ b/scripts/exposition/Extract.lean @@ -570,14 +570,15 @@ def syntacticDeps (env : Environment) (stx : Syntax) (self : Array Name) acc := acc.insert candidate return acc.toArray -/-- True when `stx` contains the source range of an exposed declaration. +/-- True when `stx` contains the source range of a compiled declaration. Declaration ranges come from the imported environment, so this recognizes wrapper commands (`open ... in`, `mutual`, attributes, and so on) without -trying to duplicate Lean's declaration-command taxonomy. -/ -def containsDeclaration (declPos : Std.HashMap Nat (Array Name)) (stx : Syntax) : Bool := +trying to duplicate Lean's declaration-command taxonomy. The positions cover +all constants from the module, not only declarations exposed on the site. -/ +def containsDeclaration (declarationPositions : Array Nat) (stx : Syntax) : Bool := match stx.getPos?, stx.getTailPos? with | some start, some stop => - declPos.any fun pos _ => start.byteIdx ≤ pos && pos < stop.byteIdx + declarationPositions.any fun pos => start.byteIdx ≤ pos && pos < stop.byteIdx | _, _ => false /-- Parse a module while elaborating only commands that can affect the parser @@ -587,7 +588,7 @@ declarations merely fail as already declared, while `private` declarations get fresh internal names and may execute their proof terms again. Context commands must still be elaborated so later commands see local notation, namespaces, variables, options, and sections exactly as the original source did. -/ -partial def parseCommands (declPos : Std.HashMap Nat (Array Name)) : +partial def parseCommands (declarationPositions : Array Nat) : Frontend.FrontendM Unit := do Frontend.updateCmdPos let cmdState ← Frontend.getCommandState @@ -605,10 +606,10 @@ partial def parseCommands (declPos : Std.HashMap Nat (Array Name)) : modify fun state => { state with commands := state.commands.push stx } Frontend.setParserState nextParserState Frontend.setMessages messages - unless containsDeclaration declPos stx && !isNotationCmdKind stx.getKind do + unless containsDeclaration declarationPositions stx && !isNotationCmdKind stx.getKind do Frontend.elabCommandAtFrontend stx unless Parser.isTerminalCommand stx do - parseCommands declPos + parseCommands declarationPositions /-- Processes one module source: classifies each command and emits the JSON entry list. `declPos` maps range-start byte indices to exposed declaration @@ -617,7 +618,8 @@ names (so a notation command learns which kinds it defines); `notationDeps` maps parser kinds to their expansion's exposed constants; `allNotationKinds` is the pool-wide kind set for `usedNotations`. -/ def processFile (env : Environment) (source : String) (filePath : String) - (declPos : Std.HashMap Nat (Array Name)) (notationKindsAt : Std.HashMap Nat Name) + (declarationPositions : Array Nat) (declPos : Std.HashMap Nat (Array Name)) + (notationKindsAt : Std.HashMap Nat Name) (notationDeps : Std.HashMap Name (Array Name)) (allNotationKinds : NameSet) (exposedByLast : Std.HashMap String (Array Name)) (visibleModules : NameSet) : IO (Array Json) := do @@ -629,7 +631,7 @@ def processFile (env : Environment) (source : String) (filePath : String) parserState cmdPos := parserState.pos } - let (_, s) ← (parseCommands declPos).run { inputCtx } |>.run initialState + let (_, s) ← (parseCommands declarationPositions).run { inputCtx } |>.run initialState let mut entries : Array Json := #[] let mut nsPrefixStack : Array Name := #[Name.anonymous] for stx in s.commands do @@ -751,6 +753,16 @@ def emitCommands (outPath : System.FilePath) (exposed : NameSet) (names : Array try pure (some (← IO.FS.readFile path)) catch _ => pure none) | continue let fileMap := FileMap.ofString source + -- Detect every declaration command from the compiled module, including + -- private/generated declarations that are intentionally absent from the + -- exposition graph. Re-elaborating any of them is redundant and can + -- execute expensive private bodies under fresh internal names. + let mut declarationPositionSet : Std.HashSet Nat := {} + for name in env.header.moduleData[moduleIdx]!.constNames do + if let some ranges ← findDeclarationRanges? name then + declarationPositionSet := declarationPositionSet.insert + (fileMap.ofPosition ranges.range.pos).byteIdx + let declarationPositions := declarationPositionSet.toArray -- One range start can carry several declarations (`irreducible_def`, -- mutual blocks), so map each position to every name declared there. let mut declPos : Std.HashMap Nat (Array Name) := {} @@ -762,8 +774,8 @@ def emitCommands (outPath : System.FilePath) (exposed : NameSet) (names : Array for (kindName, pos) in moduleKinds do notationKindsAt := notationKindsAt.insert (fileMap.ofPosition pos).byteIdx kindName let visibleModules := moduleImportClosure env module - let entries ← processFile env source path.toString declPos notationKindsAt - notationDeps allNotationKinds exposedByLast visibleModules + let entries ← processFile env source path.toString declarationPositions declPos + notationKindsAt notationDeps allNotationKinds exposedByLast visibleModules handle.putStrLn (Json.mkObj [ ("m", Json.str module.toString), ("c", Json.arr entries) From 9b4195299b5def26300bb020de081510644c3b22 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Thu, 13 Aug 2026 10:27:59 -0700 Subject: [PATCH 4/4] Clarify exposition parser initialization --- scripts/exposition/Extract.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/scripts/exposition/Extract.lean b/scripts/exposition/Extract.lean index 2d4a1d8c48..e70b871ee1 100644 --- a/scripts/exposition/Extract.lean +++ b/scripts/exposition/Extract.lean @@ -793,9 +793,9 @@ unsafe def main (args : List String) : IO UInt32 := do -- useful for testing against a partially built tree. let modules := if args.length > 2 then args.drop 2 |>.map (·.toName) else [Exposition.poolRoot] Lean.initSearchPath (← Lean.findSysroot) - -- Extension states must be loaded (and initializers executed) so that - -- `IO.processCommands` can parse Mathlib/pool notations (`Type*`, ...); - -- without them, parse-error recovery silently truncates commands. + -- Extension states must be loaded (and initializers executed) so that the + -- frontend parser recognizes Mathlib/pool notations (`Type*`, ...); without + -- them, parse-error recovery silently truncates commands. Lean.enableInitializersExecution let imports := modules.toArray.map fun module => ({ module } : Lean.Import) let env ← Lean.importModules imports {} (trustLevel := 1024) (loadExts := true)