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 (CR comments)

Browse source
This commit is contained in:
Mariana Alanis 2022-06-14 15:31:08 -05:00 • committed by Leonardo de Moura
parent 30f3d6f82d
commit e61799a77f
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 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 code"}."
return WorkerEvent.crashed err
loop
let task ← IO.asTask (loop $ ←read) Task.Priority.dedicated