From 30f3d6f82d463d2b34e21377e85a67c3ae0d8b52 Mon Sep 17 00:00:00 2001 From: Mariana Alanis Date: Tue, 14 Jun 2022 15:16:47 -0500 Subject: [PATCH] fix: add a better handling in case only worker crashes (CR comments) --- src/Lean/Server/Watchdog.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index 30a8e1b639..1b0ae8c662 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -259,7 +259,7 @@ section ServerM else -- Worker crashed fw.errorPendingRequests o (if exitCode = 1 then ErrorCode.workerCrashed else ErrorCode.stackOverflow) - s!"Server process for {fw.doc.meta.uri} crashed, {if exitCode = 1 then "see stderr for exception" else "likely due to a stack overflow or a bug in user's code"}." + s!"Server process for {fw.doc.meta.uri} crashed, {if exitCode = 1 then "see stderr for exception" else "likely due to a stack overflow or a bug in "user's" code"}." return WorkerEvent.crashed err loop let task ← IO.asTask (loop $ ←read) Task.Priority.dedicated