Zulip Chat Archive
Stream: lean4
Topic: Force-cancelling a task?
František Silváši (Apr 05 2022 at 21:12):
Is there a simple way to cancel a running task 'un-cooperatively'? The function IO.cancel task
requires that task
cooperates and handles its own IO.checkCanceled
. Currently my task
is IO.asTask <| IO.Process.run someProcess
and there's no simple way (AFAIK) to check for the cancellation request. I basically run a couple of processes and want to cancel the ones that don't terminate within a given timeout, as I am not interested in their outputs thereafter.
EDIT: I still don't know how to force-cancel a process, but I implemented a simple workaround that calls Task.spawn
and handles timeouts explicitly / gets cancelled cooperatively with IO.cancel
, a'la IO.Process.runWithTimeout
.
Last updated: Dec 20 2023 at 11:08 UTC