From 4d7d82af86d94051e175efa5398be4254e16c439 Mon Sep 17 00:00:00 2001
From: Mariana Alanis <malanistamez@microsoft.com>
Date: Tue, 14 Jun 2022 11:59:39 -0500
Subject: [PATCH] fix: add a better handling in case only worker crashes (CR
 comments)

---
 src/Lean/Data/JsonRpc.lean               | 13 ++++++++-----
 src/Lean/Server/FileWorker.lean          |  2 +-
 src/Lean/Server/Rpc/RequestHandling.lean |  2 +-
 src/Lean/Server/Watchdog.lean            |  4 ++--
 4 files changed, 12 insertions(+), 9 deletions(-)

diff --git a/src/Lean/Data/JsonRpc.lean b/src/Lean/Data/JsonRpc.lean
index 5fbcd69114..838e175aa9 100644
--- a/src/Lean/Data/JsonRpc.lean
+++ b/src/Lean/Data/JsonRpc.lean
@@ -37,6 +37,7 @@ inductive ErrorCode where
   | invalidRequest
   | methodNotFound
   | invalidParams
+  | internalError
   | workerCrashed
   | stackOverflow
   | serverNotInitialized
@@ -53,13 +54,14 @@ instance : FromJson ErrorCode := ⟨fun
   | num (-32600 : Int) => return ErrorCode.invalidRequest
   | num (-32601 : Int) => return ErrorCode.methodNotFound
   | num (-32602 : Int) => return ErrorCode.invalidParams
-  | num (-32603 : Int) => return ErrorCode.workerCrashed
-  | num (-32604 : Int) => return ErrorCode.stackOverflow
+  | num (-32603 : Int) => return ErrorCode.internalError
   | num (-32002 : Int) => return ErrorCode.serverNotInitialized
   | num (-32001 : Int) => return ErrorCode.unknownErrorCode
   | 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
   | _  => throw "expected error code"⟩
 
 instance : ToJson ErrorCode := ⟨fun
@@ -67,13 +69,14 @@ instance : ToJson ErrorCode := ⟨fun
   | ErrorCode.invalidRequest       => (-32600 : Int)
   | ErrorCode.methodNotFound       => (-32601 : Int)
   | ErrorCode.invalidParams        => (-32602 : Int)
-  | ErrorCode.workerCrashed       => (-32603 : Int)
-  | ErrorCode.stackOverflow        => (-32604 : Int)
+  | ErrorCode.internalError        => (-32603 : Int)
   | ErrorCode.serverNotInitialized => (-32002 : Int)
   | ErrorCode.unknownErrorCode     => (-32001 : Int)
   | ErrorCode.contentModified      => (-32801 : Int)
   | ErrorCode.requestCancelled     => (-32800 : Int)
-  | ErrorCode.rpcNeedsReconnect    => (-32900 : Int)⟩
+  | ErrorCode.rpcNeedsReconnect    => (-32900 : Int)
+  | ErrorCode.workerCrashed        => (-32901 : Int)
+  | ErrorCode.stackOverflow        => (-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/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index dacf1cf53d..972920c3b0 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -401,7 +401,7 @@ section MessageHandling
       catch e =>
         ctx.hOut.writeLspResponseError
           { id
-            code := ErrorCode.workerCrashed
+            code := ErrorCode.internalError
             message := toString e }
       return
 
diff --git a/src/Lean/Server/Rpc/RequestHandling.lean b/src/Lean/Server/Rpc/RequestHandling.lean
index 1c682f7325..1da7da08fd 100644
--- a/src/Lean/Server/Rpc/RequestHandling.lean
+++ b/src/Lean/Server/Rpc/RequestHandling.lean
@@ -42,7 +42,7 @@ private unsafe def handleRpcCallUnsafe (p : Lsp.RpcCallParams) : RequestM (Reque
         match proc with
         | Except.ok x => x.wrapper p.sessionId p.params
         | Except.error e => throwThe RequestError {
-          code := JsonRpc.ErrorCode.workerCrashed
+          code := JsonRpc.ErrorCode.internalError
           message := s!"Failed to evaluate RPC constant '{procName}': {e}" }
       else
         throwThe RequestError {
diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
index e4e7192424..30a8e1b639 100644
--- a/src/Lean/Server/Watchdog.lean
+++ b/src/Lean/Server/Watchdog.lean
@@ -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"}."
+            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"}."
           return WorkerEvent.crashed err
       loop
     let task ← IO.asTask (loop $ ←read) Task.Priority.dedicated
@@ -522,7 +522,7 @@ section MessageHandling
         -- TODO Do fancier error handling, like in file worker?
         | e => hOut.writeLspResponseError {
           id := id
-          code := ErrorCode.workerCrashed
+          code := ErrorCode.internalError
           message := s!"Failed to process request {id}: {e}"
         }
     -- If a definition is in a different, modified file, the ilean data should