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!