diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean
index 8f29ee4d5c..a15d6a0c43 100644
--- a/src/Lean/Elab/Frontend.lean
+++ b/src/Lean/Elab/Frontend.lean
@@ -81,10 +81,6 @@ end Frontend
 
 open Frontend
 
-def IO.processCommands (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState) (commandState : Command.State) : IO State := do
-  let (_, s) ← (Frontend.processCommands.run { inputCtx := inputCtx }).run { commandState := commandState, parserState := parserState, cmdPos := parserState.pos }
-  pure s
-
 structure IncrementalState extends State where
   inputCtx    : Parser.InputContext
   initialSnap : Language.Lean.CommandParsedSnapshot
@@ -92,12 +88,10 @@ deriving Nonempty
 
 open Language in
 /--
-Variant of `IO.processCommands` that uses the new Lean language processor implementation for
-potential incremental reuse. Pass in result of a previous invocation done with the same state
-(but usually different input context) to allow for reuse.
+Variant of `IO.processCommands` that allows for potential incremental reuse. Pass in the result of a
+previous invocation done with the same state (but usually different input context) to allow for
+reuse.
 -/
--- `IO.processCommands` can be reimplemented on top of this as soon as the additional tasks speed up
--- things instead of slowing them down
 partial def IO.processCommandsIncrementally (inputCtx : Parser.InputContext)
     (parserState : Parser.ModuleParserState) (commandState : Command.State)
     (old? : Option IncrementalState) :
@@ -110,7 +104,7 @@ where
     let snap := t.get
     let commands := commands.push snap.data.stx
     if let some next := snap.nextCmdSnap? then
-      go initialSnap next commands
+      go initialSnap next.task commands
     else
       -- Opting into reuse also enables incremental reporting, so make sure to collect messages from
       -- all snapshots
@@ -126,53 +120,17 @@ where
         inputCtx, initialSnap, commands
       }
 
+def IO.processCommands (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState)
+    (commandState : Command.State) : IO State := do
+  let st ← IO.processCommandsIncrementally inputCtx parserState commandState none
+  return st.toState
+
 def process (input : String) (env : Environment) (opts : Options) (fileName : Option String := none) : IO (Environment × MessageLog) := do
   let fileName   := fileName.getD "<input>"
   let inputCtx   := Parser.mkInputContext input fileName
   let s ← IO.processCommands inputCtx { : Parser.ModuleParserState } (Command.mkState env {} opts)
   pure (s.commandState.env, s.commandState.messages)
 
-/--
-Parses values of options registered during import and left by the C++ frontend as strings, fails if
-any option names remain unknown.
--/
-def reparseOptions (opts : Options) : IO Options := do
-  let mut opts := opts
-  let decls ← getOptionDecls
-  for (name, val) in opts do
-    let .ofString val := val
-      | continue  -- Already parsed by C++
-    -- Options can be prefixed with `weak` in order to turn off the error when the option is not
-    -- defined
-    let weak := name.getRoot == `weak
-    if weak then
-      opts := opts.erase name
-    let name := name.replacePrefix `weak Name.anonymous
-    let some decl := decls.find? name
-      | unless weak do
-          throw <| .userError s!"invalid -D parameter, unknown configuration option '{name}'
-          
-If the option is defined in this library, use '-D{`weak ++ name}' to set it conditionally"
-
-    match decl.defValue with
-    | .ofBool _ =>
-      match val with
-      | "true"  => opts := opts.insert name true
-      | "false" => opts := opts.insert name false
-      | _ =>
-        throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
-          it must be true/false"
-    | .ofNat _ =>
-      let some val := val.toNat?
-        | throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
-            it must be a natural number"
-      opts := opts.insert name val
-    | .ofString _ => opts := opts.insert name val
-    | _ => throw <| .userError s!"invalid -D parameter, configuration option '{name}' \
-              cannot be set in the command line, use set_option command"
-
-  return opts
-
 @[export lean_run_frontend]
 def runFrontend
     (input : String)
@@ -185,64 +143,31 @@ def runFrontend
     : IO (Environment × Bool) := do
   let startTime := (← IO.monoNanosNow).toFloat / 1000000000
   let inputCtx := Parser.mkInputContext input fileName
