From b7380758ae54ef60b109b7e5325075912e437958 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 18 Mar 2026 23:11:42 +0100 Subject: [PATCH] refactor: remove `Lean.Environment.replay` from core (#12972) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- src/Lean/Replay.lean | 27 ++- src/LeanChecker.lean | 5 +- src/LeanChecker/Replay.lean | 194 ------------------ tests/elab/issue12819.lean | 14 ++ .../leanchecker/LeanCheckerTests/QuotEq.lean | 3 +- 5 files changed, 38 insertions(+), 205 deletions(-) delete mode 100644 src/LeanChecker/Replay.lean create mode 100644 tests/elab/issue12819.lean diff --git a/src/Lean/Replay.lean b/src/Lean/Replay.lean index 8d16a32bf6..065a8ca2e8 100644 --- a/src/Lean/Replay.lean +++ b/src/Lean/Replay.lean @@ -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 diff --git a/src/LeanChecker.lean b/src/LeanChecker.lean index f665d6f124..48cb20f85c 100644 --- a/src/LeanChecker.lean +++ b/src/LeanChecker.lean @@ -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 diff --git a/src/LeanChecker/Replay.lean b/src/LeanChecker/Replay.lean deleted file mode 100644 index 2a9afe2c65..0000000000 --- a/src/LeanChecker/Replay.lean +++ /dev/null @@ -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 diff --git a/tests/elab/issue12819.lean b/tests/elab/issue12819.lean new file mode 100644 index 0000000000..4503e5e038 --- /dev/null +++ b/tests/elab/issue12819.lean @@ -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 diff --git a/tests/pkg/leanchecker/LeanCheckerTests/QuotEq.lean b/tests/pkg/leanchecker/LeanCheckerTests/QuotEq.lean index b7ec3ed52f..f13f8ce0a8 100644 --- a/tests/pkg/leanchecker/LeanCheckerTests/QuotEq.lean +++ b/tests/pkg/leanchecker/LeanCheckerTests/QuotEq.lean @@ -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!"