From d433fe58afaa9b8f6472ac52d207f555d972527e Mon Sep 17 00:00:00 2001
From: Marc Huisinga <mhuisi@protonmail.com>
Date: Tue, 6 Oct 2020 14:37:27 +0200
Subject: [PATCH] fix: broken pending request filtering in file worker and
 broken monad instance

---
 src/Lean/Server/FileWorker.lean | 11 +++++++++--
 src/Lean/Server/Utils.lean      |  4 ----
 2 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 2ae8d29937..36b9d9936d 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -279,7 +279,14 @@ partial def mainLoop : Unit → ServerM Unit
   st ← read;
   msg ← readLspMessage st.hIn;
   pendingRequests ← st.pendingRequestsRef.get;
-  pendingRequests ← monadLift $ pendingRequests.filterM (fun task => do f ← hasFinished task; pure ¬f);
+  let filterFinishedTasks : PendingRequestMap → RequestID → Task (Except IO.Error Unit) → IO PendingRequestMap := 
+    (fun acc id task => do
+      f ← hasFinished task;
+      pure $ if f then
+        acc.erase id
+      else
+        acc);
+  pendingRequests ← monadLift $ pendingRequests.foldM filterFinishedTasks pendingRequests;
   st.pendingRequestsRef.set pendingRequests;
   match msg with
   | Message.request id method (some params) => do
@@ -301,7 +308,7 @@ _ ← Lsp.readLspRequestAs i "initialize" InitializeParams;
 docRequest ← Lsp.readLspRequestAs i "textDocument/didOpen" DidOpenTextDocumentParams;
 doc ← openDocument o docRequest.param;
 docRef ← IO.mkRef doc;
-pendingRequestsRef ← IO.mkRef #[];
+pendingRequestsRef ← IO.mkRef (RBMap.empty : PendingRequestMap);
 runReader (mainLoop ()) (⟨i, o, docRef, pendingRequestsRef⟩ : ServerContext)
 
 end Server
diff --git a/src/Lean/Server/Utils.lean b/src/Lean/Server/Utils.lean
index be2a04fdb2..fd83283b7f 100644
--- a/src/Lean/Server/Utils.lean
+++ b/src/Lean/Server/Utils.lean
@@ -16,9 +16,5 @@ instance Thunk.monad : Monad Thunk :=
 { pure := @Thunk.pure,
   bind := @Thunk.bind }
 
-instance Task.monad : Monad Task :=
-{ pure := @Task.pure,
-  bind := @Task.bind }
-
 end Server
 end Lean