diff --git a/src/Init/Data/Range/Polymorphic/RangeIterator.lean b/src/Init/Data/Range/Polymorphic/RangeIterator.lean
index e10691d519..e35af70f6f 100644
--- a/src/Init/Data/Range/Polymorphic/RangeIterator.lean
+++ b/src/Init/Data/Range/Polymorphic/RangeIterator.lean
@@ -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
diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index 4ac1e27b78..6d9d459912 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -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
 
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 5e6028d8c2..9d2615fb11 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -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
 
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index f867a85214..ac5ba57ebc 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -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
       }⟩