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

perf: avoid kernel env block in realizeConst (#11617)

Browse source
This commit is contained in:
Sebastian Ullrich 2025-12-12 12:20:20 +01:00 • committed by GitHub
parent ad02aa159c
commit 9f74e71f10
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 9 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Lean/Environment.lean
View file

@ -2446,14 +2446,14 @@ def replayConsts (dest : Environment) (oldEnv newEnv : Environment) (skipExistin
}
checked := dest.checked.map fun kenv =>
replayKernel
oldEnv.toKernelEnv.extensions newEnv.toKernelEnv.extensions exts newPrivateConsts kenv
oldEnv.checked newEnv.checked 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 (oldState newState : Array EnvExtensionState)
replayKernel (oldEnv newEnv : Task Kernel.Environment)
(exts : Array (EnvExtension EnvExtensionState)) (consts : List AsyncConst)
(kenv : Kernel.Environment) : Except Kernel.Exception Kernel.Environment := do
let mut kenv := kenv
@ -2464,8 +2464,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 oldState)
(ext.getStateImpl newState)
(ext.getStateImpl oldEnv.get.extensions)
(ext.getStateImpl newEnv.get.extensions)
(consts.map (·.constInfo.name))) }
for c in consts do
if skipExisting && (kenv.find? c.constInfo.name).isSome then
@ -2613,9 +2613,12 @@ def realizeConst (env : Environment) (forConst : Name) (constName : Name)
let exts ← EnvExtension.envExtensionsRef.get
-- 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.
-- stored in a promise in there, creating a cycle. The closures stored in
-- `realizeEnv(').checked` should uphold this property as they are only concerned about the
-- kernel env but this cannot directly be enforced or checked except through the leak sanitizer
-- CI build.
let replayKernel := replayConsts.replayKernel (skipExisting := true)
realizeEnv.toKernelEnv.extensions realizeEnv'.toKernelEnv.extensions exts newPrivateConsts
realizeEnv.checked realizeEnv'.checked exts newPrivateConsts
let res : RealizeConstResult := { newConsts.private := newPrivateConsts, newConsts.public := newPublicConsts, replayKernel, dyn }
pure (.mk res)
let some res := res.get? RealizeConstResult | unreachable!