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

feat: publish fatal progress after worker crash

Browse source
This commit is contained in:
Sebastian Ullrich 2022-06-19 18:25:57 +02:00 • committed by Leonardo de Moura
parent c213e0e880
commit 17c2e6d529
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -260,6 +260,7 @@ section ServerM
-- Worker crashed
fw.errorPendingRequests o (if exitCode = 1 then ErrorCode.workerExited else ErrorCode.workerCrashed)
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"}."
publishProgressAtPos fw.doc.meta 0 o (kind := LeanFileProgressKind.fatalError)
return WorkerEvent.crashed err
loop
let task ← IO.asTask (loop $ ←read) Task.Priority.dedicated