From 37a49afd7b6fdc62056febfae889eaafd509f1c9 Mon Sep 17 00:00:00 2001
From: Marc Huisinga <mhuisi@protonmail.com>
Date: Sun, 29 Nov 2020 18:08:35 +0100
Subject: [PATCH] fix: snapshot list divergence & stale diagnostics

---
 src/Lean/Server/AsyncList.lean  |  2 +-
 src/Lean/Server/FileSource.lean |  4 ++--
 src/Lean/Server/FileWorker.lean | 20 +++++++++++++++++---
 3 files changed, 20 insertions(+), 6 deletions(-)

diff --git a/src/Lean/Server/AsyncList.lean b/src/Lean/Server/AsyncList.lean
index 06bef3d8c2..c72391477c 100644
--- a/src/Lean/Server/AsyncList.lean
+++ b/src/Lean/Server/AsyncList.lean
@@ -94,7 +94,7 @@ partial def updateFinishedPrefix : AsyncList ε α → IO (AsyncList ε α × Op
 private partial def finishedPrefixAux : List α → AsyncList ε α → List α
   | acc, cons hd tl      => finishedPrefixAux (hd :: acc) tl
   | acc, nil             => acc
-  | acc, asyncCons hd tl => acc
+  | acc, asyncCons hd tl => hd :: acc
 
 /-- The longest already-computed prefix of the stream. -/
 def finishedPrefix : AsyncList ε α → List α :=
diff --git a/src/Lean/Server/FileSource.lean b/src/Lean/Server/FileSource.lean
index 8f87277bef..e5484f681b 100644
--- a/src/Lean/Server/FileSource.lean
+++ b/src/Lean/Server/FileSource.lean
@@ -9,8 +9,8 @@ import Lean.Data.Lsp
 namespace Lean
 namespace Lsp
 
-class FileSource (α : Type) :=
-  (fileSource : α → DocumentUri)
+class FileSource (α : Type) where
+  fileSource : α → DocumentUri
 export FileSource (fileSource)
 
 instance Location.hasFileSource : FileSource Location :=
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index ac69497206..6b4fe0f1a4 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -53,7 +53,7 @@ private def sendDiagnostics (h : FS.Stream) (uri : DocumentUri) (version : Nat)
       : PublishDiagnosticsParams }
 
 private def logSnapContent (s : Snapshot) (text : FileMap) : IO Unit :=
-  IO.eprintln $ "`" ++ text.source.extract s.beginPos (s.endPos-1) ++ "`"
+  IO.eprintln s!"[{s.beginPos}, {s.endPos}]: `{text.source.extract s.beginPos (s.endPos-1)}`"
 
 inductive TaskError where
   | aborted
@@ -135,11 +135,25 @@ def updateDocument (h : FS.Stream) (uri : DocumentUri) (doc : EditableDocument)
     -- so a change on some whitespace after a command recompiles it. We could
     -- be more precise.
     let validSnaps := cmdSnaps.finishedPrefix.takeWhile (fun s => s.endPos < changePos)
+    -- TODO(MH): remove temporary logging
+    IO.eprintln s!"changePos: {changePos}"
+    IO.eprintln "validSnaps:"
+    for snap in validSnaps do
+      logSnapContent snap doc.text
+    IO.eprintln "finishedPrefix:"
+    for snap in cmdSnaps.finishedPrefix do
+      logSnapContent snap doc.text
+    IO.eprintln "---"
     -- NOTE: the watchdog never sends didChange notifs with a header change to the
     -- worker, so the header snapshot is always valid.
     let lastSnap := validSnaps.getLastD doc.headerSnap
-    let newSnaps ← unfoldCmdSnaps h uri newVersion newText lastSnap
-    let newCmdSnaps := AsyncList.ofList validSnaps ++ newSnaps
+    let newCmdSnaps ← match validSnaps.get? (validSnaps.length - 2) with
+      | none => do
+        let newSnaps ← unfoldCmdSnaps h uri newVersion newText lastSnap
+        pure $ AsyncList.ofList validSnaps.dropLast ++ newSnaps
+      | some secondLastSnap => do
+        let newSnaps ← unfoldCmdSnaps h uri newVersion newText secondLastSnap
+        pure $ AsyncList.ofList (validSnaps.take (validSnaps.length - 2)) ++ newSnaps
     -- NOTE: We do not cancel old tasks explicitly, the GC does this for us when no refs remain.
     pure ⟨newVersion, newText, newHeaderSnap, newCmdSnaps⟩