Proposal. Add an opt-in parallel mode to Lean.Kernel.Environment.replay (src/Lean/Replay.lean):
- Theorems: each theorem is added with
addDeclWithoutChecking. It is checked by the same kernel call (addDeclCore) against the environment as it was just before it, in a Task.
- Before finishing: all tasks are awaited before the postponed constructor and recursor checks, and any failure fails the replay.
- Everything else: non-theorem declarations are still checked in order on one thread.
Every declaration is checked by the same call against the same environment as today; only the order of the theorem checks changes. Cycles stay impossible, because a theorem is checked against an environment that contains neither it nor anything after it.
Size of the change. It's small, about 25 lines:
- the
.thmInfo case of replayConstant;
- a task list in the reader context;
- a loop in
replay that awaits the tasks.
A working version is in leanprover/comparator#99: this commit is the whole change, written against a verbatim copy of replayConstant and replay (previous commit). Its tests check that it gives the same verdict as replay, both on valid input and on forged input: ill-typed proofs, an ill-typed lemma used later, cyclic theorems and an ill-typed definition.
Why in core. Comparator and similar checkers use replay to re-check a whole exported environment. In leanprover/comparator#99, @eric-wieser suggested core is the better home. Comparator would then need no copy of Replay.lean at all, which keeps its trusted code small.
User experience. It would be opt-in, for example a parallel : Bool := false argument or a separate function, so existing users see no change.
Beneficiaries. Anyone who replays very large environments. Our case is https://github.com/dpwoodru/general-courtade-kumar-lean: a ~100 GB export with 22.1M constants, mostly decide proofs of generated certificates.
- Single-threaded
replay was projected at one to two weeks.
- The parallel version replayed it in 83 h on one machine with 342 threads, and accepted it.
Community feedback. This was discussed in leanprover/comparator#95 and #99 (@eric-wieser, @nomeata). @nomeata noted that the FRO hasn't yet decided whether the official replay should be multi-threaded; this issue is meant to make that decision concrete.
Maintainability. The change is small and local to Replay.lean, and the sequential path is unchanged.
Happy to send a PR if this direction is acceptable. The prototype was written with AI coding assistance.
Proposal. Add an opt-in parallel mode to
Lean.Kernel.Environment.replay(src/Lean/Replay.lean):addDeclWithoutChecking. It is checked by the same kernel call (addDeclCore) against the environment as it was just before it, in aTask.Every declaration is checked by the same call against the same environment as today; only the order of the theorem checks changes. Cycles stay impossible, because a theorem is checked against an environment that contains neither it nor anything after it.
Size of the change. It's small, about 25 lines:
.thmInfocase ofreplayConstant;replaythat awaits the tasks.A working version is in leanprover/comparator#99: this commit is the whole change, written against a verbatim copy of
replayConstantandreplay(previous commit). Its tests check that it gives the same verdict asreplay, both on valid input and on forged input: ill-typed proofs, an ill-typed lemma used later, cyclic theorems and an ill-typed definition.Why in core. Comparator and similar checkers use
replayto re-check a whole exported environment. In leanprover/comparator#99, @eric-wieser suggested core is the better home. Comparator would then need no copy ofReplay.leanat all, which keeps its trusted code small.User experience. It would be opt-in, for example a
parallel : Bool := falseargument or a separate function, so existing users see no change.Beneficiaries. Anyone who replays very large environments. Our case is https://github.com/dpwoodru/general-courtade-kumar-lean: a ~100 GB export with 22.1M constants, mostly
decideproofs of generated certificates.replaywas projected at one to two weeks.Community feedback. This was discussed in leanprover/comparator#95 and #99 (@eric-wieser, @nomeata). @nomeata noted that the FRO hasn't yet decided whether the official replay should be multi-threaded; this issue is meant to make that decision concrete.
Maintainability. The change is small and local to
Replay.lean, and the sequential path is unchanged.Happy to send a PR if this direction is acceptable. The prototype was written with AI coding assistance.