From c268d7e97bb075427a8412cceecc4e483379ac25 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 3 Jul 2023 11:30:35 +0200
Subject: [PATCH] fix: kill descendant processes on worker exit

---
 src/Lean/Server/Watchdog.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
index dadce6cac3..b67bb04ddb 100644
--- a/src/Lean/Server/Watchdog.lean
+++ b/src/Lean/Server/Watchdog.lean
@@ -210,6 +210,9 @@ section ServerM
         -- If writeLspMessage from above errors we will block here, but the main task will
         -- quit eventually anyways if that happens
         let exitCode ← fw.proc.wait
+        -- Remove surviving descendant processes, if any, such as from nested builds.
+        -- On Windows, we instead rely on elan doing this.
+        try fw.proc.kill catch _ => pure ()
         match exitCode with
         | 0 =>
           -- Worker was terminated
@@ -241,6 +244,8 @@ section ServerM
       toStdioConfig := workerCfg
       cmd           := st.workerPath.toString
       args          := #["--worker"] ++ st.args.toArray ++ #[m.uri]
+      -- open session for `kill` above
+      setsid        := true
     }
     let pendingRequestsRef ← IO.mkRef (RBMap.empty : PendingRequestMap)
     -- The task will never access itself, so this is fine