Interrupting command in VSCode does not kill it

Stream: lean4

[Yicheng Qian]

It seems that interrupting commands that invokes IO.Process.spawn in VSCode does not kill the child being spawned. Here is a mwe (in Linux(WSL)):

import Lean
open Lean

def spawnSleep (n : Nat) : IO UInt32 := do
  let proc ← IO.Process.spawn
    {stdin := .piped, stdout := .piped, stderr := .piped, cmd := "sleep", args := #[s!"{n}"]}
  proc.wait

-- Type something here --> <-- multiple times to interrupt the normal execution of the following command
#eval spawnSleep 30

If we type at the --> <-- multiple times with short pauses in between, we can see multiple sleep running in the background.

[Yicheng Qian]

Some context: I'm working on a tactic that invokes external commands. If some theorem in a file invokes my tactic, and I keep editing that file for a while, my computer becomes extremely slow and sometimes even crashes.

[Yicheng Qian]

Restarting lean server on the file (ctrl+shift+x) kills the spawned process

[Yicheng Qian]

But re-loading the imports can take a long time.

[Sebastian Ullrich]

wait maps more or less directly to the OS primitive, there isn't really anything the elaborator could do to interrupt it. I would suggest busy-waiting with a small sleep and using Child.kill if IO.checkCanceled returns true, which the elaborator sets on cancellation starting with 4.3.0-rc1.

[Joe Hendrix]

@Yicheng Qian I'm working on Lean bindings to libuv as a side project. Right now, there isn't much there, but I am working on TCP. I plan to start adding process creation once that's done.

I'll see if we can have a way of creating a libuv async that is triggered when IO.checkCanceled is set. That should provide a mechanism for waiting for processes but killing them if the elaborator sets cancellation. This doesn't help immediately, but should provide a more robust long term API.

[Yicheng Qian]

Sebastian Ullrich said:

wait maps more or less directly to the OS primitive, there isn't really anything the elaborator could do to interrupt it. I would suggest busy-waiting with a small sleep and using Child.kill if IO.checkCanceled returns true, which the elaborator sets on cancellation starting with 4.3.0-rc1.

Sorry, I'm confused about the approach, and I can't find busy-waiting primitives (non-blocking ones) in Lean. Can you provide a modified spawnSleep that kills the child when interrupted?

[Yicheng Qian]

I tried this:

def spawnSleep (n : Nat) : IO Nat := do
  let proc ← IO.Process.spawn
    {stdin := .piped, stdout := .piped, stderr := .piped, cmd := "sleep", args := #[s!"{n}"]}
  let _ ← IO.asTask (do
    let start ← IO.monoMsNow
    while true do
      IO.sleep 100
      if ← IO.checkCanceled then
        proc.kill
        break
      if (← IO.monoMsNow) - start > n * 2000 then
        break)
  let _ ← proc.wait
  return 0

But the sleep is not killed when the command is interrupted.

[Sebastian Ullrich]

Oh, if you do that in a separate Task, it will have its own cancellation flag. If you switch it around, i.e. do the Child.wait in a task and busy-wait on it in the main thread using IO.hasFinished, I believe it should work on 4.3.0-rc1+.

[Sebastian Ullrich]

If we had https://doc.rust-lang.org/std/process/struct.Child.html#method.try_wait, the additional task would not be necessary

[Yicheng Qian]

Great! Now it works

def spawnSleep₂ (n : Nat) : IO Nat := do
  let proc ← IO.Process.spawn
    {stdin := .piped, stdout := .piped, cmd := "sleep", args := #[s!"{n}"]}
  let tsk ← IO.asTask proc.wait
  while true do
    IO.sleep 100
    if ← IO.checkCanceled then
      proc.kill
      break
    if ← IO.hasFinished tsk then
      break
  return 0

-- Type something here --> <-- multiple times to interrupt the normal execution of the following command
#eval spawnSleep₂ 5

[Yicheng Qian]

But this seems a bit magical to me.

[Yicheng Qian]

Why proc.kill is still executed even after the command is interrupted ...

[Sebastian Ullrich]

Yicheng Qian said:

But this seems a bit magical to me.

I wouldn't call it ergonomic, but from my point of view it would be more magical if the original code just worked :)

[Sebastian Ullrich]

Yicheng Qian said:

Why proc.kill is still executed even after the command is interrupted ...

What do you mean?

[Yicheng Qian]

I'm thinking that, when the command #eval spawnSleep₂ 5 is interrupted (when I type something above it), it's likely that we're in IO.sleep 100, and everything below will not be executed after the interruption. So I'm surprised that proc.kill is still executed and sleep is killed.

[Sebastian Ullrich]

Task cancellation is cooperative, nothing will be skipped until someone uses checkCanceled. I/O primitives like sleep don't check it, and the sleep itself is not interruptible either.

[Yicheng Qian]

Ah, I see.

[Yicheng Qian]

I certainly didn't know that before. I though that lean would just interrupt the task right at the command it's executing.

def spin : IO Unit := do
  let mut i := 0
  while true do
    i := i + 1
    if i % 10000000 == 0 then
      IO.println "Oh"

-- Type something here --> <-- multiple times to interrupt the normal execution of the following command
#eval spin

If I type at --> <-- for k times, top will tell me that lean uses (k+1) * 100% CPU :)

[Yicheng Qian]

So this issue is not necessarily related to IO.spawn.

[Notification Bot]

This topic was moved here from #lean4 > Interrupting spawn in VSCode does not kill child by Yicheng Qian.

[Yicheng Qian]

Anyway checkCanceled still solves the issue

def spin : IO Unit := do
  let mut i := 0
  while true do
    i := i + 1
    if i % 10000000 == 0 then
      IO.println "Oh"
    if ← IO.checkCanceled then
      break

[Yicheng Qian]

Btw

def spin : IO Unit := do
  let mut i := 0
  while true do
    i := i + 1

#eval spin

causes

Lean server printed an error: libc++abi: terminating due to uncaught exception of type lean::exception: unreachable code

should this be considered an issue?

[Sebastian Ullrich]

That does look like an issue