-  if true then
-    -- Temporarily keep alive old cmdline driver for the Lean language so that we don't pay the
-    -- overhead of passing the environment between snapshots until we actually make good use of it
-    -- outside the server
-    let (header, parserState, messages) ← Parser.parseHeader inputCtx
-    -- allow `env` to be leaked, which would live until the end of the process anyway
-    let (env, messages) ← processHeader (leakEnv := true) header opts messages inputCtx trustLevel
-    -- now that imports have been loaded, check options again
-    let opts ← reparseOptions opts
-    let env := env.setMainModule mainModuleName
-    let mut commandState := Command.mkState env messages opts
-    let elabStartTime := (← IO.monoNanosNow).toFloat / 1000000000
-
-    if ileanFileName?.isSome then
-      -- Collect InfoTrees so we can later extract and export their info to the ilean file
-      commandState := { commandState with infoState.enabled := true }
-
-    let s ← IO.processCommands inputCtx parserState commandState
-    Language.reportMessages s.commandState.messages opts jsonOutput
-
-    if let some ileanFileName := ileanFileName? then
-      let trees := s.commandState.infoState.trees.toArray
-      let references ←
-        Lean.Server.findModuleRefs inputCtx.fileMap trees (localVars := false) |>.toLspModuleRefs
-      let ilean := { module := mainModuleName, references : Lean.Server.Ilean }
-      IO.FS.writeFile ileanFileName $ Json.compress $ toJson ilean
-
-    if let some out := trace.profiler.output.get? opts then
-      let traceState := s.commandState.traceState
-      -- importing does not happen in an elaboration monad, add now
-      let traceState := { traceState with
-        traces := #[{
-          ref := .missing,
-          msg := .trace { cls := `Import, startTime, stopTime := elabStartTime }
-            (.ofFormat "importing") #[]
-        }].toPArray' ++ traceState.traces
-      }
-      let profile ← Firefox.Profile.export mainModuleName.toString startTime traceState opts
-      IO.FS.writeFile ⟨out⟩ <| Json.compress <| toJson profile
-
-    return (s.commandState.env, !s.commandState.messages.hasErrors)
-
+  let opts := Language.Lean.internal.minimalSnapshots.set opts true
   let ctx := { inputCtx with }
   let processor := Language.Lean.process
   let snap ← processor (fun _ => pure <| .ok { mainModuleName, opts, trustLevel }) none ctx
   let snaps := Language.toSnapshotTree snap
   snaps.runAndReport opts jsonOutput
+
   if let some ileanFileName := ileanFileName? then
     let trees := snaps.getAll.concatMap (match ·.infoTree? with | some t => #[t] | _ => #[])
     let references := Lean.Server.findModuleRefs inputCtx.fileMap trees (localVars := false)
     let ilean := { module := mainModuleName, references := ← references.toLspModuleRefs : Lean.Server.Ilean }
     IO.FS.writeFile ileanFileName $ Json.compress $ toJson ilean
 
-  let hasErrors := snaps.getAll.any (·.diagnostics.msgLog.hasErrors)
   -- TODO: remove default when reworking cmdline interface in Lean; currently the only case
   -- where we use the environment despite errors in the file is `--stats`
-  let env := Language.Lean.waitForFinalEnv? snap |>.getD (← mkEmptyEnvironment)
-  pure (env, !hasErrors)
+  let some cmdState := Language.Lean.waitForFinalCmdState? snap
+    | return (← mkEmptyEnvironment, false)
+
+  if let some out := trace.profiler.output.get? opts then
+    let traceState := cmdState.traceState
+    let profile ← Firefox.Profile.export mainModuleName.toString startTime traceState opts
+    IO.FS.writeFile ⟨out⟩ <| Json.compress <| toJson profile
+
+  let hasErrors := snaps.getAll.any (·.diagnostics.msgLog.hasErrors)
+  pure (cmdState.env, !hasErrors)
 
 
 end Lean.Elab
diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean
index 994f8dd098..78dc1ceefb 100644
--- a/src/Lean/Language/Lean.lean
+++ b/src/Lean/Language/Lean.lean
@@ -234,6 +234,54 @@ structure SetupImportsResult where
   /-- Kernel trust level. -/
   trustLevel : UInt32 := 0
 
+/-- Performance option used by cmdline driver. -/
+register_builtin_option internal.minimalSnapshots : Bool := {
+  defValue := false
+  descr    := "reduce information stored in snapshots to the minimum necessary for the cmdline \
+driver: diagnostics per command and final full snapshot"
+}
+
+/--
+Parses values of options registered during import and left by the C++ frontend as strings, fails if
+any option names remain unknown.
+-/
+def reparseOptions (opts : Options) : IO Options := do
+  let mut opts := opts
+  let decls ← getOptionDecls
+  for (name, val) in opts do
+    let .ofString val := val
+      | continue  -- Already parsed by C++
+    -- Options can be prefixed with `weak` in order to turn off the error when the option is not
+    -- defined
+    let weak := name.getRoot == `weak
+    if weak then
+      opts := opts.erase name
+    let name := name.replacePrefix `weak Name.anonymous
+    let some decl := decls.find? name
+      | unless weak do
+          throw <| .userError s!"invalid -D parameter, unknown configuration option '{name}'
+
+If the option is defined in this library, use '-D{`weak ++ name}' to set it conditionally"
+
+    match decl.defValue with
+    | .ofBool _ =>
+      match val with
+      | "true"  => opts := opts.insert name true
+      | "false" => opts := opts.insert name false
+      | _ =>
+        throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
+          it must be true/false"
+    | .ofNat _ =>
+      let some val := val.toNat?
+        | throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
+            it must be a natural number"
+      opts := opts.insert name val
+    | .ofString _ => opts := opts.insert name val
+    | _ => throw <| .userError s!"invalid -D parameter, configuration option '{name}' \
+              cannot be set in the command line, use set_option command"
+
+  return opts
+
 /--
 Entry point of the Lean language processor.
 
@@ -279,9 +327,11 @@ where
               if let some oldProcSuccess := oldProcessed.result? then
                 -- also wait on old command parse snapshot as parsing is cheap and may allow for
                 -- elaboration reuse
-                oldProcSuccess.firstCmdSnap.bindIO (sync := true) fun oldCmd =>
+                oldProcSuccess.firstCmdSnap.bindIO (sync := true) fun oldCmd => do
+                  let prom ← IO.Promise.new
+                  let _ ← IO.asTask (parseCmd oldCmd newParserState oldProcSuccess.cmdState oldProcSuccess.cmdState.env prom ctx)
                   return .pure { oldProcessed with result? := some { oldProcSuccess with
-                    firstCmdSnap := (← parseCmd oldCmd newParserState oldProcSuccess.cmdState ctx) } }
+                    firstCmdSnap := { range? := none, task := prom.result } } }
               else
                 return .pure oldProcessed) } }
       else return old
