max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: remove Lean.Environment.replay from core (#12972)

Browse source 
This PR removes the obsolete `Lean.Environment.replay` from
`src/Lean/Replay.lean` and replaces it with the improved version from
`src/LeanChecker/Replay.lean`, which includes fixes for duplicate
theorem handling and Quot/Eq dependency ordering. The primed names
(`Replay'`, `replay'`) are renamed back to `Replay` and `replay`.

A test for the original issue (nested inductives failing with `replay`)
is added as `tests/elab/issue12819.lean`.

Closes #12819

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This commit is contained in:
Joachim Breitner 2026-03-18 23:11:42 +01:00 • committed by GitHub
parent 24ee19e405
commit b7380758ae
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
5 changed files with 38 additions and 205 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
src/Lean/Replay.lean
View file

@ -6,9 +6,9 @@ Authors: Kim Morrison
module
prelude
import Lean.CoreM
public import Lean.AddDecl
public section
import Lean.Util.FoldConsts
/-!
# `Lean.Environment.replay`
@ -34,7 +34,7 @@ structure Context where
newConstants : Std.HashMap Name ConstantInfo
structure State where
env : Environment
env : Kernel.Environment
remaining : NameSet := {}
pending : NameSet := {}
postponedConstructors : NameSet := {}
@ -82,6 +82,18 @@ partial def replayConstant (name : Name) : M Unit := do
| .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
addDecl (Declaration.thmDecl info)
| .axiomInfo info =>
addDecl (Declaration.axiomDecl info)
@ -115,6 +127,9 @@ partial def replayConstant (name : Name) : M Unit := do
| .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 =>
@ -158,17 +173,17 @@ open Replay
Throws a `IO.userError` if the kernel rejects a constant,
or if there are malformed recursors or constructors for inductive types.
-/
def replay (newConstants : Std.HashMap Name ConstantInfo) (env : Environment) : IO Environment := do
public def replay (newConstants : Std.HashMap Name ConstantInfo) (env : Environment) : IO 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
let (_, s) ← StateRefT'.run (s := { env := env.toKernelEnv, remaining }) do
ReaderT.run (r := { newConstants }) do
for n in remaining do
replayConstant n
checkPostponedConstructors
checkPostponedRecursors
return s.env
return .ofKernelEnv s.env

5
src/LeanChecker.lean
View file

@ -5,7 +5,6 @@ Authors: Kim Morrison, Sebastian Ullrich
-/
import Lean.CoreM
import Lean.Replay
import LeanChecker.Replay
import Lake.Load.Manifest
open Lean
@ -31,12 +30,12 @@ unsafe def replayFromImports (module : Name) : IO Unit := do
-- Collect constants from last ("most private") part, which subsumes all prior ones
for name in parts[parts.size-1].1.constNames, ci in parts[parts.size-1].1.constants do
newConstants := newConstants.insert name ci
let env' ← env.replay' newConstants
let env' ← env.replay newConstants
env'.freeRegions
unsafe def replayFromFresh (module : Name) : IO Unit := do
Lean.withImportModules #[{module}] {} fun env => do
discard <| (← mkEmptyEnvironment).replay' env.constants.map₁
discard <| (← mkEmptyEnvironment).replay env.constants.map₁
/-- Read the name of the main module from the `lake-manifest`. -/
-- This has been copied from `ImportGraph.getCurrentModule` in the

194
src/LeanChecker/Replay.lean
View file

@ -1,194 +0,0 @@
/-
Copyright (c) 2023 Kim Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kim Morrison
-/
prelude
import Lean.CoreM
import Lean.AddDecl
import Lean.Util.FoldConsts
/-!
# `Lean.Environment.replay`
`replay env constantMap` will "replay" all the constants in `constantMap : HashMap Name ConstantInfo` into `env`,
sending each declaration to the kernel for checking.
`replay` 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`.
`replay` can be used either as:
* a verifier for an `Environment`, by sending everything to the kernel, or
* a mechanism to safely transfer constants from one `Environment` to another.
## Implementation notes
This is a patched version of `Lean.Environment.Replay`, which is in the `lean4` repository
up to `v4.18.0`, but will be deprecated in `v4.19.0` and then removed. Once it it removed,
the prime on the `Replay'` namespace, the prime on `Lean.Environment.replay'`
should be removed here.
-/
namespace Lean.Environment
namespace Replay'
structure Context where
newConstants : Std.HashMap Name ConstantInfo
structure State where
env : Kernel.Environment
remaining : NameSet := {}
pending : NameSet := {}
postponedConstructors : NameSet := {}
postponedRecursors : NameSet := {}
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 d (cancelTk? := none) with
| .ok env => modify fun s => { s with env := env }
| .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
addDecl (Declaration.thmDecl 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 Replay'
open Replay'
/--
"Replay" some constants into an `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.
-/
def replay' (newConstants : Std.HashMap Name ConstantInfo) (env : Environment) : IO 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 := env.toKernelEnv, remaining }) do
ReaderT.run (r := { newConstants }) do
for n in remaining do
replayConstant n
checkPostponedConstructors
checkPostponedRecursors
return .ofKernelEnv s.env

14
tests/elab/issue12819.lean Normal file
View file

@ -0,0 +1,14 @@
import Lean
open Lean Lean.Meta
inductive Nested where
| c : List Nested → Nested
run_meta show MetaM Unit from do
let env ← getEnv
let consts := env.constants.map₂.foldl (init := ∅) fun consts n info =>
consts.insert n info
let some importEnv := env.importEnv?
| unreachable!
let _ ← importEnv.replay consts

3
tests/pkg/leanchecker/LeanCheckerTests/QuotEq.lean
View file

@ -1,5 +1,4 @@
import Lean
import LeanChecker.Replay
-- Test: Quot/Eq dependency ordering
--
@ -29,6 +28,6 @@ open Lean
-- Replay from a fresh environment - this would fail before the fix
-- if Quot was processed before Eq
let freshEnv ← mkEmptyEnvironment
let _ ← freshEnv.replay' constants
let _ ← freshEnv.replay constants
IO.println "Replay succeeded!"