fix: add a better handling in case only worker crashes (apply CR comments)

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. -/

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 :=

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