@@ -343,42 +393,68 @@ where
       let setup ← match (← setupImports stx) with
         | .ok setup => pure setup
         | .error snap => return snap
+
+      let startTime := (← IO.monoNanosNow).toFloat / 1000000000
       -- allows `headerEnv` to be leaked, which would live until the end of the process anyway
       let (headerEnv, msgLog) ← Elab.processHeader (leakEnv := true) stx setup.opts .empty
         ctx.toInputContext setup.trustLevel
+      let stopTime := (← IO.monoNanosNow).toFloat / 1000000000
       let diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog)
       if msgLog.hasErrors then
         return { diagnostics, result? := none }
 
       let headerEnv := headerEnv.setMainModule setup.mainModuleName
-      let cmdState := Elab.Command.mkState headerEnv msgLog setup.opts
-      let cmdState := { cmdState with infoState := {
-        enabled := true
-        trees := #[Elab.InfoTree.context (.commandCtx {
-          env     := headerEnv
-          fileMap := ctx.fileMap
-          ngen    := { namePrefix := `_import }
-        }) (Elab.InfoTree.node
-            (Elab.Info.ofCommandInfo { elaborator := `header, stx })
-            (stx[1].getArgs.toList.map (fun importStx =>
-              Elab.InfoTree.node (Elab.Info.ofCommandInfo {
-                elaborator := `import
-                stx := importStx
-              }) #[].toPArray'
-            )).toPArray'
-        )].toPArray'
-      }}
+      let mut traceState := default
+      if trace.profiler.output.get? setup.opts |>.isSome then
+        traceState := {
+          traces := #[{
+            ref := .missing,
+            msg := .trace { cls := `Import, startTime, stopTime }
+              (.ofFormat "importing") #[]
+            : TraceElem
+          }].toPArray'
+        }
+      -- now that imports have been loaded, check options again
+      let opts ← reparseOptions setup.opts
+      let cmdState := Elab.Command.mkState headerEnv msgLog opts
+      let cmdState := { cmdState with
+        infoState := {
+          enabled := true
+          trees := #[Elab.InfoTree.context (.commandCtx {
+            env     := headerEnv
+            fileMap := ctx.fileMap
+            ngen    := { namePrefix := `_import }
+          }) (Elab.InfoTree.node
+              (Elab.Info.ofCommandInfo { elaborator := `header, stx })
+              (stx[1].getArgs.toList.map (fun importStx =>
+                Elab.InfoTree.node (Elab.Info.ofCommandInfo {
+                  elaborator := `import
+                  stx := importStx
+                }) #[].toPArray'
+              )).toPArray'
+          )].toPArray'
+        }
+        traceState
+      }
+      let prom ← IO.Promise.new
+      -- The speedup of these `markPersistent`s is negligible but they help in making unexpected
+      -- `inc_ref_cold`s more visible
+      let parserState := Runtime.markPersistent parserState
+      let cmdState := Runtime.markPersistent cmdState
+      let ctx := Runtime.markPersistent ctx
+      let _ ← IO.asTask (parseCmd none parserState cmdState cmdState.env prom ctx)
       return {
         diagnostics
         infoTree? := cmdState.infoState.trees[0]!
         result? := some {
           cmdState
-          firstCmdSnap := (← parseCmd none parserState cmdState)
+          firstCmdSnap := { range? := none, task := prom.result }
         }
       }
 
   parseCmd (old? : Option CommandParsedSnapshot) (parserState : Parser.ModuleParserState)
-      (cmdState : Command.State) : LeanProcessingM (SnapshotTask CommandParsedSnapshot) := do
+      (cmdState : Command.State) (initEnv : Environment) (prom : IO.Promise CommandParsedSnapshot) :
+      LeanProcessingM Unit := do
     let ctx ← read
 
     -- check for cancellation, most likely during elaboration of previous command, before starting
@@ -387,82 +463,100 @@ where
       -- this is a bit ugly as we don't want to adjust our API with `Option`s just for cancellation
       -- (as no-one should look at this result in that case) but anything containing `Environment`
       -- is not `Inhabited`
-      return .pure <| .mk (nextCmdSnap? := none) {
+      prom.resolve <| .mk (nextCmdSnap? := none) {
         diagnostics := .empty, stx := .missing, parserState
         elabSnap := .pure <| .ofTyped { diagnostics := .empty : SnapshotLeaf }
         finishedSnap := .pure { diagnostics := .empty, cmdState }
         tacticCache := (← IO.mkRef {})
       }
+      return
 
-    let unchanged old newParserState : BaseIO CommandParsedSnapshot :=
+    let unchanged old newParserState : BaseIO Unit :=
       -- when syntax is unchanged, reuse command processing task as is
       -- NOTE: even if the syntax tree is functionally unchanged, the new parser state may still
       -- have changed because of trailing whitespace and comments etc., so it is passed separately
       -- from `old`
-      if let some oldNext := old.nextCmdSnap? then
-        return .mk (data := old.data)
-          (nextCmdSnap? := (← old.data.finishedSnap.bindIO (sync := true) fun oldFinished =>
-            -- also wait on old command parse snapshot as parsing is cheap and may allow for
-            -- elaboration reuse
-            oldNext.bindIO (sync := true) fun oldNext => do
-              parseCmd oldNext newParserState oldFinished.cmdState ctx))
-      else return old  -- terminal command, we're done!
+      if let some oldNext := old.nextCmdSnap? then do
+        let newProm ← IO.Promise.new
+        let _ ← old.data.finishedSnap.bindIO fun oldFinished =>
+          -- also wait on old command parse snapshot as parsing is cheap and may allow for
+          -- elaboration reuse
+          oldNext.bindIO (sync := true) fun oldNext => do
+            parseCmd oldNext newParserState oldFinished.cmdState initEnv newProm ctx
+            return .pure ()
+        prom.resolve <| .mk (data := old.data) (nextCmdSnap? := some { range? := none, task := newProm.result })
+      else prom.resolve old  -- terminal command, we're done!
 
     -- fast path, do not even start new task for this snapshot
     if let some old := old? then
       if let some nextCom ← old.nextCmdSnap?.bindM (·.get?) then
         if (← isBeforeEditPos nextCom.data.parserState.pos) then
-          return .pure (← unchanged old old.data.parserState)
+          return (← unchanged old old.data.parserState)
 
-    SnapshotTask.ofIO (some ⟨parserState.pos, ctx.input.endPos⟩) do
-      let beginPos := parserState.pos
-      let scope := cmdState.scopes.head!
-      let pmctx := {
-        env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace
-        openDecls := scope.openDecls
-      }
-      let (stx, parserState, msgLog) := Parser.parseCommand ctx.toInputContext pmctx parserState
-        .empty
+    let beginPos := parserState.pos
+    let scope := cmdState.scopes.head!
+    let pmctx := {
+      env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace
+      openDecls := scope.openDecls
+    }
+    let (stx, parserState, msgLog) :=
+      profileit "parsing" scope.opts fun _ =>
+        Parser.parseCommand ctx.toInputContext pmctx parserState .empty
 
-      -- semi-fast path
-      if let some old := old? then
-        -- NOTE: as `parserState.pos` includes trailing whitespace, this forces reprocessing even if
-        -- only that whitespace changes, which is wasteful but still necessary because it may
-        -- influence the range of error messages such as from a trailing `exact`
-        if stx.eqWithInfo old.data.stx then
-          -- Here we must make sure to pass the *new* parser state; see NOTE in `unchanged`
-          return (← unchanged old parserState)
-        -- on first change, make sure to cancel old invocation
-        -- TODO: pass token into incrementality-aware elaborators to improve reuse of still-valid,
-        -- still-running elaboration steps?
-        if let some tk := ctx.oldCancelTk? then
-          tk.set
+    -- semi-fast path
+    if let some old := old? then
+      -- NOTE: as `parserState.pos` includes trailing whitespace, this forces reprocessing even if
+      -- only that whitespace changes, which is wasteful but still necessary because it may
+      -- influence the range of error messages such as from a trailing `exact`
+      if stx.eqWithInfo old.data.stx then
+        -- Here we must make sure to pass the *new* parser state; see NOTE in `unchanged`
+        return (← unchanged old parserState)
+      -- on first change, make sure to cancel old invocation
+      -- TODO: pass token into incrementality-aware elaborators to improve reuse of still-valid,
+      -- still-running elaboration steps?
+      if let some tk := ctx.oldCancelTk? then
+        tk.set
 
-      -- definitely resolved in `doElab` task
-      let elabPromise ← IO.Promise.new
-      let tacticCache ← old?.map (·.data.tacticCache) |>.getDM (IO.mkRef {})
-      let finishedSnap ←
-        doElab stx cmdState beginPos
-          { old? := old?.map fun old => ⟨old.data.stx, old.data.elabSnap⟩, new := elabPromise }
-          tacticCache
-          ctx
-
-      let next? ← if Parser.isTerminalCommand stx then pure none
-        -- for now, wait on "command finished" snapshot before parsing next command
-        else some <$> finishedSnap.bindIO fun finished =>
-          parseCmd none parserState finished.cmdState ctx
-      return .mk (nextCmdSnap? := next?) {
-        diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog)
-        stx
-        parserState
-        elabSnap := { range? := stx.getRange?, task := elabPromise.result }
-        finishedSnap
+    -- definitely resolved in `doElab` task
+    let elabPromise ← IO.Promise.new
+    let tacticCache ← old?.map (·.data.tacticCache) |>.getDM (IO.mkRef {})
+    let finishedSnap ←
+      doElab stx cmdState beginPos
+        { old? := old?.map fun old => ⟨old.data.stx, old.data.elabSnap⟩, new := elabPromise }
         tacticCache
+        ctx
+
+    let minimalSnapshots := internal.minimalSnapshots.get cmdState.scopes.head!.opts
+    let next? ← if Parser.isTerminalCommand stx then pure none
+      -- for now, wait on "command finished" snapshot before parsing next command
+      else some <$> IO.Promise.new
+    let diagnostics ← Snapshot.Diagnostics.ofMessageLog msgLog
+    let data := if minimalSnapshots && !Parser.isTerminalCommand stx then {
+      diagnostics
+      stx := .missing
+      parserState := {}
+      elabSnap := { range? := stx.getRange?, task := elabPromise.result }
+      finishedSnap := .pure {
+        diagnostics := finishedSnap.diagnostics
+        infoTree? := none
+        cmdState := {
+          env := initEnv
+          maxRecDepth := 0
+        }
       }
+      tacticCache
+    } else {
+      diagnostics, stx, parserState, tacticCache
+      elabSnap := { range? := stx.getRange?, task := elabPromise.result }
+      finishedSnap := .pure finishedSnap
+    }
+    prom.resolve <| .mk (nextCmdSnap? := next?.map ({ range? := some ⟨parserState.pos, ctx.input.endPos⟩, task := ·.result })) data
+    if let some next := next? then
+      parseCmd none parserState finishedSnap.cmdState initEnv next ctx
 
   doElab (stx : Syntax) (cmdState : Command.State) (beginPos : String.Pos)
       (snap : SnapshotBundle DynamicSnapshot) (tacticCache : IO.Ref Tactic.Cache) :
-      LeanProcessingM (SnapshotTask CommandFinishedSnapshot) := do
+      LeanProcessingM CommandFinishedSnapshot := do
     let ctx ← read
     -- (Try to) use last line of command as range for final snapshot task. This ensures we do not
     -- retract the progress bar to a previous position in case the command support incremental
@@ -471,48 +565,46 @@ where
     -- `parseCmd` and containing the entire range of the command will determine the reported
     -- progress and be resolved effectively at the same time as this snapshot task, so `tailPos` is
     -- irrelevant in this case.
-    let tailPos := stx.getTailPos? |>.getD beginPos
-    SnapshotTask.ofIO (some ⟨tailPos, tailPos⟩) do
-      let scope := cmdState.scopes.head!
-      let cmdStateRef ← IO.mkRef { cmdState with messages := .empty }
-      /-
-      The same snapshot may be executed by different tasks. So, to make sure `elabCommandTopLevel`
-      has exclusive access to the cache, we create a fresh reference here. Before this change, the
-      following `tacticCache.modify` would reset the tactic post cache while another snapshot was
-      still using it.
-      -/
-      let tacticCacheNew ← IO.mkRef (← tacticCache.get)
-      let cmdCtx : Elab.Command.Context := { ctx with
-        cmdPos       := beginPos
-        tacticCache? := some tacticCacheNew
-        snap?        := some snap
-        cancelTk?    := some ctx.newCancelTk
-      }
-      let (output, _) ←
-        IO.FS.withIsolatedStreams (isolateStderr := stderrAsMessages.get scope.opts) do
-          liftM (m := BaseIO) do
-            withLoggingExceptions
-              (getResetInfoTrees *> Elab.Command.elabCommandTopLevel stx)
-              cmdCtx cmdStateRef
-      let postNew := (← tacticCacheNew.get).post
-      tacticCache.modify fun _ => { pre := postNew, post := {} }
-      let cmdState ← cmdStateRef.get
-      let mut messages := cmdState.messages
-      if !output.isEmpty then
-        messages := messages.add {
-          fileName := ctx.fileName
-          severity := MessageSeverity.information
-          pos      := ctx.fileMap.toPosition beginPos
-          data     := output
-        }
-      let cmdState := { cmdState with messages }
-      -- definitely resolve eventually
-      snap.new.resolve <| .ofTyped { diagnostics := .empty : SnapshotLeaf }
-      return {
-        diagnostics := (← Snapshot.Diagnostics.ofMessageLog cmdState.messages)
-        infoTree? := some cmdState.infoState.trees[0]!
-        cmdState
+    let scope := cmdState.scopes.head!
+    let cmdStateRef ← IO.mkRef { cmdState with messages := .empty }
+    /-
+    The same snapshot may be executed by different tasks. So, to make sure `elabCommandTopLevel`
+    has exclusive access to the cache, we create a fresh reference here. Before this change, the
+    following `tacticCache.modify` would reset the tactic post cache while another snapshot was
+    still using it.
+    -/
+    let tacticCacheNew ← IO.mkRef (← tacticCache.get)
+    let cmdCtx : Elab.Command.Context := { ctx with
+      cmdPos       := beginPos
+      tacticCache? := some tacticCacheNew
+      snap?        := if internal.minimalSnapshots.get scope.opts then none else snap
+      cancelTk?    := some ctx.newCancelTk
+    }
+    let (output, _) ←
+      IO.FS.withIsolatedStreams (isolateStderr := stderrAsMessages.get scope.opts) do
+        liftM (m := BaseIO) do
+          withLoggingExceptions
+            (getResetInfoTrees *> Elab.Command.elabCommandTopLevel stx)
+            cmdCtx cmdStateRef
+    let postNew := (← tacticCacheNew.get).post
+    tacticCache.modify fun _ => { pre := postNew, post := {} }
+    let cmdState ← cmdStateRef.get
+    let mut messages := cmdState.messages
+    if !output.isEmpty then
+      messages := messages.add {
+        fileName := ctx.fileName
+        severity := MessageSeverity.information
+        pos      := ctx.fileMap.toPosition beginPos
+        data     := output
       }
+    let cmdState := { cmdState with messages }
+    -- definitely resolve eventually
+    snap.new.resolve <| .ofTyped { diagnostics := .empty : SnapshotLeaf }
+    return {
+      diagnostics := (← Snapshot.Diagnostics.ofMessageLog cmdState.messages)
+      infoTree? := some cmdState.infoState.trees[0]!
+      cmdState
+    }
 
 /--
 Convenience function for tool uses of the language processor that skips header handling.
@@ -520,14 +612,15 @@ Convenience function for tool uses of the language processor that skips header h
 def processCommands (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState)
     (commandState : Command.State)
     (old? : Option (Parser.InputContext × CommandParsedSnapshot) := none) :
-    BaseIO (SnapshotTask CommandParsedSnapshot) := do
-  process.parseCmd (old?.map (·.2)) parserState commandState
+    BaseIO (Task CommandParsedSnapshot) := do
+  let prom ← IO.Promise.new
+  process.parseCmd (old?.map (·.2)) parserState commandState commandState.env prom
     |>.run (old?.map (·.1))
     |>.run { inputCtx with }
+  return prom.result
 
-
-/-- Waits for and returns final environment, if importing was successful. -/
-partial def waitForFinalEnv? (snap : InitialSnapshot) : Option Environment := do
+/-- Waits for and returns final command state, if importing was successful. -/
+partial def waitForFinalCmdState? (snap : InitialSnapshot) : Option Command.State := do
   let snap ← snap.result?
   let snap ← snap.processedSnap.get.result?
   goCmd snap.firstCmdSnap.get
@@ -535,6 +628,6 @@ where goCmd snap :=
   if let some next := snap.nextCmdSnap? then
     goCmd next.get
   else
-    snap.data.finishedSnap.get.cmdState.env
+    snap.data.finishedSnap.get.cmdState
 
 end Lean
diff --git a/tests/lean/2505.lean.expected.out b/tests/lean/2505.lean.expected.out
index 6610d40a35..98a7adec30 100644
--- a/tests/lean/2505.lean.expected.out
+++ b/tests/lean/2505.lean.expected.out
@@ -1,3 +1,3 @@
+2505.lean:14:0-14:7: warning: declaration uses 'sorry'
 target : A (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))
 target' : A (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))
-2505.lean:14:0-14:7: warning: declaration uses 'sorry'
diff --git a/tests/lean/4089.lean.expected.out b/tests/lean/4089.lean.expected.out
index 9152f7bfa4..18c8b0d2e9 100644
--- a/tests/lean/4089.lean.expected.out
+++ b/tests/lean/4089.lean.expected.out
@@ -8,6 +8,7 @@ def f (x_1 : obj) : obj :=
     let x_5 : obj := reset[2] x_1;
     let x_4 : obj := reuse x_5 in ctor_0[Prod.mk] x_3 x_2;
     ret x_4
+
 [reset_reuse]
 def Sigma.toProd._rarg (x_1 : obj) : obj :=
   case x_1 : obj of
@@ -20,6 +21,7 @@ def Sigma.toProd._rarg (x_1 : obj) : obj :=
 def Sigma.toProd (x_1 : ◾) (x_2 : ◾) : obj :=
   let x_3 : obj := pap Sigma.toProd._rarg;
   ret x_3
+
 [reset_reuse]
 def foo (x_1 : obj) : obj :=
   case x_1 : obj of
@@ -35,4 +37,4 @@ def foo (x_1 : obj) : obj :=
       let x_5 : obj := proj[0] x_3;
       let x_6 : obj := foo x_4;
       let x_7 : obj := reuse x_9 in ctor_1[List.cons] x_5 x_6;
-      ret x_7
\ No newline at end of file
+      ret x_7
diff --git a/tests/lean/4240.lean.expected.out b/tests/lean/4240.lean.expected.out
index 174456c8f3..30636e3d30 100644
--- a/tests/lean/4240.lean.expected.out
+++ b/tests/lean/4240.lean.expected.out
@@ -23,4 +23,4 @@ def isSomeWithInstanceNat._boxed (x_1 : obj) : obj :=
   let x_2 : u8 := isSomeWithInstanceNat x_1;
   dec x_1;
   let x_3 : obj := box x_2;
-  ret x_3
\ No newline at end of file
+  ret x_3
diff --git a/tests/lean/Process.lean.expected.out b/tests/lean/Process.lean.expected.out
index 600e4f2544..5d186fa1f4 100644
--- a/tests/lean/Process.lean.expected.out
+++ b/tests/lean/Process.lean.expected.out
@@ -1,6 +1,5 @@
-hi!
-<stdin>:1:0: warning: using 'exit' to interrupt Lean
 1
+hi!
 0
 "ho!\n"
 "hu!\n"
@@ -9,6 +8,7 @@ flush of broken pipe failed
 100000
 0
 0
+<stdin>:1:0: warning: using 'exit' to interrupt Lean
 0
 0
 none
diff --git a/tests/lean/computedFieldsCode.lean.expected.out b/tests/lean/computedFieldsCode.lean.expected.out
index 10f711f905..4c2e4c9e17 100644
--- a/tests/lean/computedFieldsCode.lean.expected.out
+++ b/tests/lean/computedFieldsCode.lean.expected.out
@@ -106,6 +106,7 @@ def Exp.hash._override._boxed (x_1 : obj) : obj :=
   dec x_1;
   let x_3 : obj := box x_2;
   ret x_3
+
 [result]
 def f._closed_1 : obj :=
   let x_1 : u32 := 10;
@@ -124,6 +125,7 @@ def f._closed_3 : u64 :=
 def f : u64 :=
   let x_1 : u64 := f._closed_3;
   ret x_1
+
 [result]
 def g (x_1 : @& obj) : u8 :=
   case x_1 : obj of
@@ -138,6 +140,7 @@ def g._boxed (x_1 : obj) : obj :=
   dec x_1;
   let x_3 : obj := box x_2;
   ret x_3
+
 [result]
 def hash' (x_1 : @& obj) : obj :=
   case x_1 : obj of
@@ -161,6 +164,7 @@ def hash'._boxed (x_1 : obj) : obj :=
   let x_2 : obj := hash' x_1;
   dec x_1;
   ret x_2
+
 [result]
 def getAppFn (x_1 : @& obj) : obj :=
   case x_1 : obj of
@@ -175,6 +179,7 @@ def getAppFn._boxed (x_1 : obj) : obj :=
   let x_2 : obj := getAppFn x_1;
   dec x_1;
   ret x_2
+
 [result]
 def Exp.f (x_1 : @& obj) : obj :=
   let x_2 : obj := getAppFn x_1;
@@ -182,4 +187,4 @@ def Exp.f (x_1 : @& obj) : obj :=
 def Exp.f._boxed (x_1 : obj) : obj :=
   let x_2 : obj := Exp.f x_1;
   dec x_1;
-  ret x_2
\ No newline at end of file
+  ret x_2
diff --git a/tests/lean/csimpAttr.lean.expected.out b/tests/lean/csimpAttr.lean.expected.out
index d69d1215be..a491585b8c 100644
--- a/tests/lean/csimpAttr.lean.expected.out
+++ b/tests/lean/csimpAttr.lean.expected.out
@@ -1,6 +1,7 @@
+csimpAttr.lean:7:2-7:7: error: invalid 'csimp' theorem, only constant replacement theorems (e.g., `@f = @g`) are currently supported.
 
 [init]
 def f (x_1 : obj) : obj :=
   let x_2 : obj := Nat.add x_1 x_1;
   let x_3 : obj := Nat.add x_2 x_2;
-  ret x_3csimpAttr.lean:7:2-7:7: error: invalid 'csimp' theorem, only constant replacement theorems (e.g., `@f = @g`) are currently supported.
+  ret x_3
diff --git a/tests/lean/csimpAttrAppend.lean.expected.out b/tests/lean/csimpAttrAppend.lean.expected.out
index 0b72623159..2e7eac5952 100644
--- a/tests/lean/csimpAttrAppend.lean.expected.out
+++ b/tests/lean/csimpAttrAppend.lean.expected.out
@@ -3,4 +3,4 @@
 def f (x_1 : obj) (x_2 : obj) (x_3 : obj) : obj :=
   let x_4 : obj := List.appendTR._rarg x_1 x_2;
   let x_5 : obj := List.appendTR._rarg x_4 x_3;
-  ret x_5
\ No newline at end of file
+  ret x_5
diff --git a/tests/lean/dbgMacros.lean.expected.out b/tests/lean/dbgMacros.lean.expected.out
index 9b70d1b860..54d6f8756c 100644
--- a/tests/lean/dbgMacros.lean.expected.out
+++ b/tests/lean/dbgMacros.lean.expected.out
@@ -1,10 +1,10 @@
 PANIC at f dbgMacros:2:14: unexpected zero
-PANIC at g dbgMacros:10:14: unreachable code has been reached
-PANIC at h dbgMacros:16:0: assertion violation: x != 0
 0
 9
+PANIC at g dbgMacros:10:14: unreachable code has been reached
 0
 0
+PANIC at h dbgMacros:16:0: assertion violation: x != 0
 0
 f2, x: 10
 11
diff --git a/tests/lean/doubleReset.lean.expected.out b/tests/lean/doubleReset.lean.expected.out
index fce8062bf3..25937761cd 100644
--- a/tests/lean/doubleReset.lean.expected.out
+++ b/tests/lean/doubleReset.lean.expected.out
@@ -34,4 +34,4 @@ def applyProjectionRules._rarg (x_1 : obj) (x_2 : obj) : obj :=
   ret x_5
 def applyProjectionRules (x_1 : ◾) (x_2 : ◾) (x_3 : ◾) : obj :=
   let x_4 : obj := pap applyProjectionRules._rarg;
-  ret x_4
\ No newline at end of file
+  ret x_4
diff --git a/tests/lean/etaReducedMvarAssignments.lean.expected.out b/tests/lean/etaReducedMvarAssignments.lean.expected.out
index 7c743ec28e..b85fc4033b 100644
--- a/tests/lean/etaReducedMvarAssignments.lean.expected.out
+++ b/tests/lean/etaReducedMvarAssignments.lean.expected.out
@@ -1,4 +1,4 @@
-Pi.hasLe : LE ((i : ι) → α i)
-[Meta.isDefEq.assign] ✅ ?m i := α i
-  [Meta.isDefEq.assign.beforeMkLambda] ?m [i] := α i
-  [Meta.isDefEq.assign.checkTypes] ✅ (?m : ι → Type ?u) := (α : ι → Type v)
+Pi.hasLe : LE ((i : ι) → α i)
+[Meta.isDefEq.assign] ✅ ?m i := α i
+  [Meta.isDefEq.assign.beforeMkLambda] ?m [i] := α i
+  [Meta.isDefEq.assign.checkTypes] ✅ (?m : ι → Type ?u) := (α : ι → Type v)
diff --git a/tests/lean/listLength.lean.expected.out b/tests/lean/listLength.lean.expected.out
index 311ee817f5..ae2f89a73c 100644
--- a/tests/lean/listLength.lean.expected.out
+++ b/tests/lean/listLength.lean.expected.out
@@ -5,4 +5,4 @@ def f (x_1 : obj) : obj :=
   let x_3 : obj := List.lengthTRAux._rarg x_1 x_2;
   let x_4 : obj := 2;
   let x_5 : obj := Nat.mul x_4 x_3;
-  ret x_5
\ No newline at end of file
+  ret x_5
diff --git a/tests/lean/lit_values.lean.expected.out b/tests/lean/lit_values.lean.expected.out
index ee860cc74b..20056b7967 100644
--- a/tests/lean/lit_values.lean.expected.out
+++ b/tests/lean/lit_values.lean.expected.out
@@ -3,10 +3,10 @@
 (some 2)
 (some -2)
 (some a)
+some "hello"
 (some (⟨5, 3⟩))
 (some (⟨12, 0x003#12⟩))
 (some 2)
 (some 2)
 (some 2)
 (some 2)
-some "hello"
diff --git a/tests/lean/unboxStruct.lean.expected.out b/tests/lean/unboxStruct.lean.expected.out
index 8d0db228ff..feffd37563 100644
--- a/tests/lean/unboxStruct.lean.expected.out
+++ b/tests/lean/unboxStruct.lean.expected.out
@@ -7,4 +7,4 @@ def test2._boxed (x_1 : obj) (x_2 : obj) : obj :=
   let x_3 : u32 := unbox x_1;
   dec x_1;
   let x_4 : obj := test2 x_3 x_2;
-  ret x_4
\ No newline at end of file
+  ret x_4
diff --git a/tests/lean/updateExprIssue.lean.expected.out b/tests/lean/updateExprIssue.lean.expected.out
index 10537d1e32..5e550af5df 100644
--- a/tests/lean/updateExprIssue.lean.expected.out
+++ b/tests/lean/updateExprIssue.lean.expected.out
@@ -1,4 +1,5 @@
 
+
 [init]
 def sefFn (x_1 : obj) (x_2 : obj) : obj :=
   case x_1 : obj of