From d26dbe73d554f720fa9dce48780b657a64107e2d Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 14 Nov 2024 10:36:48 +0100
Subject: [PATCH] fix: do not double-report `snapshotTasks` after
 `wrapAsyncAsSnapshot`

---
 src/Lean/CoreM.lean        | 6 +++++-
 src/Lean/Elab/Command.lean | 6 +++++-
 2 files changed, 10 insertions(+), 2 deletions(-)

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 ()