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

feat: introduce Lean.realizeValue for sharing computation results between compatible environment branches (#9798)

Browse source 
This PR introduces `Lean.realizeValue`, a new metaprogramming API for
parallelism-aware caching of `MetaM` computations
This commit is contained in:
Sebastian Ullrich 2025-08-09 19:19:29 +02:00 • committed by GitHub
parent 479da83f57
commit c970c74d66
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 233 additions and 136 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Data/Range/Polymorphic/RangeIterator.lean
View file

@ -441,7 +441,7 @@ instance RangeIterator.instIteratorLoop {su} [UpwardEnumerable α] [SupportsUppe
(f : (out : α) → UpwardEnumerable.LE least out → SupportsUpperBound.IsSatisfied upperBound out → (c : γ) → n (Subtype (fun s : ForInStep γ => Pl out c s)))
(next : α) (hl : UpwardEnumerable.LE least next) (hu : SupportsUpperBound.IsSatisfied upperBound next) : n γ := do
match ← f next hl hu acc with
| ⟨.yield acc', h⟩ =>
| ⟨.yield acc', _⟩ =>
match hs : UpwardEnumerable.succ? next with
| some next' =>
if hu : SupportsUpperBound.IsSatisfied upperBound next' then

11
src/Lean/CoreM.lean
View file

@ -570,8 +570,8 @@ register_builtin_option stderrAsMessages : Bool := {
Creates snapshot reporting given `withIsolatedStreams` output and diagnostics and traces from the
given state.
-/
def mkSnapshot (output : String) (ctx : Context) (st : State)
(desc : String := by exact decl_name%.toString) : BaseIO Language.SnapshotTree := do
def mkSnapshot? (output : String) (ctx : Context) (st : State)
(desc : String := by exact decl_name%.toString) : BaseIO (Option Language.SnapshotTree) := do
let mut msgs := st.messages
if !output.isEmpty then
msgs := msgs.add {
@ -580,7 +580,9 @@ def mkSnapshot (output : String) (ctx : Context) (st : State)
pos := ctx.fileMap.toPosition <| ctx.ref.getPos?.getD 0
data := output
}
return .mk {
if !msgs.hasUnreported && st.traceState.traces.isEmpty && st.snapshotTasks.isEmpty then
return none
return some <| .mk {
desc
diagnostics := (← Language.Snapshot.Diagnostics.ofMessageLog msgs)
traces := st.traceState
@ -617,7 +619,8 @@ def wrapAsyncAsSnapshot {α : Type} (act : α → CoreM Unit) (cancelTk? : Optio
let ctx ← readThe Core.Context
return fun a => do
match (← (f a).toBaseIO) with
| .ok (output, st) => mkSnapshot output ctx st desc
| .ok (output, st) =>
return (← mkSnapshot? output ctx st desc).getD (toSnapshotTree (default : SnapshotLeaf))
-- interrupt or abort exception as `try catch` above should have caught any others
| .error _ => default

258
src/Lean/Environment.lean
View file

@ -529,13 +529,6 @@ private structure VisibilityMap (α : Type) where
«public» : α
deriving Inhabited, Nonempty
/-- Realization results, to be replayed onto other branches. -/
private structure RealizationResult where
newConsts : VisibilityMap (List AsyncConst)
replayKernel : Kernel.Environment → Except Kernel.Exception Kernel.Environment
dyn : Dynamic
deriving Nonempty
/-- Context for `realizeConst` established by `enableRealizationsForConst`. -/
private structure RealizationContext where
/--
@ -545,12 +538,11 @@ private structure RealizationContext where
/-- Saved options. Empty for imported constants. -/
opts : Options
/--
`realizeConst _ c ..` adds a mapping from `c` to a task of the realization results: the newly
added constants (incl. extension data in `AsyncConst.exts?`), a function for replaying the
changes onto a derived kernel environment, and auxiliary data (always `SnapshotTree` in builtin
uses, but untyped to avoid cyclic module references).
`realizeValue _ key ..` adds a mapping from `(typeName key, key)` to a task of the realization
result (`RealizeValueResult` when called from `Lean.realizeValue`, `RealizeConstResult` from
`Environment.realizeConst`).
-/
constsRef : IO.Ref (NameMap (Task RealizationResult))
realizeMapRef : IO.Ref (NameMap NonScalar /- PHashMap α (Task Dynamic) -/)
/--
Elaboration-specific extension of `Kernel.Environment` that adds tracking of asynchronously
@ -596,19 +588,19 @@ structure Environment where
/-- Information about this asynchronous branch of the environment, if any. -/
private asyncCtx? : Option AsyncContext := none
/--
Realized constants belonging to imported declarations. Must be initialized by calling
Realized values belonging to imported declarations. Must be initialized by calling
`enableRealizationsForImports`.
-/
private realizedImportedConsts? : Option RealizationContext
private importRealizationCtx? : Option RealizationContext
/--
Realized constants belonging to local declarations. This is a map from local declarations, which
Realized values belonging to local declarations. This is a map from local declarations, which
need to be registered synchronously using `enableRealizationsForConst`, to their realization
context incl. a ref of realized constants.
context.
-/
private realizedLocalConsts : NameMap RealizationContext := {}
private localRealizationCtxMap : NameMap RealizationContext := {}
/--
Task collecting all realizations from the current and already-forked environment branches, akin to
how `checked` collects all declarations. We only use it as a fallback in
Task collecting all realized constants from the current and already-forked environment branches,
akin to how `checked` collects all declarations. We only use it as a fallback in
`findAsyncCore?`/`getState`; see there.
-/
private allRealizations : Task (NameMap AsyncConst) := .pure {}
@ -649,7 +641,7 @@ private def asyncConsts (env : Environment) : AsyncConsts :=
-- both cases, the environment should be temporary and not leak into elaboration.
@[export lean_elab_environment_of_kernel_env]
def ofKernelEnv (env : Kernel.Environment) : Environment :=
{ base.private := env, base.public := env, realizedImportedConsts? := none }
{ base.private := env, base.public := env, importRealizationCtx? := none }
@[export lean_elab_environment_to_kernel_env]
def toKernelEnv (env : Environment) : Kernel.Environment :=
@ -684,7 +676,7 @@ it.
-/
def importEnv? (env : Environment) : Option Environment :=
-- safety: `RealizationContext` is private
unsafe env.realizedImportedConsts?.map (unsafeCast (β := Environment) ·.env)
unsafe env.importRealizationCtx?.map (unsafeCast (β := Environment) ·.env)
/-- Forgets about the asynchronous context restrictions. Used only for `withoutModifyingEnv`. -/
def unlockAsync (env : Environment) : Environment :=
@ -869,25 +861,22 @@ def enableRealizationsForConst (env : Environment) (opts : Options) (c : Name) :
if !asyncCtx.mayContain c then
panic! s!"{c} is outside current context {asyncCtx.declPrefix}"
return env
if env.realizedLocalConsts.contains c then
if env.localRealizationCtxMap.contains c then
return env
return { env with realizedLocalConsts := env.realizedLocalConsts.insert c {
return { env with localRealizationCtxMap := env.localRealizationCtxMap.insert c {
-- safety: `RealizationContext` is private
env := unsafe unsafeCast env
opts
constsRef := (← IO.mkRef {}) } }
realizeMapRef := (← IO.mkRef {}) } }
def areRealizationsEnabledForConst (env : Environment) (c : Name) : Bool :=
(env.base.get env |>.const2ModIdx.contains c) || env.localRealizationCtxMap.contains c
/-- Returns debug output about the asynchronous state of the environment. -/
def dbgFormatAsyncState (env : Environment) : BaseIO String :=
return s!"\
asyncCtx.declPrefix: {repr <| env.asyncCtx?.map (·.declPrefix)}\
\nasyncConsts: {repr <| env.asyncConsts.revList.reverse.map (·.constInfo.name)}\
\nrealizedLocalConsts: {repr (← env.realizedLocalConsts.toList.mapM fun (n, ctx) => do
let consts := (← ctx.constsRef.get).toList
return (n, consts.map (·.1)))}
\nrealizedImportedConsts?: {repr <| (← env.realizedImportedConsts?.mapM fun ctx => do
return (← ctx.constsRef.get).toList.map fun (n, m?) =>
(n, m?.get.1.private.map (fun c : AsyncConst => c.constInfo.name.toString) |> toString))}
\nasyncConsts: {repr <| env.asyncConsts.revList.reverse.map (·.constInfo.name)}
\nbase.private.constants.map₂: {repr <| env.base.private.constants.map₂.toList.map (·.1)}"
/-- Returns debug output about the synchronous state of the environment. -/
@ -1158,7 +1147,7 @@ def setMainModule (env : Environment) (m : Name) : Environment := Id.run do
let env := env.modifyCheckedAsync ({ · with
header.mainModule := m
})
{ env with realizedImportedConsts? := env.realizedImportedConsts?.map ({ · with
{ env with importRealizationCtx? := env.importRealizationCtx?.map ({ · with
-- safety: `RealizationContext` is private
env := unsafe unsafeCast env
}) }
@ -1515,7 +1504,7 @@ def mkEmptyEnvironment (trustLevel : UInt32 := 0) : IO Environment := do
extensions := exts
irBaseExts := exts
}
realizedImportedConsts? := none
importRealizationCtx? := none
}
structure PersistentEnvExtensionState (α : Type) (σ : Type) where
@ -2189,7 +2178,7 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
let mut env : Environment := {
base.private := privateBase
base.public := publicBase
realizedImportedConsts? := none
importRealizationCtx? := none
serverBaseExts := (← setImportedEntries privateBase.extensions serverData)
}
if leakEnv then
@ -2215,11 +2204,11 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
Safety: There are no concurrent accesses to `env` at this point, assuming
extensions' `addImportFn`s did not spawn any unbound tasks. -/
env ← unsafe Runtime.markPersistent env
return { env with realizedImportedConsts? := some {
return { env with importRealizationCtx? := some {
-- safety: `RealizationContext` is private
env := unsafe unsafeCast env
opts
constsRef := (← IO.mkRef {})
realizeMapRef := (← IO.mkRef {})
} }
/--
@ -2432,98 +2421,123 @@ def hasUnsafe (env : Environment) (e : Expr) : Bool :=
| _ => false;
c?.isSome
/-- Plumbing function for `Lean.Meta.realizeValue`; see documentation there. -/
def realizeValue [BEq α] [Hashable α] [TypeName α] (env : Environment) (forConst : Name) (key : α)
(realize : Environment → Options → BaseIO Dynamic) : IO Dynamic := do
-- the following code is inherently non-deterministic in number of heartbeats, reset them at the
-- end
let heartbeats ← IO.getNumHeartbeats
-- find `RealizationContext` for `forConst` in `importRealizationCtx?` or `localRealizationCtxMap`
let ctx ← if env.base.get env |>.const2ModIdx.contains forConst then
env.importRealizationCtx?.getDM <|
throw <| .userError s!"Environment.realizeConst: `realizedImportedConsts` is empty"
else
match env.localRealizationCtxMap.find? forConst with
| some ctx => pure ctx
| none =>
throw <| .userError s!"trying to realize `{TypeName.typeName α}` value but \
`enableRealizationsForConst` must be called for '{forConst}' first"
let prom ← IO.Promise.new
-- atomically check whether we are the first branch to realize `key`
let existingConsts? ← ctx.realizeMapRef.modifyGet fun m =>
-- Safety: `typeName α` should uniquely identify `PHashMap α (Task Dynamic)`; there are no other
-- accesses to `private realizeMapRef` outside this function.
let m' := match m.find? (TypeName.typeName α) with
| some m' => unsafe unsafeCast (β := PHashMap α (Task Dynamic)) m'
| none => {}
match m'[key] with
| some prom' => (some prom', m)
| none =>
let m' := m'.insert key prom.result!
let m := m.insert (TypeName.typeName α) (unsafe unsafeCast (β := NonScalar) m')
(none, m)
let res ← if let some t := existingConsts? then
pure t.get
else
-- safety: `RealizationContext` is private
let realizeEnv : Environment := unsafe unsafeCast ctx.env
let realizeEnv := { realizeEnv with
-- allow realizations to recursively realize other constants for `forConst`. Do note that
-- this allows for recursive realization of `α` itself, which will deadlock.
localRealizationCtxMap := realizeEnv.localRealizationCtxMap.insert forConst ctx
importRealizationCtx? := env.importRealizationCtx?
}
let res ← realize realizeEnv ctx.opts
prom.resolve res
pure res
IO.setNumHeartbeats heartbeats
return res
private structure RealizeConstKey where
constName : Name
deriving BEq, Hashable, TypeName
/-- Realization results, to be replayed onto other branches. -/
private structure RealizeConstResult where
newConsts : VisibilityMap (List AsyncConst)
replayKernel : Kernel.Environment → Except Kernel.Exception Kernel.Environment
dyn : Dynamic
deriving Nonempty, TypeName
/-- Plumbing function for `Lean.Meta.realizeConst`; see documentation there. -/
def realizeConst (env : Environment) (forConst : Name) (constName : Name)
(realize : Environment → Options → BaseIO (Environment × Dynamic)) :
IO (Environment × Task (Option Kernel.Exception) × Dynamic) := do
-- the following code is inherently non-deterministic in number of heartbeats, reset them at the
-- end
let heartbeats ← IO.getNumHeartbeats
if env.asyncCtx?.any (·.realizingStack.contains constName) then
throw <| IO.userError s!"Environment.realizeConst: cyclic realization of '{constName}'"
let mut env := env
-- find `RealizationContext` for `forConst` in `realizedImportedConsts?` or `realizedLocalConsts`
let ctx ← if env.base.get env |>.const2ModIdx.contains forConst then
env.realizedImportedConsts?.getDM <|
throw <| .userError s!"Environment.realizeConst: `realizedImportedConsts` is empty"
else
match env.realizedLocalConsts.find? forConst with
| some ctx => pure ctx
| none =>
throw <| .userError s!"trying to realize {constName} but `enableRealizationsForConst` must be called for '{forConst}' first"
let prom ← IO.Promise.new
-- ensure `prom` is not left unresolved from stray exceptions
BaseIO.toIO do
-- atomically check whether we are the first branch to realize `constName`
let existingConsts? ← ctx.constsRef.modifyGet fun m => match m.find? constName with
| some prom' => (some prom', m)
| none => (none, m.insert constName prom.result!)
let res ← if let some existingConsts := existingConsts? then
pure existingConsts.get
else
-- safety: `RealizationContext` is private
let realizeEnv : Environment := unsafe unsafeCast ctx.env
let realizeEnv := { realizeEnv with
-- allow realizations to recursively realize other constants for `forConst`. Do note that
-- this allows for recursive realization of `constName` itself, which will deadlock.
realizedLocalConsts := realizeEnv.realizedLocalConsts.insert forConst ctx
realizedImportedConsts? := env.realizedImportedConsts?
}
-- ensure that environment extension modifications know they are in an async context
let realizeEnv := realizeEnv.enterAsyncRealizing constName
-- skip kernel in `realize`, we'll re-typecheck anyway
let realizeOpts := debug.skipKernelTC.set ctx.opts true
let (realizeEnv', dyn) ← realize realizeEnv realizeOpts
-- We could check that `c` was indeed added here but in practice `realize` has already
-- reported an error so we don't.
let res ← env.realizeValue forConst { constName : RealizeConstKey } fun realizeEnv realizeOpts => do
-- ensure that environment extension modifications know they are in an async context
let realizeEnv := realizeEnv.enterAsyncRealizing constName
-- skip kernel in `realize`, we'll re-typecheck anyway
let realizeOpts := debug.skipKernelTC.set realizeOpts true
let (realizeEnv', dyn) ← realize realizeEnv realizeOpts
-- We could check that `c` was indeed added here but in practice `realize` has already
-- reported an error so we don't.
-- find new constants incl. nested realizations, add current extension state, and compute
-- closure
let numNewPrivateConsts := realizeEnv'.asyncConstsMap.private.size - realizeEnv.asyncConstsMap.private.size
let newPrivateConsts := realizeEnv'.asyncConstsMap.private.revList.take numNewPrivateConsts |>.reverse
let newPrivateConsts := newPrivateConsts.map fun c =>
let c := { c with isRealized := true }
if c.exts?.isNone then
{ c with exts? := some <| .pure realizeEnv'.base.private.extensions }
else c
let numNewPublicConsts := realizeEnv'.asyncConstsMap.public.size - realizeEnv.asyncConstsMap.public.size
let newPublicConsts := realizeEnv'.asyncConstsMap.public.revList.take numNewPublicConsts |>.reverse
let newPublicConsts := newPublicConsts.map fun c =>
let c := { c with isRealized := true }
if c.exts?.isNone then
{ 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
let res := { newConsts.private := newPrivateConsts, newConsts.public := newPublicConsts, replayKernel, dyn }
prom.resolve res
pure res
let exPromise ← IO.Promise.new
let env := { env with
asyncConstsMap := {
«private» := res.newConsts.private.foldl (init := env.asyncConstsMap.private) fun consts c =>
if consts.find? c.constInfo.name |>.isSome then
consts
else
consts.add c
«public» := res.newConsts.public.foldl (init := env.asyncConstsMap.public) fun consts c =>
if consts.find? c.constInfo.name |>.isSome then
consts
else
consts.add c
}
checked := (← BaseIO.mapTask (t := env.checked) fun kenv => do
match res.replayKernel kenv with
| .ok kenv => return kenv
| .error e =>
exPromise.resolve e
return kenv)
allRealizations := env.allRealizations.map (sync := true) fun allRealizations =>
res.newConsts.private.foldl (init := allRealizations) fun allRealizations c =>
allRealizations.insert c.constInfo.name c
-- find new constants incl. nested realizations, add current extension state, and compute
-- closure
let numNewPrivateConsts := realizeEnv'.asyncConstsMap.private.size - realizeEnv.asyncConstsMap.private.size
let newPrivateConsts := realizeEnv'.asyncConstsMap.private.revList.take numNewPrivateConsts |>.reverse
let newPrivateConsts := newPrivateConsts.map fun c =>
let c := { c with isRealized := true }
if c.exts?.isNone then
{ c with exts? := some <| .pure realizeEnv'.base.private.extensions }
else c
let numNewPublicConsts := realizeEnv'.asyncConstsMap.public.size - realizeEnv.asyncConstsMap.public.size
let newPublicConsts := realizeEnv'.asyncConstsMap.public.revList.take numNewPublicConsts |>.reverse
let newPublicConsts := newPublicConsts.map fun c =>
let c := { c with isRealized := true }
if c.exts?.isNone then
{ 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
let res : RealizeConstResult := { newConsts.private := newPrivateConsts, newConsts.public := newPublicConsts, replayKernel, dyn }
pure (.mk res)
let some res := res.get? RealizeConstResult | unreachable!
let exPromise ← IO.Promise.new
let env := { env with
asyncConstsMap := {
«private» := res.newConsts.private.foldl (init := env.asyncConstsMap.private) fun consts c =>
if consts.find? c.constInfo.name |>.isSome then
consts
else
consts.add c
«public» := res.newConsts.public.foldl (init := env.asyncConstsMap.public) fun consts c =>
if consts.find? c.constInfo.name |>.isSome then
consts
else
consts.add c
}
IO.setNumHeartbeats heartbeats
return (env, exPromise.result?, res.dyn)
checked := (← BaseIO.mapTask (t := env.checked) fun kenv => do
match res.replayKernel kenv with
| .ok kenv => return kenv
| .error e =>
exPromise.resolve e
return kenv)
allRealizations := env.allRealizations.map (sync := true) fun allRealizations =>
res.newConsts.private.foldl (init := allRealizations) fun allRealizations c =>
allRealizations.insert c.constInfo.name c
}
return (env, exPromise.result?, res.dyn)
end Environment

98
src/Lean/Meta/Basic.lean
View file

@ -295,6 +295,7 @@ structure FunInfo where
That is, the (0-indexed) position of parameters that the result type depends on.
-/
resultDeps : Array Nat := #[]
deriving TypeName
/--
Key for the function information cache.
@ -2469,8 +2470,86 @@ private partial def setAllDiagRanges (snap : Language.SnapshotTree) (pos endPos
open Language
private structure RealizeValueResult where
res? : Except Exception Dynamic
snap? : Option SnapshotTree
deriving TypeName
/--
Realizes and caches a value for a given key with all environment objects derived from calling
`enableRealizationsForConst forConst` (fails if not called yet). If
this is the first environment branch passing the specific `key`, `realize` is called with the
environment and options at the time of calling `enableRealizationsForConst` if `forConst` is from
the current module and the state just after importing otherwise, thus helping achieve deterministic
results despite the non-deterministic choice of which thread is tasked with realization. In other
words, the result of `realizeValue` is *as if* `realize` had been called immediately after
`enableRealizationsForConst forConst`, with most effects but the return value discarded (see below).
Whether two calls of `realizeValue` with different `forConst`s but the same `key` share the result
is undefined; in practice, the key should usually uniquely determine `forConst` by e.g. including it
as a field.
`realizeValue` cannot check what other data is captured in the `realize` closure,
so it is best practice to extract it into a separate function and pass only arguments uniquely
determined by `key`. Traces, diagnostics, and raw std stream
output of `realize` are reported at all callers via `Core.logSnapshotTask` (so that the location of
generated diagnostics is deterministic). Note that, as `realize` is run using the options at
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.
-/
def realizeValue [BEq α] [Hashable α] [TypeName α] [TypeName β] (forConst : Name) (key : α) (realize : MetaM β) :
MetaM β := do
let env ← getEnv
if !env.areRealizationsEnabledForConst forConst then
return (← realize)
let coreCtx ← readThe Core.Context
let coreCtx := {
-- these fields should be invariant throughout the file
fileName := coreCtx.fileName, fileMap := coreCtx.fileMap
-- heartbeat limits inside `realizeAndReport` should be measured from this point on
initHeartbeats := (← IO.getNumHeartbeats)
}
let res ← env.realizeValue forConst key (realizeAndReport coreCtx)
let some res := res.get? RealizeValueResult | unreachable!
if let some snap := res.snap? then
let mut snap := snap
-- localize diagnostics
if let some range := (← getRef).getRange? then
let fileMap ← getFileMap
snap ← setAllDiagRanges snap (fileMap.toPosition range.start) (fileMap.toPosition range.stop)
Core.logSnapshotTask <| .finished (stx? := none) snap
match res.res? with
| .ok dyn => dyn.get? β |>.getDM (unreachable!)
| .error e => throw e
where
-- similar to `wrapAsyncAsSnapshot` but not sufficiently so to share code
realizeAndReport (coreCtx : Core.Context) env opts := do
let coreCtx := { coreCtx with options := opts }
let act :=
IO.FS.withIsolatedStreams (isolateStderr := Core.stderrAsMessages.get opts) (do
-- catch all exceptions
let _ : MonadExceptOf _ MetaM := MonadAlwaysExcept.except
observing do
realize)
<* addTraceAsMessages
let res? ← act |>.run' |>.run coreCtx { env } |>.toBaseIO
let res ← match res? with
| .ok ((output, err?), st) => pure {
snap? := (← Core.mkSnapshot? output coreCtx st)
res? := err?.map (.mk)
: RealizeValueResult
}
| _ =>
let _ : Inhabited RealizeValueResult := ⟨{
snap? := (← Core.mkSnapshot? "" coreCtx { env })
res? := default
: RealizeValueResult
}⟩
unreachable!
return .mk (α := RealizeValueResult) res
private structure RealizeConstantResult where
snap : SnapshotTree
snap? : Option SnapshotTree
error? : Option Exception
deriving TypeName
@ -2527,12 +2606,13 @@ def realizeConst (forConst : Name) (constName : Name) (realize : MetaM Unit) :
cancelTk? := none
}
if let some res := dyn.get? RealizeConstantResult then
let mut snap := res.snap
-- localize diagnostics
if let some range := (← getRef).getRange? then
let fileMap ← getFileMap
snap ← setAllDiagRanges snap (fileMap.toPosition range.start) (fileMap.toPosition range.stop)
Core.logSnapshotTask <| .finished (stx? := none) snap
if let some snap := res.snap? then
let mut snap := snap
-- localize diagnostics
if let some range := (← getRef).getRange? then
let fileMap ← getFileMap
snap ← setAllDiagRanges snap (fileMap.toPosition range.start) (fileMap.toPosition range.stop)
Core.logSnapshotTask <| .finished (stx? := none) snap
if let some e := res.error? then
throw e
setEnv env
@ -2555,7 +2635,7 @@ where
let res? ← act |>.run' |>.run coreCtx { env } |>.toBaseIO
match res? with
| .ok ((output, err?), st) => pure (st.env, .mk {
snap := (← Core.mkSnapshot output coreCtx st)
snap? := (← Core.mkSnapshot? output coreCtx st)
error? := match err? with
| .ok () => none
| .error e => some e
@ -2563,7 +2643,7 @@ where
})
| _ =>
let _ : Inhabited (Environment × Dynamic) := ⟨env, .mk {
snap := (← Core.mkSnapshot "" coreCtx { env })
snap? := (← Core.mkSnapshot? "" coreCtx { env })
error? := none
: RealizeConstantResult
}⟩