From 42e472ff3fa7d6669c25b4c407cbb715ac38d8eb Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 6 Aug 2025 13:24:11 +0200
Subject: [PATCH] refactor: simplify `AddConstAsyncResult.commitCheckEnv` use
 (#9715)

Also gets rid of some artifical `blocked (untracked)` time
---
 src/Lean/Elab/MutualDef.lean |  9 ++-------
 src/Lean/Environment.lean    | 11 ++++++-----
 2 files changed, 8 insertions(+), 12 deletions(-)

diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 13516d0d16..8d971f11c2 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -1236,13 +1236,8 @@ where
         let ctx ← CommandContextInfo.save
         infoPromise.resolve <| .context (.commandCtx ctx) <| .node info (← getInfoTrees)
       async.commitConst (← getEnv)
-      let cancelTk ← IO.CancelToken.new
-      let checkAct ← wrapAsyncAsSnapshot (desc := s!"finishing proof of {declId.declName}")
-          (cancelTk? := cancelTk) fun _ => do profileitM Exception "elaboration" (← getOptions) do
-        processDeriving #[header]
-        async.commitCheckEnv (← getEnv)
-      let checkTask ← BaseIO.mapTask (t := (← getEnv).checked) checkAct
-      Core.logSnapshotTask { stx? := none, task := checkTask, cancelTk? := cancelTk }
+      processDeriving #[header]
+      async.commitCheckEnv (← getEnv)
     Core.logSnapshotTask { stx? := none, task := (← BaseIO.asTask (act ())), cancelTk? := cancelTk }
     applyAttributesAt declId.declName view.modifiers.attrs .afterTypeChecking
     applyAttributesAt declId.declName view.modifiers.attrs .afterCompilation
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 221639fb8a..5e6028d8c2 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -1123,9 +1123,9 @@ def AddConstAsyncResult.commitConst (res : AddConstAsyncResult) (env : Environme
 
 /--
 Assuming `Lean.addDecl` has been run for the constant to be added on the async environment branch,
-commits the full constant info from that call to the main environment, waits for the final kernel
-environment resulting from the `addDecl` call, and commits it to the main branch as well, unblocking
-kernel additions there. All `commitConst` preconditions apply.
+commits the full constant info from that call to the main environment, (asynchronously) waits for
+the final kernel environment resulting from the `addDecl` call, and commits it to the main branch as
+well, unblocking kernel additions there. All `commitConst` preconditions apply.
 -/
 def AddConstAsyncResult.commitCheckEnv (res : AddConstAsyncResult) (env : Environment) :
     IO Unit := do
@@ -1133,8 +1133,9 @@ def AddConstAsyncResult.commitCheckEnv (res : AddConstAsyncResult) (env : Enviro
   -- `info?`
   if !(← res.constPromise.isResolved) then
     res.commitConst env
-  res.checkedEnvPromise.resolve env.checked.get
-  res.allRealizationsPromise.resolve env.allRealizations.get
+  BaseIO.chainTask (sync := true) env.checked fun checked => do
+    res.checkedEnvPromise.resolve checked
+    BaseIO.chainTask (sync := true) env.allRealizations res.allRealizationsPromise.resolve
 
 /--
 Checks whether `findAsync?` would return a result.