diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 293b8ab4c2..914a0e6ad3 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -423,7 +423,11 @@ def wrapAsyncAsSnapshot (act : Unit → CoreM Unit) (desc : String := by exact d IO.FS.withIsolatedStreams (isolateStderr := stderrAsMessages.get (← getOptions)) do let tid ← IO.getTID -- reset trace state and message log so as not to report them twice - modify fun st => { st with messages := st.messages.markAllReported, traceState := { tid } } + modify fun st => { st with + messages := st.messages.markAllReported + traceState := { tid } + snapshotTasks := #[] + } try withTraceNode `Elab.async (fun _ => return desc) do act () diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 4ed5181437..54fcc53651 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -313,7 +313,11 @@ def wrapAsyncAsSnapshot (act : Unit → CommandElabM Unit) IO.FS.withIsolatedStreams (isolateStderr := Core.stderrAsMessages.get (← getOptions)) do let tid ← IO.getTID -- reset trace state and message log so as not to report them twice - modify fun st => { st with messages := st.messages.markAllReported, traceState := { tid } } + modify fun st => { st with + messages := st.messages.markAllReported + traceState := { tid } + snapshotTasks := #[] + } try withTraceNode `Elab.async (fun _ => return desc) do act ()