max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: add a better handling in case only worker crashes

Browse source
This commit is contained in:
Mariana Alanis 2022-06-13 14:04:22 -05:00 • committed by Leonardo de Moura
parent 6b75ca9734
commit b0f9754e0f
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Server/Watchdog.lean
View file

@ -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 in user 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"}."
return WorkerEvent.crashed err
loop
let task ← IO.asTask (loop $ ←read) Task.Priority.dedicated