From 1c2aacc4a8a476d671cdcc750ecb6a85e17e4b67 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 22 Jun 2021 19:14:57 +0200 Subject: [PATCH] fix: worker: don't wait for tasks on exit --- src/Lean/Server/FileWorker.lean | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index d44845d5fa..6010e8f49f 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -355,7 +355,12 @@ def workerMain : IO UInt32 := do let o ← IO.getStdout let e ← IO.getStderr try - initAndRunWorker i o e + let exitCode ← initAndRunWorker i o e + -- HACK: all `Task`s are currently "foreground", i.e. we join on them on main thread exit, but we definitely don't + -- want to do that in the case of the worker processes, which can produce non-terminating tasks evaluating user code + o.flush + e.flush + IO.Process.exit exitCode.toUInt8 catch err => e.putStrLn s!"worker initialization error: {err}" return (1 : UInt32)