From 17c2e6d529421850f1237636546599eb392cd252 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sun, 19 Jun 2022 18:25:57 +0200
Subject: [PATCH] feat: publish fatal progress after worker crash

---
 src/Lean/Server/Watchdog.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
index e530f2b373..ce09f372cf 100644
--- a/src/Lean/Server/Watchdog.lean
+++ b/src/Lean/Server/Watchdog.lean
@@ -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