From b1d02e346d9152e1eba63339ac0947e72ff06e7e Mon Sep 17 00:00:00 2001 From: dpwoodru Date: Mon, 5 Oct 2026 01:50:55 +0000 Subject: [PATCH 1/4] feat: optional parallel kernel replay (parallel_replay) Adds an opt-in config field "parallel_replay" (default false). When it is set, comparator replays the solution with Lean.Kernel.Environment.replayParallel, defined in Comparator/Replay.lean: a copy of Lean's src/Lean/Replay.lean (v4.35.0-rc3) in which each theorem is added with addDeclWithoutChecking and checked by addDeclCore, against the environment just before it, in a Task. All tasks are awaited, and any kernel error fails the replay, before the postponed constructor/recursor checks. Non-theorem declarations are checked in order as before. Tests: tests/ParallelReplayUnit.lean (same verdict as replay on valid and forged inputs, run in CI) and the integration tests parallel_match and parallel_olean_issue. Closes #95. --- .github/workflows/lean_action_ci.yml | 4 + Comparator.lean | 1 + Comparator/Replay.lean | 221 ++++++++++++++++++ Main.lean | 11 +- README.md | 8 + tests/ParallelReplayUnit.lean | 70 ++++++ tests/projects/parallel_match/Challenge.lean | 2 + tests/projects/parallel_match/Solution.lean | 5 + tests/projects/parallel_match/config.json | 8 + tests/projects/parallel_match/test.json | 3 + .../parallel_olean_issue/Challenge.lean | 1 + .../parallel_olean_issue/Solution.lean | 22 ++ .../projects/parallel_olean_issue/config.json | 8 + tests/projects/parallel_olean_issue/test.json | 3 + 14 files changed, 365 insertions(+), 2 deletions(-) create mode 100644 Comparator/Replay.lean create mode 100644 tests/ParallelReplayUnit.lean create mode 100644 tests/projects/parallel_match/Challenge.lean create mode 100644 tests/projects/parallel_match/Solution.lean create mode 100644 tests/projects/parallel_match/config.json create mode 100644 tests/projects/parallel_match/test.json create mode 100644 tests/projects/parallel_olean_issue/Challenge.lean create mode 100644 tests/projects/parallel_olean_issue/Solution.lean create mode 100644 tests/projects/parallel_olean_issue/config.json create mode 100644 tests/projects/parallel_olean_issue/test.json diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index b863382..c8cc42d 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -54,3 +54,7 @@ jobs: run: | export PATH="$GITHUB_WORKSPACE/nanoda/target/release:$GITHUB_WORKSPACE/lean4export/.lake/build/bin:$GITHUB_WORKSPACE/landrun:$PATH" lean --run runtests.lean + + - name: Run parallel replay kernel tests + working-directory: comparator + run: lake env lean --run tests/ParallelReplayUnit.lean diff --git a/Comparator.lean b/Comparator.lean index 3baf3bd..1a196ed 100644 --- a/Comparator.lean +++ b/Comparator.lean @@ -5,3 +5,4 @@ Authors: Henrik Böving -/ import Comparator.Axioms import Comparator.Compare +import Comparator.Replay diff --git a/Comparator/Replay.lean b/Comparator/Replay.lean new file mode 100644 index 0000000..a58aa1c --- /dev/null +++ b/Comparator/Replay.lean @@ -0,0 +1,221 @@ +/- +Copyright (c) 2023 Kim Morrison. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ +import Lean.CoreM +import Lean.AddDecl +import Lean.Util.FoldConsts + +/-! +This file is a copy of `src/Lean/Replay.lean` from Lean v4.35.0-rc3, renamed to +`Lean.Kernel.Environment.replayParallel` (namespace `ParallelReplay`) so that it does not clash with +Lean's own `replay`. The only change in behavior: theorems are added to the environment with +`addDeclWithoutChecking`, and each theorem is checked by the kernel (`addDeclCore`) in a separate task +against the environment as it was just before that theorem; `replayParallel` waits for all of these +tasks and fails if any of them failed. Every declaration is therefore checked by the same kernel call +against the same environment as in `replay`; only the order in which theorems are checked differs. +-/ + +/-! +# `Lean.Kernel.Environment.replayParallel` (based on `Lean.Kernel.Environment.replay`) + +`replayParallel env constantMap` will "replay" all the constants in `constantMap : HashMap Name ConstantInfo` into `env`, +sending each declaration to the kernel for checking. + +`replayParallel` does not send constructors or recursors in `constantMap` to the kernel, +but rather checks that they are identical to constructors or recursors generated in the environment +after replaying any inductive definitions occurring in `constantMap`. + +`replayParallel` can be used either as: +* a verifier for a `Kernel.Environment`, by sending everything to the kernel, or +* a mechanism to safely transfer constants from one `Kernel.Environment` to another. + +-/ + +namespace Lean.Kernel.Environment + +namespace ParallelReplay + +structure Context where + newConstants : Std.HashMap Name ConstantInfo + +structure State where + env : Kernel.Environment + remaining : NameSet := {} + pending : NameSet := {} + postponedConstructors : NameSet := {} + postponedRecursors : NameSet := {} + /-- Kernel checks of theorems, running in parallel; see `addThmAsync`. -/ + tasks : Array (Name × Task (Except Kernel.Exception Kernel.Environment)) := #[] + +abbrev M := ReaderT Context <| StateRefT State IO + +/-- Check if a `Name` still needs processing. If so, move it from `remaining` to `pending`. -/ +def isTodo (name : Name) : M Bool := do + let r := (← get).remaining + if r.contains name then + modify fun s => { s with remaining := s.remaining.erase name, pending := s.pending.insert name } + return true + else + return false + +/-- Use the current `Environment` to throw a `Kernel.Exception`. -/ +def throwKernelException (ex : Kernel.Exception) : M Unit := do + throw <| .userError <| (← ex.toMessageData {} |>.toString) + +/-- Add a declaration, possibly throwing a `Kernel.Exception`. -/ +def addDecl (d : Declaration) : M Unit := do + match (← get).env.addDeclCore 0 0 d (cancelTk? := none) with + | .ok env => modify fun s => { s with env := env } + | .error ex => throwKernelException ex + +/-- +Add a theorem to the environment without checking it, and spawn a task that checks it with the kernel +against the environment as it was before the theorem was added. +-/ +def addThmAsync (info : TheoremVal) : M Unit := do + let kenv := (← get).env + let decl := Declaration.thmDecl info + match kenv.addDeclWithoutChecking decl with + | .ok env => + let t := Task.spawn fun () => kenv.addDeclCore 0 0 decl (cancelTk? := none) + modify fun s => { s with env := env, tasks := s.tasks.push (info.name, t) } + | .error ex => throwKernelException ex + +mutual +/-- +Check if a `Name` still needs to be processed (i.e. is in `remaining`). + +If so, recursively replay any constants it refers to, +to ensure we add declarations in the right order. + +The construct the `Declaration` from its stored `ConstantInfo`, +and add it to the environment. +-/ +partial def replayConstant (name : Name) : M Unit := do + if ← isTodo name then + let some ci := (← read).newConstants[name]? | unreachable! + replayConstants ci.getUsedConstantsAsSet + -- Check that this name is still pending: a mutual block may have taken care of it. + if (← get).pending.contains name then + try + match ci with + | .defnInfo info => + addDecl (Declaration.defnDecl info) + | .thmInfo info => + -- Ignore duplicate theorems. This code is identical to that in `finalizeImport` before it + -- added extended duplicates support for the module system, which is not relevant for us + -- here as we always load all .olean information. We need this case *because* of the module + -- system -- as we have more data loaded than it, we might encounter duplicate private + -- theorems where elaboration under the module system would have only one of them in scope. + if let some (.thmInfo info') := (← get).env.find? ci.name then + if info.name == info'.name && + info.type == info'.type && + info.levelParams == info'.levelParams && + info.all == info'.all + then + return + addThmAsync info + | .axiomInfo info => + addDecl (Declaration.axiomDecl info) + | .opaqueInfo info => + addDecl (Declaration.opaqueDecl info) + | .inductInfo info => + let lparams := info.levelParams + let nparams := info.numParams + let all ← info.all.mapM fun n => do pure <| ((← read).newConstants[n]!) + for o in all do + modify fun s => + { s with remaining := s.remaining.erase o.name, pending := s.pending.erase o.name } + let ctorInfo ← all.mapM fun ci => do + pure (ci, ← ci.inductiveVal!.ctors.mapM fun n => do + pure ((← read).newConstants[n]!)) + -- Make sure we are really finished with the constructors. + for (_, ctors) in ctorInfo do + for ctor in ctors do + replayConstants ctor.getUsedConstantsAsSet + let types : List InductiveType := ctorInfo.map fun ⟨ci, ctors⟩ => + { name := ci.name + type := ci.type + ctors := ctors.map fun ci => { name := ci.name, type := ci.type } } + addDecl (Declaration.inductDecl lparams nparams types false) + -- We postpone checking constructors, + -- and at the end make sure they are identical + -- to the constructors generated when we replay the inductives. + | .ctorInfo info => + modify fun s => { s with postponedConstructors := s.postponedConstructors.insert info.name } + -- Similarly we postpone checking recursors. + | .recInfo info => + modify fun s => { s with postponedRecursors := s.postponedRecursors.insert info.name } + | .quotInfo _ => + -- `Quot.lift` and `Quot.ind` have types that reference `Eq`, + -- so we need to ensure `Eq` is replayed before adding the quotient declaration. + replayConstant `Eq + addDecl (Declaration.quotDecl) + modify fun s => { s with pending := s.pending.erase name } + catch ex => + throw <| .userError s!"while replaying declaration '{name}':\n{ex}" + +/-- Replay a set of constants one at a time. -/ +partial def replayConstants (names : NameSet) : M Unit := do + for n in names do replayConstant n + +end + +/-- +Check that all postponed constructors are identical to those generated +when we replayed the inductives. +-/ +def checkPostponedConstructors : M Unit := do + for ctor in (← get).postponedConstructors do + match (← get).env.find? ctor, (← read).newConstants[ctor]? with + | some (.ctorInfo info), some (.ctorInfo info') => + if ! (info == info') then throw <| IO.userError s!"Invalid constructor {ctor}" + | _, _ => throw <| IO.userError s!"No such constructor {ctor}" + +/-- +Check that all postponed recursors are identical to those generated +when we replayed the inductives. +-/ +def checkPostponedRecursors : M Unit := do + for ctor in (← get).postponedRecursors do + match (← get).env.find? ctor, (← read).newConstants[ctor]? with + | some (.recInfo info), some (.recInfo info') => + if ! (info == info') then throw <| IO.userError s!"Invalid recursor {ctor}" + | _, _ => throw <| IO.userError s!"No such recursor {ctor}" + +end ParallelReplay + +open ParallelReplay + +/-- +"Replay" some constants into a `Kernel.Environment`, sending them to the kernel for checking. + +Throws a `IO.userError` if the kernel rejects a constant, +or if there are malformed recursors or constructors for inductive types. + +Theorems are checked in parallel tasks; non-theorem declarations are checked in order, as in `replay`. +-/ +def replayParallel (newConstants : Std.HashMap Name ConstantInfo) (env : Kernel.Environment) : + IO Kernel.Environment := do + let mut remaining : NameSet := ∅ + for (n, ci) in newConstants.toList do + -- We skip unsafe constants, and also partial constants. + -- Later we may want to handle partial constants. + if !ci.isUnsafe && !ci.isPartial then + remaining := remaining.insert n + let (_, s) ← StateRefT'.run (s := { env, remaining }) do + ReaderT.run (r := { newConstants }) do + for n in remaining do + replayConstant n + -- Wait for the kernel checks of all theorems. + for (name, t) in (← get).tasks do + if let .error ex := t.get then + try ParallelReplay.throwKernelException ex + catch ex => throw <| .userError s!"while replaying declaration '{name}':\n{ex}" + checkPostponedConstructors + checkPostponedRecursors + return s.env + +end Kernel.Environment diff --git a/Main.lean b/Main.lean index 8560511..f148020 100644 --- a/Main.lean +++ b/Main.lean @@ -21,6 +21,7 @@ structure Context where whichLandrun : String whichLean4Export : String externalKernels : (Std.TreeMap String (Array String)) + parallelReplay : Bool abbrev M := ReaderT Context IO @@ -219,7 +220,11 @@ def runBuiltinKernel (solution : Export.ExportedEnv) : M (Option String) := do let quotTargets := [`Quot.mk, `Quot.lift, `Quot.ind] let kernelConstMap := quotTargets.foldl (init := origConstMap) (·.erase ·) try - kernelEnv ← kernelEnv.replay kernelConstMap + if (← read).parallelReplay then + IO.println "Using parallel replay: theorems are checked by the kernel in parallel tasks." + kernelEnv ← kernelEnv.replayParallel kernelConstMap + else + kernelEnv ← kernelEnv.replay kernelConstMap IO.println "Lean default kernel accepts the solution" catch e => IO.println "Lean default kernel rejects the solution" @@ -325,6 +330,7 @@ structure Config where permitted_axioms : Array String enable_nanoda? : Option Bool external_kernels? : Option (Std.TreeMap String (Array String)) + parallel_replay? : Option Bool deriving Lean.FromJson, Lean.ToJson, Repr def M.run (x : M α) (cfg : Config) : IO α := do @@ -361,7 +367,8 @@ def M.run (x : M α) (cfg : Config) : IO α := do gitLocation := gitLocation, whichLean4Export := whichLean4Export, whichLandrun := whichLandrun, - externalKernels := externalKernels + externalKernels := externalKernels, + parallelReplay := cfg.parallel_replay?.getD false } end Comparator diff --git a/README.md b/README.md index e1d67f6..e24b8d4 100644 --- a/README.md +++ b/README.md @@ -85,6 +85,14 @@ moves toward having an option to receive the input file as a `CLI` argument. For development purposes, comparator supports overriding `nanoda` specifically using the `COMPARATOR_NANODA` environment variable. +## Parallel Kernel Replay +For very large solutions the replay through the Lean kernel dominates the run time, because it checks +every declaration one at a time. Setting `"parallel_replay": true` in the configuration makes comparator +check theorems in parallel tasks on Lean's task pool (`LEAN_NUM_THREADS` sets the number of workers). +Definitions, inductive types and all other declarations are still checked in order on one thread. Every +theorem is checked by the same kernel call, against the same environment, as in the default sequential +replay, and comparator waits for all theorem checks before accepting the solution. The default is `false`. + ## Definition Holes Sometimes challenges want to leave open definitions for solutions to fill in. This can range from simple things like filling in a `Prop` valued definition to resolve whether a conjecture is true or diff --git a/tests/ParallelReplayUnit.lean b/tests/ParallelReplayUnit.lean new file mode 100644 index 0000000..82794ac --- /dev/null +++ b/tests/ParallelReplayUnit.lean @@ -0,0 +1,70 @@ +import Lean +import Comparator.Replay + +/-! +Kernel-level tests of `Lean.Kernel.Environment.replayParallel`. Every case must be accepted or rejected +exactly as by `Lean.Kernel.Environment.replay`; the rejected cases include proofs that the elaborator would +never produce, so they are built directly as `ConstantInfo`s. + +Run with `lake env lean --run tests/ParallelReplayUnit.lean` (after `lake build`). +-/ + +open Lean + +/-- `inductive TestTrue : Prop | intro` and `inductive TestFalse : Prop` (no constructors). -/ +def propInductives : List ConstantInfo := + let trueInd : InductiveVal := { + name := `TestTrue, levelParams := [], type := .sort .zero, + numParams := 0, numIndices := 0, all := [`TestTrue], ctors := [`TestTrue.intro], + numNested := 0, isRec := false, isUnsafe := false, isReflexive := false } + let trueCtor : ConstructorVal := { + name := `TestTrue.intro, levelParams := [], type := .const `TestTrue [], + induct := `TestTrue, cidx := 0, numParams := 0, numFields := 0, isUnsafe := false } + let falseInd : InductiveVal := { + name := `TestFalse, levelParams := [], type := .sort .zero, + numParams := 0, numIndices := 0, all := [`TestFalse], ctors := [], + numNested := 0, isRec := false, isUnsafe := false, isReflexive := false } + [.inductInfo trueInd, .ctorInfo trueCtor, .inductInfo falseInd] + +def thm (name : Name) (type value : Expr) : ConstantInfo := + .thmInfo { name, levelParams := [], type, value, all := [name] } + +/-- Replay `propInductives ++ extra` with both `replay` and `replayParallel`; return whether both +gave the expected verdict. -/ +def runBoth (label : String) (expectAccept : Bool) (extra : List ConstantInfo) : IO Bool := do + let constMap := (propInductives ++ extra).foldl (init := {}) fun m ci => m.insert ci.name ci + let kenv := (← mkEmptyEnvironment).toKernelEnv + let seqOk ← try discard <| kenv.replay constMap; pure true catch _ => pure false + let parOk ← try discard <| kenv.replayParallel constMap; pure true catch _ => pure false + let ok := seqOk == expectAccept && parOk == expectAccept + IO.println s!"{if ok then "ok " else "FAIL"} {label}: expected accept={expectAccept}, replay={seqOk}, replayParallel={parOk}" + return ok + +def main : IO UInt32 := do + let tru := Expr.const `TestTrue [] + let intro := Expr.const `TestTrue.intro [] + let fls := Expr.const `TestFalse [] + let results := #[ + -- a valid chain: `lemA : TestTrue := intro`, `thmB : TestTrue := lemA` + ← runBoth "valid chain of theorems" true + [thm `lemA tru intro, thm `thmB tru (.const `lemA [])], + -- a theorem whose proof has the wrong type (`TestTrue` is a type, not a proof of `TestTrue`) + ← runBoth "ill-typed proof of the last theorem" false + [thm `lemA tru intro, thm `thmB tru tru], + -- an ill-typed lemma used by a theorem whose own proof is fine given the lemma's statement + ← runBoth "ill-typed proof of a lemma used later" false + [thm `lemBad fls intro, thm `thmUsesBad fls (.const `lemBad [])], + -- two theorems that prove `TestFalse` from each other + ← runBoth "cyclic theorems" false + [thm `cycleA fls (.const `cycleB []), thm `cycleB fls (.const `cycleA [])], + -- an ill-typed definition (checked on the main thread, as in `replay`) + ← runBoth "ill-typed definition" false + [.defnInfo { name := `badDef, levelParams := [], type := fls, value := intro, + hints := .abbrev, safety := .safe, all := [`badDef] }] + ] + if results.all id then + IO.println "All parallel replay kernel tests passed." + return 0 + else + IO.println "Some parallel replay kernel tests FAILED." + return 1 diff --git a/tests/projects/parallel_match/Challenge.lean b/tests/projects/parallel_match/Challenge.lean new file mode 100644 index 0000000..b45c299 --- /dev/null +++ b/tests/projects/parallel_match/Challenge.lean @@ -0,0 +1,2 @@ +theorem comm (n m : Nat) : n + m = m + n := by + sorry diff --git a/tests/projects/parallel_match/Solution.lean b/tests/projects/parallel_match/Solution.lean new file mode 100644 index 0000000..3056a74 --- /dev/null +++ b/tests/projects/parallel_match/Solution.lean @@ -0,0 +1,5 @@ +theorem add_zero_right (n : Nat) : n + 0 = n := rfl + +theorem comm (n m : Nat) : n + m = m + n := by + have _ := add_zero_right n + grind diff --git a/tests/projects/parallel_match/config.json b/tests/projects/parallel_match/config.json new file mode 100644 index 0000000..c1df714 --- /dev/null +++ b/tests/projects/parallel_match/config.json @@ -0,0 +1,8 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": ["comm"], + "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"], + "enable_nanoda": false, + "parallel_replay": true +} diff --git a/tests/projects/parallel_match/test.json b/tests/projects/parallel_match/test.json new file mode 100644 index 0000000..5d4bf27 --- /dev/null +++ b/tests/projects/parallel_match/test.json @@ -0,0 +1,3 @@ +{ + "exit_code": 0 +} diff --git a/tests/projects/parallel_olean_issue/Challenge.lean b/tests/projects/parallel_olean_issue/Challenge.lean new file mode 100644 index 0000000..a5626c9 --- /dev/null +++ b/tests/projects/parallel_olean_issue/Challenge.lean @@ -0,0 +1 @@ +theorem boom : False := sorry diff --git a/tests/projects/parallel_olean_issue/Solution.lean b/tests/projects/parallel_olean_issue/Solution.lean new file mode 100644 index 0000000..203072e --- /dev/null +++ b/tests/projects/parallel_olean_issue/Solution.lean @@ -0,0 +1,22 @@ +import Lean + +open Lean + +unsafe def badNatUnsafe : Nat := unsafeCast (-4294967296 : Int) + +@[implemented_by badNatUnsafe] opaque badNatVal : Nat + +run_elab + addDecl <| .defnDecl { + name := .str .anonymous "badNat" + levelParams := [] + type := .const ``Nat [] + value := .lit <| .natVal badNatVal + hints := .opaque + safety := .safe + } + +theorem boom : False := by + have truly_marvelous_0 : ¬badNat ≤ 9223372036854775807 := by decide + have truly_marvelous_1 : ¬9223372036854775807 < badNat := by decide + omega diff --git a/tests/projects/parallel_olean_issue/config.json b/tests/projects/parallel_olean_issue/config.json new file mode 100644 index 0000000..0acb509 --- /dev/null +++ b/tests/projects/parallel_olean_issue/config.json @@ -0,0 +1,8 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": ["boom"], + "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"], + "enable_nanoda": false, + "parallel_replay": true +} diff --git a/tests/projects/parallel_olean_issue/test.json b/tests/projects/parallel_olean_issue/test.json new file mode 100644 index 0000000..fe08d6a --- /dev/null +++ b/tests/projects/parallel_olean_issue/test.json @@ -0,0 +1,3 @@ +{ + "exit_code": 1 +} From 1164baab2c154df5a70a8224f1cf190cdaa18f49 Mon Sep 17 00:00:00 2001 From: dpwoodru Date: Thu, 8 Oct 2026 08:09:28 +0000 Subject: [PATCH 2/4] refactor: reuse Lean.Replay in replayParallel instead of copying it Per review: Comparator/Replay.lean now imports Lean.Replay (`import all`, since its helpers are not public there) and reuses Context, State, M, isTodo, throwKernelException, addDecl and the postponed constructor and recursor checks. The theorem-check tasks are kept in an ExtraState stacked on top of Replay.M (`StateRefT ExtraState Replay.M`). The only code still copied from Lean v4.35.0-rc3 is replayConstant, whose .thmInfo case is the actual change (addThmAsync instead of addDecl), and the loop in replayParallel, which awaits the theorem checks before the postponed constructor and recursor checks. --- Comparator/Replay.lean | 157 +++++++++++++---------------------------- 1 file changed, 50 insertions(+), 107 deletions(-) diff --git a/Comparator/Replay.lean b/Comparator/Replay.lean index a58aa1c..d7a23b3 100644 --- a/Comparator/Replay.lean +++ b/Comparator/Replay.lean @@ -3,113 +3,75 @@ Copyright (c) 2023 Kim Morrison. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ -import Lean.CoreM -import Lean.AddDecl -import Lean.Util.FoldConsts +module -/-! -This file is a copy of `src/Lean/Replay.lean` from Lean v4.35.0-rc3, renamed to -`Lean.Kernel.Environment.replayParallel` (namespace `ParallelReplay`) so that it does not clash with -Lean's own `replay`. The only change in behavior: theorems are added to the environment with -`addDeclWithoutChecking`, and each theorem is checked by the kernel (`addDeclCore`) in a separate task -against the environment as it was just before that theorem; `replayParallel` waits for all of these -tasks and fails if any of them failed. Every declaration is therefore checked by the same kernel call -against the same environment as in `replay`; only the order in which theorems are checked differs. --/ +public import Lean.AddDecl +import all Lean.Replay +import Lean.Util.FoldConsts /-! -# `Lean.Kernel.Environment.replayParallel` (based on `Lean.Kernel.Environment.replay`) - -`replayParallel env constantMap` will "replay" all the constants in `constantMap : HashMap Name ConstantInfo` into `env`, -sending each declaration to the kernel for checking. - -`replayParallel` does not send constructors or recursors in `constantMap` to the kernel, -but rather checks that they are identical to constructors or recursors generated in the environment -after replaying any inductive definitions occurring in `constantMap`. - -`replayParallel` can be used either as: -* a verifier for a `Kernel.Environment`, by sending everything to the kernel, or -* a mechanism to safely transfer constants from one `Kernel.Environment` to another. - +# `Lean.Kernel.Environment.replayParallel` + +`replayParallel` is `Lean.Kernel.Environment.replay` (from `Lean.Replay`) with one change: theorems are +added to the environment with `addDeclWithoutChecking`, and each theorem is checked by the kernel +(`addDeclCore`) in a separate task against the environment as it was just before that theorem. +`replayParallel` waits for all of these tasks, and fails if any of them failed, before the postponed +constructor and recursor checks. Every declaration is therefore checked by the same kernel call against +the same environment as in `replay`; only the order in which theorems are checked differs. + +Everything else is reused from `Lean.Replay`: `Context`, `State`, `M`, `isTodo`, `throwKernelException`, +`addDecl` and the postponed constructor and recursor checks. They are not public there, hence +`import all Lean.Replay`. The only code copied from `Lean.Replay` (Lean v4.35.0-rc3) is `replayConstant`, +whose `.thmInfo` case is the one change, and the loop in `replayParallel`. -/ namespace Lean.Kernel.Environment namespace ParallelReplay -structure Context where - newConstants : Std.HashMap Name ConstantInfo - -structure State where - env : Kernel.Environment - remaining : NameSet := {} - pending : NameSet := {} - postponedConstructors : NameSet := {} - postponedRecursors : NameSet := {} +/-- State added on top of `Replay.M`: the kernel checks of theorems, running in parallel. -/ +structure ExtraState where /-- Kernel checks of theorems, running in parallel; see `addThmAsync`. -/ tasks : Array (Name × Task (Except Kernel.Exception Kernel.Environment)) := #[] -abbrev M := ReaderT Context <| StateRefT State IO - -/-- Check if a `Name` still needs processing. If so, move it from `remaining` to `pending`. -/ -def isTodo (name : Name) : M Bool := do - let r := (← get).remaining - if r.contains name then - modify fun s => { s with remaining := s.remaining.erase name, pending := s.pending.insert name } - return true - else - return false - -/-- Use the current `Environment` to throw a `Kernel.Exception`. -/ -def throwKernelException (ex : Kernel.Exception) : M Unit := do - throw <| .userError <| (← ex.toMessageData {} |>.toString) - -/-- Add a declaration, possibly throwing a `Kernel.Exception`. -/ -def addDecl (d : Declaration) : M Unit := do - match (← get).env.addDeclCore 0 0 d (cancelTk? := none) with - | .ok env => modify fun s => { s with env := env } - | .error ex => throwKernelException ex +abbrev M := StateRefT ExtraState Replay.M /-- Add a theorem to the environment without checking it, and spawn a task that checks it with the kernel against the environment as it was before the theorem was added. -/ def addThmAsync (info : TheoremVal) : M Unit := do - let kenv := (← get).env + let kenv := (← getThe Replay.State).env let decl := Declaration.thmDecl info match kenv.addDeclWithoutChecking decl with | .ok env => let t := Task.spawn fun () => kenv.addDeclCore 0 0 decl (cancelTk? := none) - modify fun s => { s with env := env, tasks := s.tasks.push (info.name, t) } - | .error ex => throwKernelException ex + modifyThe Replay.State fun s => { s with env := env } + modifyThe ExtraState fun s => { s with tasks := s.tasks.push (info.name, t) } + | .error ex => Replay.throwKernelException ex mutual /-- -Check if a `Name` still needs to be processed (i.e. is in `remaining`). - -If so, recursively replay any constants it refers to, -to ensure we add declarations in the right order. - -The construct the `Declaration` from its stored `ConstantInfo`, -and add it to the environment. +`Replay.replayConstant`, in the monad `M`, except that theorems are added with `addThmAsync` instead +of `addDecl`. -/ partial def replayConstant (name : Name) : M Unit := do - if ← isTodo name then + if ← Replay.isTodo name then let some ci := (← read).newConstants[name]? | unreachable! replayConstants ci.getUsedConstantsAsSet -- Check that this name is still pending: a mutual block may have taken care of it. - if (← get).pending.contains name then + if (← getThe Replay.State).pending.contains name then try match ci with | .defnInfo info => - addDecl (Declaration.defnDecl info) + Replay.addDecl (Declaration.defnDecl info) | .thmInfo info => -- Ignore duplicate theorems. This code is identical to that in `finalizeImport` before it -- added extended duplicates support for the module system, which is not relevant for us -- here as we always load all .olean information. We need this case *because* of the module -- system -- as we have more data loaded than it, we might encounter duplicate private -- theorems where elaboration under the module system would have only one of them in scope. - if let some (.thmInfo info') := (← get).env.find? ci.name then + if let some (.thmInfo info') := (← getThe Replay.State).env.find? ci.name then if info.name == info'.name && info.type == info'.type && info.levelParams == info'.levelParams && @@ -118,15 +80,15 @@ partial def replayConstant (name : Name) : M Unit := do return addThmAsync info | .axiomInfo info => - addDecl (Declaration.axiomDecl info) + Replay.addDecl (Declaration.axiomDecl info) | .opaqueInfo info => - addDecl (Declaration.opaqueDecl info) + Replay.addDecl (Declaration.opaqueDecl info) | .inductInfo info => let lparams := info.levelParams let nparams := info.numParams let all ← info.all.mapM fun n => do pure <| ((← read).newConstants[n]!) for o in all do - modify fun s => + modifyThe Replay.State fun s => { s with remaining := s.remaining.erase o.name, pending := s.pending.erase o.name } let ctorInfo ← all.mapM fun ci => do pure (ci, ← ci.inductiveVal!.ctors.mapM fun n => do @@ -139,21 +101,23 @@ partial def replayConstant (name : Name) : M Unit := do { name := ci.name type := ci.type ctors := ctors.map fun ci => { name := ci.name, type := ci.type } } - addDecl (Declaration.inductDecl lparams nparams types false) + Replay.addDecl (Declaration.inductDecl lparams nparams types false) -- We postpone checking constructors, -- and at the end make sure they are identical -- to the constructors generated when we replay the inductives. | .ctorInfo info => - modify fun s => { s with postponedConstructors := s.postponedConstructors.insert info.name } + modifyThe Replay.State fun s => + { s with postponedConstructors := s.postponedConstructors.insert info.name } -- Similarly we postpone checking recursors. | .recInfo info => - modify fun s => { s with postponedRecursors := s.postponedRecursors.insert info.name } + modifyThe Replay.State fun s => + { s with postponedRecursors := s.postponedRecursors.insert info.name } | .quotInfo _ => -- `Quot.lift` and `Quot.ind` have types that reference `Eq`, -- so we need to ensure `Eq` is replayed before adding the quotient declaration. replayConstant `Eq - addDecl (Declaration.quotDecl) - modify fun s => { s with pending := s.pending.erase name } + Replay.addDecl (Declaration.quotDecl) + modifyThe Replay.State fun s => { s with pending := s.pending.erase name } catch ex => throw <| .userError s!"while replaying declaration '{name}':\n{ex}" @@ -163,28 +127,6 @@ partial def replayConstants (names : NameSet) : M Unit := do end -/-- -Check that all postponed constructors are identical to those generated -when we replayed the inductives. --/ -def checkPostponedConstructors : M Unit := do - for ctor in (← get).postponedConstructors do - match (← get).env.find? ctor, (← read).newConstants[ctor]? with - | some (.ctorInfo info), some (.ctorInfo info') => - if ! (info == info') then throw <| IO.userError s!"Invalid constructor {ctor}" - | _, _ => throw <| IO.userError s!"No such constructor {ctor}" - -/-- -Check that all postponed recursors are identical to those generated -when we replayed the inductives. --/ -def checkPostponedRecursors : M Unit := do - for ctor in (← get).postponedRecursors do - match (← get).env.find? ctor, (← read).newConstants[ctor]? with - | some (.recInfo info), some (.recInfo info') => - if ! (info == info') then throw <| IO.userError s!"Invalid recursor {ctor}" - | _, _ => throw <| IO.userError s!"No such recursor {ctor}" - end ParallelReplay open ParallelReplay @@ -197,7 +139,7 @@ or if there are malformed recursors or constructors for inductive types. Theorems are checked in parallel tasks; non-theorem declarations are checked in order, as in `replay`. -/ -def replayParallel (newConstants : Std.HashMap Name ConstantInfo) (env : Kernel.Environment) : +public def replayParallel (newConstants : Std.HashMap Name ConstantInfo) (env : Kernel.Environment) : IO Kernel.Environment := do let mut remaining : NameSet := ∅ for (n, ci) in newConstants.toList do @@ -205,17 +147,18 @@ def replayParallel (newConstants : Std.HashMap Name ConstantInfo) (env : Kernel. -- Later we may want to handle partial constants. if !ci.isUnsafe && !ci.isPartial then remaining := remaining.insert n - let (_, s) ← StateRefT'.run (s := { env, remaining }) do - ReaderT.run (r := { newConstants }) do - for n in remaining do - replayConstant n + let (_, s) ← StateRefT'.run (s := ({ env, remaining } : Replay.State)) do + ReaderT.run (r := ({ newConstants } : Replay.Context)) do + let ((), extra) ← StateRefT'.run (s := ({} : ExtraState)) do + for n in remaining do + replayConstant n -- Wait for the kernel checks of all theorems. - for (name, t) in (← get).tasks do + for (name, t) in extra.tasks do if let .error ex := t.get then - try ParallelReplay.throwKernelException ex + try Replay.throwKernelException ex catch ex => throw <| .userError s!"while replaying declaration '{name}':\n{ex}" - checkPostponedConstructors - checkPostponedRecursors + Replay.checkPostponedConstructors + Replay.checkPostponedRecursors return s.env end Kernel.Environment From 431631cbb82392750250c648057265268c906aaa Mon Sep 17 00:00:00 2001 From: dpwoodru Date: Thu, 8 Oct 2026 22:06:46 +0000 Subject: [PATCH 3/4] refactor: make Comparator/Replay.lean a verbatim copy of Lean's replayConstant and replay This commit copies replayConstant, replayConstants and replay from Lean's src/Lean/Replay.lean (identical in v4.35.0-rc3, v4.35.0-rc4 and master) verbatim into namespace Lean.Kernel.Environment.Replay.Parallel, with M := Replay.M, so replayParallel temporarily behaves exactly like replay. The next commit is then the complete parallel change, as a diff against Lean's own code. --- Comparator/Replay.lean | 118 ++++++++++++++++------------------------- 1 file changed, 47 insertions(+), 71 deletions(-) diff --git a/Comparator/Replay.lean b/Comparator/Replay.lean index d7a23b3..5c201fb 100644 --- a/Comparator/Replay.lean +++ b/Comparator/Replay.lean @@ -12,83 +12,61 @@ import Lean.Util.FoldConsts /-! # `Lean.Kernel.Environment.replayParallel` -`replayParallel` is `Lean.Kernel.Environment.replay` (from `Lean.Replay`) with one change: theorems are -added to the environment with `addDeclWithoutChecking`, and each theorem is checked by the kernel -(`addDeclCore`) in a separate task against the environment as it was just before that theorem. -`replayParallel` waits for all of these tasks, and fails if any of them failed, before the postponed -constructor and recursor checks. Every declaration is therefore checked by the same kernel call against -the same environment as in `replay`; only the order in which theorems are checked differs. - -Everything else is reused from `Lean.Replay`: `Context`, `State`, `M`, `isTodo`, `throwKernelException`, -`addDecl` and the postponed constructor and recursor checks. They are not public there, hence -`import all Lean.Replay`. The only code copied from `Lean.Replay` (Lean v4.35.0-rc3) is `replayConstant`, -whose `.thmInfo` case is the one change, and the loop in `replayParallel`. +`replayConstant`, `replayConstants` and `replay` in namespace `Lean.Kernel.Environment.Replay.Parallel` below are +verbatim copies of the same definitions in `src/Lean/Replay.lean` (identical in Lean v4.35.0-rc3, v4.35.0-rc4 and +master). Everything they use from there (`Context`, `State`, `isTodo`, `throwKernelException`, `addDecl` and the +postponed constructor and recursor checks) is imported from `Lean.Replay`, with `import all` because those +definitions are not public. -/ -namespace Lean.Kernel.Environment - -namespace ParallelReplay - -/-- State added on top of `Replay.M`: the kernel checks of theorems, running in parallel. -/ -structure ExtraState where - /-- Kernel checks of theorems, running in parallel; see `addThmAsync`. -/ - tasks : Array (Name × Task (Except Kernel.Exception Kernel.Environment)) := #[] +namespace Lean.Kernel.Environment.Replay.Parallel -abbrev M := StateRefT ExtraState Replay.M - -/-- -Add a theorem to the environment without checking it, and spawn a task that checks it with the kernel -against the environment as it was before the theorem was added. --/ -def addThmAsync (info : TheoremVal) : M Unit := do - let kenv := (← getThe Replay.State).env - let decl := Declaration.thmDecl info - match kenv.addDeclWithoutChecking decl with - | .ok env => - let t := Task.spawn fun () => kenv.addDeclCore 0 0 decl (cancelTk? := none) - modifyThe Replay.State fun s => { s with env := env } - modifyThe ExtraState fun s => { s with tasks := s.tasks.push (info.name, t) } - | .error ex => Replay.throwKernelException ex +abbrev M := Replay.M mutual /-- -`Replay.replayConstant`, in the monad `M`, except that theorems are added with `addThmAsync` instead -of `addDecl`. +Check if a `Name` still needs to be processed (i.e. is in `remaining`). + +If so, recursively replay any constants it refers to, +to ensure we add declarations in the right order. + +The construct the `Declaration` from its stored `ConstantInfo`, +and add it to the environment. -/ partial def replayConstant (name : Name) : M Unit := do - if ← Replay.isTodo name then + if ← isTodo name then let some ci := (← read).newConstants[name]? | unreachable! replayConstants ci.getUsedConstantsAsSet -- Check that this name is still pending: a mutual block may have taken care of it. - if (← getThe Replay.State).pending.contains name then + if (← get).pending.contains name then try match ci with | .defnInfo info => - Replay.addDecl (Declaration.defnDecl info) + addDecl (Declaration.defnDecl info) | .thmInfo info => -- Ignore duplicate theorems. This code is identical to that in `finalizeImport` before it -- added extended duplicates support for the module system, which is not relevant for us -- here as we always load all .olean information. We need this case *because* of the module -- system -- as we have more data loaded than it, we might encounter duplicate private -- theorems where elaboration under the module system would have only one of them in scope. - if let some (.thmInfo info') := (← getThe Replay.State).env.find? ci.name then + if let some (.thmInfo info') := (← get).env.find? ci.name then if info.name == info'.name && info.type == info'.type && info.levelParams == info'.levelParams && info.all == info'.all then return - addThmAsync info + addDecl (Declaration.thmDecl info) | .axiomInfo info => - Replay.addDecl (Declaration.axiomDecl info) + addDecl (Declaration.axiomDecl info) | .opaqueInfo info => - Replay.addDecl (Declaration.opaqueDecl info) + addDecl (Declaration.opaqueDecl info) | .inductInfo info => let lparams := info.levelParams let nparams := info.numParams let all ← info.all.mapM fun n => do pure <| ((← read).newConstants[n]!) for o in all do - modifyThe Replay.State fun s => + modify fun s => { s with remaining := s.remaining.erase o.name, pending := s.pending.erase o.name } let ctorInfo ← all.mapM fun ci => do pure (ci, ← ci.inductiveVal!.ctors.mapM fun n => do @@ -101,23 +79,21 @@ partial def replayConstant (name : Name) : M Unit := do { name := ci.name type := ci.type ctors := ctors.map fun ci => { name := ci.name, type := ci.type } } - Replay.addDecl (Declaration.inductDecl lparams nparams types false) + addDecl (Declaration.inductDecl lparams nparams types false) -- We postpone checking constructors, -- and at the end make sure they are identical -- to the constructors generated when we replay the inductives. | .ctorInfo info => - modifyThe Replay.State fun s => - { s with postponedConstructors := s.postponedConstructors.insert info.name } + modify fun s => { s with postponedConstructors := s.postponedConstructors.insert info.name } -- Similarly we postpone checking recursors. | .recInfo info => - modifyThe Replay.State fun s => - { s with postponedRecursors := s.postponedRecursors.insert info.name } + modify fun s => { s with postponedRecursors := s.postponedRecursors.insert info.name } | .quotInfo _ => -- `Quot.lift` and `Quot.ind` have types that reference `Eq`, -- so we need to ensure `Eq` is replayed before adding the quotient declaration. replayConstant `Eq - Replay.addDecl (Declaration.quotDecl) - modifyThe Replay.State fun s => { s with pending := s.pending.erase name } + addDecl (Declaration.quotDecl) + modify fun s => { s with pending := s.pending.erase name } catch ex => throw <| .userError s!"while replaying declaration '{name}':\n{ex}" @@ -127,19 +103,13 @@ partial def replayConstants (names : NameSet) : M Unit := do end -end ParallelReplay - -open ParallelReplay - /-- "Replay" some constants into a `Kernel.Environment`, sending them to the kernel for checking. Throws a `IO.userError` if the kernel rejects a constant, or if there are malformed recursors or constructors for inductive types. - -Theorems are checked in parallel tasks; non-theorem declarations are checked in order, as in `replay`. -/ -public def replayParallel (newConstants : Std.HashMap Name ConstantInfo) (env : Kernel.Environment) : +public def replay (newConstants : Std.HashMap Name ConstantInfo) (env : Kernel.Environment) : IO Kernel.Environment := do let mut remaining : NameSet := ∅ for (n, ci) in newConstants.toList do @@ -147,18 +117,24 @@ public def replayParallel (newConstants : Std.HashMap Name ConstantInfo) (env : -- Later we may want to handle partial constants. if !ci.isUnsafe && !ci.isPartial then remaining := remaining.insert n - let (_, s) ← StateRefT'.run (s := ({ env, remaining } : Replay.State)) do - ReaderT.run (r := ({ newConstants } : Replay.Context)) do - let ((), extra) ← StateRefT'.run (s := ({} : ExtraState)) do - for n in remaining do - replayConstant n - -- Wait for the kernel checks of all theorems. - for (name, t) in extra.tasks do - if let .error ex := t.get then - try Replay.throwKernelException ex - catch ex => throw <| .userError s!"while replaying declaration '{name}':\n{ex}" - Replay.checkPostponedConstructors - Replay.checkPostponedRecursors + let (_, s) ← StateRefT'.run (s := { env, remaining }) do + ReaderT.run (r := { newConstants }) do + for n in remaining do + replayConstant n + checkPostponedConstructors + checkPostponedRecursors return s.env -end Kernel.Environment +end Lean.Kernel.Environment.Replay.Parallel + +namespace Lean.Kernel.Environment + +/-- +"Replay" some constants into a `Kernel.Environment`, sending them to the kernel for checking: the variant of +`Lean.Kernel.Environment.replay` defined above. +-/ +public def replayParallel (newConstants : Std.HashMap Name ConstantInfo) (env : Kernel.Environment) : + IO Kernel.Environment := + Replay.Parallel.replay newConstants env + +end Lean.Kernel.Environment From b005862ddca3c3f88c611ea6d24bb8d97e62af5b Mon Sep 17 00:00:00 2001 From: dpwoodru Date: Thu, 8 Oct 2026 22:07:46 +0000 Subject: [PATCH 4/4] feat: check theorems in parallel in replayParallel The complete parallel change, as a diff against the verbatim copy of Lean's replayConstant and replay in the previous commit: - the .thmInfo case of replayConstant calls addThmAsync instead of addDecl: the theorem is added with addDeclWithoutChecking and checked by the same kernel call (addDeclCore) against the environment just before it, in a Task; - the reader context extends Replay.Context with the list of these tasks (the Lean.Replay helpers are lifted into the new monad unchanged); - replay creates the list and awaits every task before the postponed constructor/recursor checks, failing if any task failed. --- Comparator/Replay.lean | 50 +++++++++++++++++++++++++++++++++++++----- 1 file changed, 44 insertions(+), 6 deletions(-) diff --git a/Comparator/Replay.lean b/Comparator/Replay.lean index 5c201fb..a1538fc 100644 --- a/Comparator/Replay.lean +++ b/Comparator/Replay.lean @@ -13,15 +13,47 @@ import Lean.Util.FoldConsts # `Lean.Kernel.Environment.replayParallel` `replayConstant`, `replayConstants` and `replay` in namespace `Lean.Kernel.Environment.Replay.Parallel` below are -verbatim copies of the same definitions in `src/Lean/Replay.lean` (identical in Lean v4.35.0-rc3, v4.35.0-rc4 and -master). Everything they use from there (`Context`, `State`, `isTodo`, `throwKernelException`, `addDecl` and the +copies of the same definitions in `src/Lean/Replay.lean` (identical in Lean v4.35.0-rc3, v4.35.0-rc4 and master). +Everything they use from there (`Context`, `State`, `isTodo`, `throwKernelException`, `addDecl` and the postponed constructor and recursor checks) is imported from `Lean.Replay`, with `import all` because those -definitions are not public. +definitions are not public. The copies differ from Lean's only in: + +* the `.thmInfo` case of `replayConstant` calls `addThmAsync` instead of `addDecl`: the theorem is added with + `addDeclWithoutChecking`, and checked by the same kernel call (`addDeclCore`) against the environment as it was + just before it, in a separate task; +* the reader context `Context` extends `Replay.Context` with the list of these tasks; +* `replay` creates that list, and waits for all tasks before the postponed constructor and recursor checks, + failing if any task failed. + +So every declaration is checked by the same kernel call against the same environment as in `replay`; only the +order in which theorems are checked differs. -/ namespace Lean.Kernel.Environment.Replay.Parallel -abbrev M := Replay.M +/-- `Replay.Context`, plus the kernel checks of theorems running in parallel (see `addThmAsync`). -/ +structure Context extends Replay.Context where + tasks : IO.Ref (Array (Name × Task (Except Kernel.Exception Kernel.Environment))) + +abbrev M := ReaderT Context <| StateRefT State IO + +/-- The helpers of `Lean.Replay` (`isTodo`, `addDecl`, ...) run unchanged in `M`. -/ +instance : MonadLift Replay.M M where + monadLift x := fun ctx => x.run ctx.toContext + +/-- +Add a theorem to the environment without checking it, and spawn a task that checks it with the kernel +against the environment as it was before the theorem was added. +-/ +def addThmAsync (info : TheoremVal) : M Unit := do + let kenv := (← get).env + let decl := Declaration.thmDecl info + match kenv.addDeclWithoutChecking decl with + | .ok env => + let t := Task.spawn fun () => kenv.addDeclCore 0 0 decl (cancelTk? := none) + modify fun s => { s with env := env } + (← read).tasks.modify (·.push (info.name, t)) + | .error ex => throwKernelException ex mutual /-- @@ -56,7 +88,7 @@ partial def replayConstant (name : Name) : M Unit := do info.all == info'.all then return - addDecl (Declaration.thmDecl info) + addThmAsync info | .axiomInfo info => addDecl (Declaration.axiomDecl info) | .opaqueInfo info => @@ -117,10 +149,16 @@ public def replay (newConstants : Std.HashMap Name ConstantInfo) (env : Kernel.E -- Later we may want to handle partial constants. if !ci.isUnsafe && !ci.isPartial then remaining := remaining.insert n + let tasks ← IO.mkRef #[] let (_, s) ← StateRefT'.run (s := { env, remaining }) do - ReaderT.run (r := { newConstants }) do + ReaderT.run (r := { newConstants, tasks }) do for n in remaining do replayConstant n + -- Wait for the kernel checks of all theorems; any failure fails the replay. + for (name, t) in ← tasks.get do + if let .error ex := t.get then + try throwKernelException ex + catch ex => throw <| .userError s!"while replaying declaration '{name}':\n{ex}" checkPostponedConstructors checkPostponedRecursors return s.env