feat: optional parallel kernel replay (parallel_replay)

[dpwoodru]

Closes #95.

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. That file imports Lean.Replay (via import all) and contains copies of Lean's replayConstant, replayConstants and replay, with three small changes:

• the theorem case of replayConstant adds the theorem with addDeclWithoutChecking and checks it with addDeclCore, against the environment just before it, in a Task;
• the reader context carries the list of tasks;
• replay awaits them.

Reviewing. Commit 431631c copies those three definitions verbatim from Lean's src/Lean/Replay.lean (identical in v4.35.0-rc3, v4.35.0-rc4 and master). So commit b005862 shows the complete change against Lean's own code. As suggested in review, the same change is proposed for Lean core in leanprover/lean4#15569; if it lands there, this file can go away.

All tasks are awaited before the postponed constructor/recursor checks, and any kernel error fails the replay. Non-theorem declarations are checked in order as before, and the default sequential path is unchanged.

Tests:

• tests/ParallelReplayUnit.lean checks that the verdict matches replay on valid and forged inputs. It is added to CI.
• Two new integration tests: parallel_match and parallel_olean_issue.

Motivation: the export of https://github.com/dpwoodru/general-courtade-kumar-lean is ~100 GB, with 22.1M constants, mostly decide proofs of generated certificates. A single-threaded replay was projected at one to two weeks. A build of this approach for Lean 4.33.1 replayed it in 83 h with 342 threads on one machine and accepted the solution. Details are in verification/comparator/results/2026-10-04/ of that repository.

This change was drafted with AI coding assistance.

[eric-wieser]

Do you need to copy the whole file? The more you can use by importing the previous file the better, since that reduces the size of the TCB.

[dpwoodru]

good point, thanks! pushed a refactor: it now imports Lean.Replay and reuses Context, State, M, isTodo, addDecl, throwKernelException and the postponed ctor/rec checks. the only copied code left is replayConstant (its .thmInfo case is the actual change) and the loop in replayParallel. one catch: those helpers aren't public in core, so this uses import all Lean.Replay. if you'd rather avoid that, happy to send a small lean4 PR that makes them public (or adds a hook for the theorem case) so comparator doesn't need to copy anything.

[eric-wieser]

For instance

Suggested change

	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)) := #[]
	structure State extends Replay.State where
	/-- Kernel checks of theorems, running in parallel; see `addThmAsync`. -/
	tasks : Array (Name × Task (Except Kernel.Exception Kernel.Environment)) := #[]

[dpwoodru]

went with your ExtraState version instead, since stacking it on Replay.M lets the core helpers be reused as is.

[eric-wieser]

Maybe the answer here to minimize the repetition is

structure ExtraState where
 tasks : Array (Name × Task (Except Kernel.Exception Kernel.Environment)) := #[]

abbrev M := StateRefT ExtraState (Replay.M)

[dpwoodru]

done, thanks: abbrev M := StateRefT ExtraState Replay.M.

[eric-wieser]

This doesn't seem to be what you have? Did you change your mind?

[dpwoodru]

yes, sorry, i should have said: i changed it in the latest push to keep the copied code verbatim. with StateRefT ExtraState Replay.M the outer state is ExtraState, so every get/modify in the copied replayConstant had to become getThe Replay.State/modifyThe Replay.State (that's what 1164baa did). putting the task list in the reader context instead (structure Context extends Replay.Context with an IO.Ref) keeps get, modify and read meaning what they mean in lean's code, so the copy is identical except the theorem case, and a MonadLift Replay.M M instance runs the Lean.Replay helpers unchanged. happy to switch back if you prefer the ExtraState version.

[nomeata]

If you don't want to wait for us to decide if we want the official kernel replay to be mutl-threaded, you can

• package it up in your own checker.
• use only the other kernels (nanoda, con-leche, con-ron), all of which support parallel checking

(I'm actually tweaking con-leche right now to reduce the serial part further, including parallizing the JSON parsing, precisely to make huge proofs like yours bearable.)

[dpwoodru]

thanks joachim, that's really helpful. happy to leave #99 open until you decide, no rush. in the meantime we'll try nanoda and con-leche on our export. is there a supported way to run comparator with only the external kernels (right now it always runs the builtin replay too), or should we run them directly on the lean4export output? and if it's useful for your con-leche work, our export is a decent stress test: ~105 GB (lean 4.33.1), 22.1M constants, 9.65M theorems, mostly decide-heavy certificates. the builtin replay took 83 h with 342 threads. happy to share timings.

[nomeata]

is there a supported way to run comparator with only the external kernels

Doesn’t look like it, unfortunately, but I think it is a reasonable request.

Happy to learn how con-leche fares on your huge export, and give you a sneak preview on the more parallel version, but let’s continue this on zulip maybe?

[dpwoodru]

thanks! con-leche accepted the whole export once we raised its loop step budgets (the official build runs out of fuel on one big decide +kernel proof). details and a fuel request are in leanprover/con-leche#10, and the external-kernels-only request is #102. happy to continue on zulip too.

[dpwoodru]

@eric-wieser thanks, that makes sense. two changes:

• to make it reviewable: 431631c is a verbatim copy of lean's replayConstant, replayConstants and replay (identical in rc3, rc4 and master), so b005862 shows the whole change as a diff against lean's own code: the theorem case, a task list in the reader context, and the await loop in replay. everything else is imported from Lean.Replay
• for core: i opened RFC: opt-in parallel theorem checking in Lean.Kernel.Environment.replay lean4#15569 (an RFC, since lean4 asks for an issue before a PR) proposing the same opt-in mode for Kernel.Environment.replay. if it lands, comparator won't need any copy

i also merged master (rc4) into the branch.