From c33c2c5fbda59e2f52b3828461a3965d74a463e8 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 28 Mar 2025 10:39:58 +0100 Subject: [PATCH] fix: avoid deadlock in `logGoalsAccomplishedSnapshotTask` (#7705) Fixes #7684 --- src/Lean/Elab/MutualDef.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 5a80e0cac6..99734b7b21 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -1162,6 +1162,9 @@ private def logGoalsAccomplishedSnapshotTask (views : Array DefView) -- Skip 'goals accomplished' task if we are on the command line. -- These messages are only used in the language server. return + -- make sure we don't accidentally keep any nested promises alive that would otherwise + -- auto-resolve to `none` + let views := views.map fun view => (view.ref, view.kind) let currentLog ← Core.getMessageLog let snaps := #[SnapshotTask.finished none (toSnapshotTree defsParsedSnap)] ++ (← getThe Core.State).snapshotTasks @@ -1174,11 +1177,11 @@ private def logGoalsAccomplishedSnapshotTask (views : Array DefView) msg.severity matches .error || msg.data.hasTag (· == `hasSorry) if hasErrorOrSorry then return - for d in defsParsedSnap.defs, view in views do + for d in defsParsedSnap.defs, (ref, kind) in views do let logGoalsAccomplished := let msgData := .tagged `goalsAccomplished m!"Goals accomplished!" - logAt view.ref msgData (severity := .information) (isSilent := true) - match view.kind with + logAt ref msgData (severity := .information) (isSilent := true) + match kind with | .theorem => logGoalsAccomplished | .example =>