From f58e893e632ee954a6153a99184650ed80cb10ff Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 4 Mar 2025 14:41:30 +0100
Subject: [PATCH] chore: Mathlib fixes (#7327)

* chore: revert changes to Environment.replay
* chore: disable realizeConst for now when Elab.async is not set
---
 src/Lean/Meta/Basic.lean |  4 ++++
 src/Lean/Replay.lean     | 11 +++--------
 2 files changed, 7 insertions(+), 8 deletions(-)

diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 944f4b34f5..6879f321bf 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -2271,6 +2271,10 @@ def realizeConst (forConst : Name) (constName : Name) (realize : MetaM Unit) :
   -- the relevant local environment extension state when accessed on this branch.
   if env.containsOnBranch constName then
     return
+  -- TODO: remove when Mathlib passes without it
+  if !Elab.async.get (← getOptions) then
+    realize
+    return
   withTraceNode `Meta.realizeConst (fun _ => return constName) do
     let coreCtx ← readThe Core.Context
     let coreCtx := {
diff --git a/src/Lean/Replay.lean b/src/Lean/Replay.lean
index c41c16f92b..1bdd26868f 100644
--- a/src/Lean/Replay.lean
+++ b/src/Lean/Replay.lean
@@ -22,10 +22,6 @@ after replaying any inductive definitions occurring in `constantMap`.
 * a verifier for an `Environment`, by sending everything to the kernel, or
 * a mechanism to safely transfer constants from one `Environment` to another.
 
-## Deprecation note
-
-We've decided that this code should live in the `https://github.com/leanprover/lean4checker` repository,
-rather than the core distribution. This code is now deprecated, and will be removed in a future release.
 -/
 
 namespace Lean.Environment
@@ -36,7 +32,7 @@ structure Context where
   newConstants : Std.HashMap Name ConstantInfo
 
 structure State where
-  env : Kernel.Environment
+  env : Environment
   remaining : NameSet := {}
   pending : NameSet := {}
   postponedConstructors : NameSet := {}
@@ -157,7 +153,6 @@ open Replay
 Throws a `IO.userError` if the kernel rejects a constant,
 or if there are malformed recursors or constructors for inductive types.
 -/
-@[deprecated "Use the `lean4checker` package instead" (since := "2025-03-04")]
 def replay (newConstants : Std.HashMap Name ConstantInfo) (env : Environment) : IO Environment := do
   let mut remaining : NameSet := ∅
   for (n, ci) in newConstants.toList do
@@ -165,10 +160,10 @@ def replay (newConstants : Std.HashMap Name ConstantInfo) (env : Environment) :
     -- 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
+  let (_, s) ← StateRefT'.run (s := { env, remaining }) do
     ReaderT.run (r := { newConstants }) do
       for n in remaining do
         replayConstant n
       checkPostponedConstructors
       checkPostponedRecursors
-  return .ofKernelEnv s.env
+  return s.env