From bfbad5354081a9654c8fcf42d39e32b8fae49d3d Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 24 Nov 2025 11:16:56 +0100
Subject: [PATCH] fix: avoid storing reference to environment in realization
 result to prevent promise cycle (#11328)

This PR fixes freeing memory accidentally retained for each document
version in the language server on certain elaboration workloads. The
issue must have existed since 4.18.0.
---
 src/Lean/Environment.lean                | 18 +++++++++++++-----
 src/Lean/Meta/Basic.lean                 |  3 +++
 tests/bench/speedcenter.exec.velcom.yaml | 10 ++++++++++
 3 files changed, 26 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 1dd8c50543..1abcf4886d 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -2443,13 +2443,17 @@ def replayConsts (dest : Environment) (oldEnv newEnv : Environment) (skipExistin
         else
           consts.add c
     }
-    checked := dest.checked.map fun kenv => replayKernel exts newPrivateConsts kenv |>.toOption.getD kenv
+    checked := dest.checked.map fun kenv =>
+      replayKernel
+        oldEnv.toKernelEnv.extensions newEnv.toKernelEnv.extensions exts newPrivateConsts kenv
+      |>.toOption.getD kenv
     allRealizations := dest.allRealizations.map (sync := true) fun allRealizations =>
       newPrivateConsts.foldl (init := allRealizations) fun allRealizations c =>
         allRealizations.insert c.constInfo.name c
   }
 where
-  replayKernel (exts : Array (EnvExtension EnvExtensionState)) (consts : List AsyncConst)
+  replayKernel (oldState newState : Array EnvExtensionState)
+      (exts : Array (EnvExtension EnvExtensionState)) (consts : List AsyncConst)
       (kenv : Kernel.Environment) : Except Kernel.Exception Kernel.Environment := do
     let mut kenv := kenv
     -- replay extensions first in case kernel checking needs them (`IR.declMapExt`)
@@ -2459,8 +2463,8 @@ where
           -- safety: like in `modifyState`, but that one takes an elab env instead of a kernel env
           extensions := unsafe (ext.modifyStateImpl kenv.extensions <|
             replay
-              (ext.getStateImpl oldEnv.toKernelEnv.extensions)
-              (ext.getStateImpl newEnv.toKernelEnv.extensions)
+              (ext.getStateImpl oldState)
+              (ext.getStateImpl newState)
               (consts.map (·.constInfo.name))) }
     for c in consts do
       if skipExisting && (kenv.find? c.constInfo.name).isSome then
@@ -2602,7 +2606,11 @@ def realizeConst (env : Environment) (forConst : Name) (constName : Name)
         { c with exts? := some <| .pure realizeEnv'.base.private.extensions }
       else c
     let exts ← EnvExtension.envExtensionsRef.get
-    let replayKernel := replayConsts.replayKernel (skipExisting := true) realizeEnv realizeEnv' exts newPrivateConsts
+    -- NOTE: We must ensure that `realizeEnv.localRealizationCtxMap` is not reachable via `res`
+    -- (such as by storing `realizeEnv` or `realizeEnv'` in a field or the closure) as `res` will be
+    -- stored in a promise in there, creating a cycle.
+    let replayKernel := replayConsts.replayKernel (skipExisting := true)
+      realizeEnv.toKernelEnv.extensions realizeEnv'.toKernelEnv.extensions exts newPrivateConsts
     let res : RealizeConstResult := { newConsts.private := newPrivateConsts, newConsts.public := newPublicConsts, replayKernel, dyn }
     pure (.mk res)
   let some res := res.get? RealizeConstResult | unreachable!
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 6e3cbeed1c..a5ec6a6a69 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -2534,6 +2534,9 @@ generated diagnostics is deterministic). Note that, as `realize` is run using th
 declaration time of `forConst`, trace options must be set prior to that (or, for imported constants,
 on the cmdline) in order to be active. If `realize` throws an exception, it is rethrown at all
 callers.
+
+CAVEAT: `realize` MUST NOT reference the current environment (the result of `getEnv`) in its result
+to avoid creating an un-collectable promise cycle.
 -/
 def realizeValue [BEq α] [Hashable α] [TypeName α] [TypeName β] (forConst : Name) (key : α) (realize : MetaM β) :
     MetaM β := do
diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml
index 4191ea53db..d2b6ec8697 100644
--- a/tests/bench/speedcenter.exec.velcom.yaml
+++ b/tests/bench/speedcenter.exec.velcom.yaml
@@ -141,6 +141,16 @@
     cmd: lean --run ../script/benchReelabWatchdogRss.lean lean Init/Data/List/Sublist.lean 10 -j4 -Dexperimental.module=true
     max_runs: 2
     parse_output: true
+# This benchmark uncovered the promise cycle in `realizeConst` (#11328)
+- attributes:
+    description: Init.Data.List.Basic re-elab
+    tags: [other]
+  run_config:
+    <<: *time
+    cwd: ../../src
+    cmd: lean --run ../script/benchReelabRss.lean lean Init/Data/List/Basic.lean 10 -j4 -Dexperimental.module=true
+    max_runs: 2
+    parse_output: true
 - attributes:
     description: import Lean
     tags: [other]