From 198179d0ccdff19e688bbb8b69ef8e6bbc997e61 Mon Sep 17 00:00:00 2001
From: Mariana Alanis <malanistamez@microsoft.com>
Date: Wed, 15 Jun 2022 12:20:40 -0500
Subject: [PATCH] fix: add a better handling in case only worker crashes (apply
 CR comments)

---
 src/Lean/Data/JsonRpc.lean    | 12 ++++++------
 src/Lean/Server/Requests.lean |  2 +-
 src/Lean/Server/Watchdog.lean |  4 ++--
 3 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/src/Lean/Data/JsonRpc.lean b/src/Lean/Data/JsonRpc.lean
index 838e175aa9..a72d739c82 100644
--- a/src/Lean/Data/JsonRpc.lean
+++ b/src/Lean/Data/JsonRpc.lean
@@ -38,8 +38,6 @@ inductive ErrorCode where
   | methodNotFound
   | invalidParams
   | internalError
-  | workerCrashed
-  | stackOverflow
   | serverNotInitialized
   | unknownErrorCode
   -- LSP-specific codes below.
@@ -47,6 +45,8 @@ inductive ErrorCode where
   | requestCancelled
   -- Lean-specific codes below.
   | rpcNeedsReconnect
+  | workerExited
+  | workerCrashed
   deriving Inhabited, BEq
 
 instance : FromJson ErrorCode := ⟨fun
@@ -60,8 +60,8 @@ instance : FromJson ErrorCode := ⟨fun
   | num (-32801 : Int) => return ErrorCode.contentModified
   | num (-32800 : Int) => return ErrorCode.requestCancelled
   | num (-32900 : Int) => return ErrorCode.rpcNeedsReconnect
-  | num (-32901 : Int) => return ErrorCode.workerCrashed
-  | num (-32902 : Int) => return ErrorCode.stackOverflow
+  | num (-32901 : Int) => return ErrorCode.workerExited
+  | num (-32902 : Int) => return ErrorCode.workerCrashed
   | _  => throw "expected error code"⟩
 
 instance : ToJson ErrorCode := ⟨fun
@@ -75,8 +75,8 @@ instance : ToJson ErrorCode := ⟨fun
   | ErrorCode.contentModified      => (-32801 : Int)
   | ErrorCode.requestCancelled     => (-32800 : Int)
   | ErrorCode.rpcNeedsReconnect    => (-32900 : Int)
-  | ErrorCode.workerCrashed        => (-32901 : Int)
-  | ErrorCode.stackOverflow        => (-32902 : Int)⟩
+  | ErrorCode.workerExited        => (-32901 : Int)
+  | ErrorCode.workerCrashed        => (-32902 : Int)⟩
 
 /- Uses separate constructors for notifications and errors because client and server
 behavior is expected to be wildly different for both. -/
diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean
index 169583838f..e4588cf6c5 100644
--- a/src/Lean/Server/Requests.lean
+++ b/src/Lean/Server/Requests.lean
@@ -38,7 +38,7 @@ def methodNotFound (method : String) : RequestError :=
     message := s!"No request handler found for '{method}'" }
 
 instance : Coe IO.Error RequestError where
-  coe e := { code := ErrorCode.workerCrashed
+  coe e := { code := ErrorCode.internalError
              message := toString e }
 
 def toLspResponseError (id : RequestID) (e : RequestError) : ResponseError Unit :=
diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
index d35a7a778a..e530f2b373 100644
--- a/src/Lean/Server/Watchdog.lean
+++ b/src/Lean/Server/Watchdog.lean
@@ -258,8 +258,8 @@ section ServerM
           return WorkerEvent.terminated
         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 code"}."
+          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"}."
           return WorkerEvent.crashed err
       loop
     let task ← IO.asTask (loop $ ←read) Task.Priority.dedicated