From 9efe4283e2ea1dff90e2572cbb0c348dda0a677c Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 30 Apr 2026 11:22:33 +0200 Subject: [PATCH] fix: propagate parent cancel token to parallel tactic subtasks (#13428) This PR fixes parallel tactic combinators (`attempt_all_par`, `first_par`) leaking their subtasks when the server cancels elaboration on re-elaboration. Subtasks spawned via `CoreM.asTask` (and its `MetaM`/`TermElabM`/`TacticM` variants) get a fresh `IO.CancelToken`, which previously had no link to the parent token; `cancelRec` would set the command-level token but the children kept running. The fix is one line in `CoreM.asTask`: when a parent token is in scope, register `cancelToken.set` as an `onSet` callback on the parent. Server-level cancellation now flows down to every parallel subtask, and `Core.checkInterrupted` inside the child sees the token set as expected. Fixes #13300. Co-Authored-By: Claude Opus 4.7 --------- Co-authored-by: Claude Opus 4.6 --- src/Lean/Elab/Task.lean | 5 +++++ tests/server_interactive/cancellation_par.lean.out.expected | 2 -- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/Lean/Elab/Task.lean b/src/Lean/Elab/Task.lean index 4248920ef2..aeebc74517 100644 --- a/src/Lean/Elab/Task.lean +++ b/src/Lean/Elab/Task.lean @@ -51,6 +51,11 @@ def asTask (t : CoreM α) : CoreM (BaseIO Unit × Task (CoreM α)) := do -- but modify it to return both the result and state let wrappedAct ← Core.wrapAsync (fun () => do let a ← t; let s ← get; return (a, s)) (some cancelToken) let task ← (wrappedAct ()).asTask + -- Propagate parent cancel token to child: when the parent is cancelled, + -- the child token is set too. This ensures that subtasks spawned via `asTask` + -- respond to server-level cancellation (e.g. on re-elaboration). + if let some parentTk := (← read).cancelTk? then + parentTk.onSet cancelToken.set return (cancelToken.set, task.map (sync := true) fun result => match result with | .ok (a, s) => do diff --git a/tests/server_interactive/cancellation_par.lean.out.expected b/tests/server_interactive/cancellation_par.lean.out.expected index 2f11c7a36a..b16d7e5966 100644 --- a/tests/server_interactive/cancellation_par.lean.out.expected +++ b/tests/server_interactive/cancellation_par.lean.out.expected @@ -2,7 +2,5 @@ blocked! cancelled! blocked! cancelled! -attempt_all_par: leaked! blocked! cancelled! -first_par: leaked!