From d9c6a992b5faceb2ca36e6848353e7b9f3385e58 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Thu, 21 Jan 2021 14:43:30 -0500 Subject: [PATCH] feat: specify version in waitForDiagnostics --- src/Lean/Data/Lsp/Extra.lean | 14 ++++++++------ src/Lean/Data/Lsp/Ipc.lean | 4 ++-- src/Lean/Server/FileSource.lean | 2 +- src/Lean/Server/FileWorker.lean | 21 ++++++++++++++++----- src/Lean/Server/Watchdog.lean | 2 +- tests/lean/server/diags.lean | 2 +- tests/lean/server/edits.lean | 4 ++-- tests/lean/server/init_exit_worker.lean | 2 +- 8 files changed, 32 insertions(+), 19 deletions(-) diff --git a/src/Lean/Data/Lsp/Extra.lean b/src/Lean/Data/Lsp/Extra.lean index b8510bb557..ec240c916b 100644 --- a/src/Lean/Data/Lsp/Extra.lean +++ b/src/Lean/Data/Lsp/Extra.lean @@ -8,20 +8,22 @@ import Lean.Data.Json import Lean.Data.JsonRpc import Lean.Data.Lsp.Basic -/- +/-! This file contains Lean-specific extensions to LSP. The following additional packets are supported: -- "textDocument/waitForDiagnostics": Yields a response when all the diagnostics that were pending at the time of - arrival of the packet have been emitted. Exists for synchronization purposes, e.g. during testing or when external tools might want to use - our LSP server. +- "textDocument/waitForDiagnostics": Yields a response when all the diagnostics for a version of the document + greater or equal to the specified one have been emitted. If the request specifies a version above the most + recently processed one, the server will delay the response until it does receive the specified version. + Exists for synchronization purposes, e.g. during testing or when external tools might want to use our LSP server. -/ namespace Lean.Lsp open Json -structure WaitForDiagnosticsParam where - uri : DocumentUri +structure WaitForDiagnosticsParams where + uri : DocumentUri + version : Nat deriving ToJson, FromJson structure WaitForDiagnostics diff --git a/src/Lean/Data/Lsp/Ipc.lean b/src/Lean/Data/Lsp/Ipc.lean index 408999933f..7469cf43cf 100644 --- a/src/Lean/Data/Lsp/Ipc.lean +++ b/src/Lean/Data/Lsp/Ipc.lean @@ -50,9 +50,9 @@ def waitForExit : IpcM UInt32 := do /-- Waits for the worker to emit all diagnostics for the current document version and returns them as a list. -/ -partial def collectDiagnostics (waitForDiagnosticsId : RequestID := 0) (target : DocumentUri) +partial def collectDiagnostics (waitForDiagnosticsId : RequestID := 0) (target : DocumentUri) (version : Nat) : IpcM (List (Notification PublishDiagnosticsParams)) := do - writeRequest ⟨waitForDiagnosticsId, "textDocument/waitForDiagnostics", WaitForDiagnosticsParam.mk target⟩ + writeRequest ⟨waitForDiagnosticsId, "textDocument/waitForDiagnostics", WaitForDiagnosticsParams.mk target version⟩ let rec loop : IpcM (List (Notification PublishDiagnosticsParams)) := do match ←readMessage with | Message.response id _ => diff --git a/src/Lean/Server/FileSource.lean b/src/Lean/Server/FileSource.lean index 8d6a152636..6b16a61a78 100644 --- a/src/Lean/Server/FileSource.lean +++ b/src/Lean/Server/FileSource.lean @@ -52,7 +52,7 @@ instance DefinitionParams.hasFileSource : FileSource DefinitionParams := instance TypeDefinitionParams.hasFileSource : FileSource TypeDefinitionParams := ⟨fun h => fileSource h.toTextDocumentPositionParams⟩ -instance WaitForDiagnosticsParam.hasFileSource : FileSource WaitForDiagnosticsParam := +instance WaitForDiagnosticsParams.hasFileSource : FileSource WaitForDiagnosticsParams := ⟨fun p => p.uri⟩ instance DocumentSymbolParams.hasFileSource : FileSource DocumentSymbolParams := diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 0635a7880a..cedbfa9cdb 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -488,12 +488,23 @@ section RequestHandling children? := syms.toArray } :: syms', stxs'') - def handleWaitForDiagnostics (id : RequestID) (p : WaitForDiagnosticsParam) + partial def handleWaitForDiagnostics (id : RequestID) (p : WaitForDiagnosticsParams) : ServerM (Task (Except IO.Error (Except RequestError WaitForDiagnostics))) := do let st ← read - let doc ← st.docRef.get - let t ← doc.cmdSnaps.waitAll - t.map fun _ => Except.ok $ Except.ok WaitForDiagnostics.mk + let rec waitLoop : IO EditableDocument := do + let doc ← st.docRef.get + if p.version ≤ doc.meta.version then + return doc + else + IO.sleep 50 + waitLoop + let t ← IO.asTask waitLoop + let t ← IO.bindTask t fun + | Except.error e => unreachable! + | Except.ok doc => do + let t₁ ← doc.cmdSnaps.waitAll + return t₁.map fun _ => Except.ok WaitForDiagnostics.mk + return t.map fun _ => Except.ok <| Except.ok WaitForDiagnostics.mk end RequestHandling @@ -531,7 +542,7 @@ section MessageHandling st.hOut.writeLspResponseError { id := id, code := ErrorCode.internalError, message := toString e } queueRequest id t₁ match method with - | "textDocument/waitForDiagnostics" => handle WaitForDiagnosticsParam WaitForDiagnostics handleWaitForDiagnostics + | "textDocument/waitForDiagnostics" => handle WaitForDiagnosticsParams WaitForDiagnostics handleWaitForDiagnostics | "textDocument/hover" => handle HoverParams (Option Hover) handleHover | "textDocument/declaration" => handle TextDocumentPositionParams (Array LocationLink) <| handleDefinition (goToType? := false) | "textDocument/definition" => handle TextDocumentPositionParams (Array LocationLink) <| handleDefinition (goToType? := false) diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index 8725c505f6..6bbbde5ee6 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -379,7 +379,7 @@ section MessageHandling let uri := fileSource parsedParams tryWriteMessage uri ⟨id, method, parsedParams⟩ FileWorker.writeRequest match method with - | "textDocument/waitForDiagnostics" => handle WaitForDiagnosticsParam + | "textDocument/waitForDiagnostics" => handle WaitForDiagnosticsParams | "textDocument/hover" => handle HoverParams | "textDocument/declaration" => handle DeclarationParams | "textDocument/definition" => handle DefinitionParams diff --git a/tests/lean/server/diags.lean b/tests/lean/server/diags.lean index 50fe52e7ca..1430392dde 100644 --- a/tests/lean/server/diags.lean +++ b/tests/lean/server/diags.lean @@ -11,7 +11,7 @@ open IO Lean Lsp hIn.write (←FS.readBinFile "open_content.log") hIn.flush - let diags ← Ipc.collectDiagnostics 1 "file:///test.lean" + let diags ← Ipc.collectDiagnostics 1 "file:///test.lean" 1 if diags.isEmpty then throw $ userError "Test failed, no diagnostics received." else diff --git a/tests/lean/server/edits.lean b/tests/lean/server/edits.lean index a02855da21..a5bd750a6a 100644 --- a/tests/lean/server/edits.lean +++ b/tests/lean/server/edits.lean @@ -12,12 +12,12 @@ open IO Lean Lsp hIn.write (←FS.readBinFile "open_content.log") hIn.flush - discard <| Ipc.collectDiagnostics 1 "file:///test.lean" + discard <| Ipc.collectDiagnostics 1 "file:///test.lean" 1 hIn.write (←FS.readBinFile "content_changes.log") hIn.flush - let diags ← Ipc.collectDiagnostics 2 "file:///test.lean" + let diags ← Ipc.collectDiagnostics 2 "file:///test.lean" 7 if diags.isEmpty then throw $ userError "Test failed, no diagnostics received." else diff --git a/tests/lean/server/init_exit_worker.lean b/tests/lean/server/init_exit_worker.lean index 8643fd7fcc..a9bcb0981f 100644 --- a/tests/lean/server/init_exit_worker.lean +++ b/tests/lean/server/init_exit_worker.lean @@ -9,7 +9,7 @@ open IO Lean Lsp hIn.write (←FS.readBinFile "open_empty.log") hIn.flush - let diags ← Ipc.collectDiagnostics 1 "file:///empty" + let diags ← Ipc.collectDiagnostics 1 "file:///empty" 1 assert! diags.length == 1 Ipc.writeNotification ⟨"exit", Json.null⟩