feat: server-side support for incremental diagnostics (#13260)

This PR adds server-side support for incremental diagnostics via a new
`isIncremental` field on `PublishDiagnosticsParams` that is only used by
the language server when clients set `incrementalDiagnosticSupport` in
`LeanClientCapabilities`.

### Context

The goal of this new feature is to avoid quadratic reporting of
diagnostics.

LSP has two means of reporting diagnostics; pull diagnostics (where the
client decides when to fetch the diagnostics of a project) and push
diagnostics (where the server decides when to update the set of
diagnostics of a file in the client).
Pull diagnostics have the inherent problem that clients need to
heuristically decide when the set of diagnostics should be updated, and
that diagnostics can only be incrementally reported per file, so the
Lean language server has always stuck with push diagnostics instead.
In principle, push diagnostics were also intended to only be reported
once for a full file, but all major language clients also support
replacing the old set of diagnostics for a file when a new set of
diagnostics is reported for the same version of the file, so we have
always reported diagnostics incrementally while the file is being
processed in this way.
However, this approach has a major limitation: all notifications must be
a full set of diagnostics, which means that we have to report a
quadratic amount of diagnostics while processing a file to the end.

### Semantics

When `LeanClientCapabilities.incrementalDiagnosticSupport` is set, the
language server will set `PublishDiagnosticsParams.isIncremental` when
it is reporting a set of diagnostics that should simply be appended to
the previously reported set of diagnostics instead of replacing it.
Specifically, clients implementing this new feature should implement the
following behaviour:
- If `PublishDiagnosticsParams.isIncremental` is `false` or the field is
missing, the current diagnostic report for a specific document should
replace the previous diagnostic report for that document instead of
appending to it. This is identical to the current behavior before this
PR.
- If `PublishDiagnosticsParams.isIncremental` is `true`, the current
diagnostic report for a specific document should append to the previous
diagnostic report for that document instead of replacing it.
- Versions should be ignored when deciding whether to replace or append
to a previous set of diagnostics. The language server ensures that the
`isIncremental` flag is set correctly.

### Client-side implementation

A client-side implementation for the VS Code extension can be found at
[vscode-lean4#752](https://github.com/leanprover/vscode-lean4/pull/752).

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
Co-authored-by: Wojciech Nawrocki <13901751+Vtec234@users.noreply.github.com>

src/Lean/Data/Lsp/Capabilities.lean

@@ -64,6 +64,12 @@ structure WorkspaceClientCapabilities where
   deriving ToJson, FromJson
 
 structure LeanClientCapabilities where
+  /--
+  Whether the client supports incremental `textDocument/publishDiagnostics` updates.
+  If `none` or `false`, the server will never set `PublishDiagnosticsParams.isIncremental?`
+  and always report full diagnostic updates that replace the previous one.
+  -/
+  incrementalDiagnosticSupport? : Option Bool := none
   /--
   Whether the client supports `DiagnosticWith.isSilent = true`.
   If `none` or `false`, silent diagnostics will not be served to the client.
@@ -84,6 +90,13 @@ structure ClientCapabilities where
   lean?         : Option LeanClientCapabilities         := none
   deriving ToJson, FromJson
 
+def ClientCapabilities.incrementalDiagnosticSupport (c : ClientCapabilities) : Bool := Id.run do
+  let some lean := c.lean?
+    | return false
+  let some incrementalDiagnosticSupport := lean.incrementalDiagnosticSupport?
+    | return false
+  return incrementalDiagnosticSupport
+
 def ClientCapabilities.silentDiagnosticSupport (c : ClientCapabilities) : Bool := Id.run do
   let some lean := c.lean?
     | return false

src/Lean/Data/Lsp/Diagnostics.lean

@@ -159,6 +159,14 @@ abbrev Diagnostic := DiagnosticWith String
 structure PublishDiagnosticsParams where
   uri : DocumentUri
   version? : Option Int := none
+  /--
+  Whether the client should append this set of diagnostics to the previous set
+  rather than replacing the previous set by this one (the default LSP behavior).
+  `false` means the client should replace.
+  `none` is equivalent to `false`.
+  This is a Lean-specific extension (see `LeanClientCapabilities`).
+  -/
+  isIncremental? : Option Bool := none
   diagnostics : Array Diagnostic
   deriving Inhabited, BEq, ToJson, FromJson
 

src/Lean/Data/Lsp/Ipc.lean

@@ -102,9 +102,32 @@ def normalizePublishDiagnosticsParams (p : PublishDiagnosticsParams) :
     sorted.toArray
 }
 
+/--
+Merges a new `textDocument/publishDiagnostics` notification into a previously accumulated one.
+
+- If there is no previous notification, the new one is used as-is.
+- If `isIncremental?` is `true`, the new diagnostics are appended.
+- Otherwise the new notification replaces the previous one.
+
+The returned params always have `isIncremental? := some false` since they represent the full
+accumulated set.
+-/
+def mergePublishDiagnosticsParams (prev? : Option PublishDiagnosticsParams)
+    (next : PublishDiagnosticsParams) : PublishDiagnosticsParams := Id.run do
+  let replace := { next with isIncremental? := some false }
+  let some prev := prev?
+    | return replace
+  if next.isIncremental?.getD false then
+    return { next with
+      diagnostics := prev.diagnostics ++ next.diagnostics
+      isIncremental? := some false }
+  return replace
+
 /--
 Waits for the worker to emit all diagnostic notifications for the current document version and
-returns the last notification, if any.
+returns the accumulated diagnostics, if any.
+
+Incoming notifications are merged using `mergePublishDiagnosticsParams`.
 
 We used to return all notifications but with debouncing in the server, this would not be
 deterministic anymore as what messages are dropped depends on wall-clock timing.
@@ -112,22 +135,25 @@ deterministic anymore as what messages are dropped depends on wall-clock timing.
 partial def collectDiagnostics (waitForDiagnosticsId : RequestID := 0) (target : DocumentUri) (version : Nat)
 : IpcM (Option (Notification PublishDiagnosticsParams)) := do
   writeRequest ⟨waitForDiagnosticsId, "textDocument/waitForDiagnostics", WaitForDiagnosticsParams.mk target version⟩
-  loop
+  loop none
 where
-  loop := do
+  loop (accumulated? : Option PublishDiagnosticsParams) := do
     match (←readMessage) with
     | Message.response id _ =>
-      if id == waitForDiagnosticsId then return none
-      else loop
-    | Message.responseError id _    msg _ =>
+      if id == waitForDiagnosticsId then
+        return accumulated?.map fun p =>
+          ⟨"textDocument/publishDiagnostics", normalizePublishDiagnosticsParams p⟩
+      else loop accumulated?
+    | Message.responseError id _ msg _ =>
       if id == waitForDiagnosticsId then
         throw $ userError s!"Waiting for diagnostics failed: {msg}"
-      else loop
+      else loop accumulated?
     | Message.notification "textDocument/publishDiagnostics" (some param) =>
       match fromJson? (toJson param) with
-      | Except.ok diagnosticParam => return (← loop).getD ⟨"textDocument/publishDiagnostics", normalizePublishDiagnosticsParams diagnosticParam⟩
+      | Except.ok (diagnosticParam : PublishDiagnosticsParams) =>
+        loop (some (mergePublishDiagnosticsParams accumulated? diagnosticParam))
       | Except.error inner => throw $ userError s!"Cannot decode publishDiagnostics parameters\n{inner}"
-    | _ => loop
+    | _ => loop accumulated?
 
 partial def waitForILeans (waitForILeansId : RequestID := 0) (target : DocumentUri) (version : Nat) : IpcM Unit := do
   writeRequest ⟨waitForILeansId, "$/lean/waitForILeans", WaitForILeansParams.mk target version⟩

src/Lean/Server/FileWorker.lean

@@ -77,8 +77,6 @@ def OutputMessage.ofMsg (msg : JsonRpc.Message) : OutputMessage where
   msg? := msg
   serialized := toJson msg |>.compress
 
-open Widget in
-
 structure WorkerContext where
   /-- Synchronized output channel for LSP messages. Notifications for outdated versions are
     discarded on read. -/
@@ -89,10 +87,6 @@ structure WorkerContext where
   -/
   maxDocVersionRef         : IO.Ref Int
   freshRequestIdRef        : IO.Ref Int
-  /--
-  Diagnostics that are included in every single `textDocument/publishDiagnostics` notification.
-  -/
-  stickyDiagnosticsRef     : IO.Ref (Array InteractiveDiagnostic)
   partialHandlersRef       : IO.Ref (Std.TreeMap String PartialHandlerInfo)
   pendingServerRequestsRef : IO.Ref (Std.TreeMap RequestID (IO.Promise (ServerRequestResponse Json)))
   hLog                     : FS.Stream
@@ -208,19 +202,11 @@ This option can only be set on the command line, not in the lakefile or via `set
     diags : Array Widget.InteractiveDiagnostic
   deriving TypeName
 
-  /--
-  Sends a `textDocument/publishDiagnostics` notification to the client that contains the diagnostics
-  in `ctx.stickyDiagnosticsRef` and `doc.diagnosticsRef`.
-  -/
+  /-- Sends a `textDocument/publishDiagnostics` notification to the client. -/
   private def publishDiagnostics (ctx : WorkerContext) (doc : EditableDocumentCore)
       : BaseIO Unit := do
-    let stickyInteractiveDiagnostics ← ctx.stickyDiagnosticsRef.get
-    let docInteractiveDiagnostics ← doc.diagnosticsRef.get
-    let diagnostics :=
-      stickyInteractiveDiagnostics ++ docInteractiveDiagnostics
-      |>.map (·.toDiagnostic)
-    let notification := mkPublishDiagnosticsNotification doc.meta diagnostics
-    ctx.chanOut.sync.send <| .ofMsg notification
+    let supportsIncremental := ctx.initParams.capabilities.incrementalDiagnosticSupport
+    doc.publishDiagnostics supportsIncremental fun notif => ctx.chanOut.sync.send <| .ofMsg notif
 
   open Language in
   /--
@@ -321,7 +307,7 @@ This option can only be set on the command line, not in the lakefile or via `set
             if let some cacheRef := node.element.diagnostics.interactiveDiagsRef? then
               cacheRef.set <| some <| .mk { diags : MemorizedInteractiveDiagnostics }
             pure diags
-        doc.diagnosticsRef.modify (· ++ diags)
+        doc.appendDiagnostics diags
         if (← get).hasBlocked then
           publishDiagnostics ctx doc
 
@@ -463,7 +449,7 @@ section Initialization
     let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
     let maxDocVersionRef ← IO.mkRef 0
     let freshRequestIdRef ← IO.mkRef (0 : Int)
-    let stickyDiagnosticsRef ← IO.mkRef ∅
+    let stickyDiagsRef ← IO.mkRef {}
     let pendingServerRequestsRef ← IO.mkRef ∅
     let chanOut ← mkLspOutputChannel maxDocVersionRef
     let timestamp ← IO.monoMsNow
@@ -493,11 +479,10 @@ section Initialization
       maxDocVersionRef
       freshRequestIdRef
       cmdlineOpts := opts
-      stickyDiagnosticsRef
     }
+    let diagnosticsMutex ← Std.Mutex.new { stickyDiagsRef }
     let doc : EditableDocumentCore := {
-      «meta» := doc, initSnap
-      diagnosticsRef := (← IO.mkRef ∅)
+      «meta» := doc, initSnap, diagnosticsMutex
     }
     let reporterCancelTk ← CancelToken.new
     let reporter ← reportSnapshots ctx doc reporterCancelTk
@@ -578,14 +563,11 @@ section Updates
     modify fun st => { st with pendingRequests := map st.pendingRequests }
 
   /-- Given the new document, updates editable doc state. -/
-  def updateDocument (doc : DocumentMeta) : WorkerM Unit := do
+  def updateDocument («meta» : DocumentMeta) : WorkerM Unit := do
     (← get).reporterCancelTk.set
     let ctx ← read
-    let initSnap ← ctx.processor doc.mkInputContext
-    let doc : EditableDocumentCore := {
-      «meta» := doc, initSnap
-      diagnosticsRef := (← IO.mkRef ∅)
-    }
+    let initSnap ← ctx.processor «meta».mkInputContext
+    let doc ← (← get).doc.update «meta» initSnap
     let reporterCancelTk ← CancelToken.new
     let reporter ← reportSnapshots ctx doc reporterCancelTk
     modify fun st => { st with doc := { doc with reporter }, reporterCancelTk }
@@ -637,18 +619,16 @@ section NotificationHandling
     let ctx ← read
     let s ← get
     let text := s.doc.meta.text
-    let importOutOfDataMessage := .text s!"Imports are out of date and should be rebuilt; \
-      use the \"Restart File\" command in your editor."
+    let importOutOfDateMessage :=
+      .text s!"Imports are out of date and should be rebuilt; \
+        use the \"Restart File\" command in your editor."
     let diagnostic := {
       range      := ⟨⟨0, 0⟩, ⟨1, 0⟩⟩
       fullRange? := some ⟨⟨0, 0⟩, text.utf8PosToLspPos text.source.rawEndPos⟩
       severity?  := DiagnosticSeverity.information
-      message := importOutOfDataMessage
+      message := importOutOfDateMessage
     }
-    ctx.stickyDiagnosticsRef.modify fun stickyDiagnostics =>
-      let stickyDiagnostics := stickyDiagnostics.filter
-        (·.message.stripTags != importOutOfDataMessage.stripTags)
-      stickyDiagnostics.push diagnostic
+    s.doc.appendStickyDiagnostic diagnostic
     publishDiagnostics ctx s.doc.toEditableDocumentCore
 
 def handleRpcRelease (p : Lsp.RpcReleaseParams) : WorkerM Unit := do
@@ -759,19 +739,17 @@ section MessageHandling
 
   open Widget RequestM Language in
   def handleGetInteractiveDiagnosticsRequest
-      (ctx : WorkerContext)
+      (doc : EditableDocument)
       (params : GetInteractiveDiagnosticsParams)
       : RequestM (Array InteractiveDiagnostic) := do
-    let doc ← readDoc
     -- NOTE: always uses latest document (which is the only one we can retrieve diagnostics for);
     -- any race should be temporary as the client should re-request interactive diagnostics when
     -- they receive the non-interactive diagnostics for the new document
-    let stickyDiags ← ctx.stickyDiagnosticsRef.get
-    let diags ← doc.diagnosticsRef.get
+    let allDiags ← doc.collectCurrentDiagnostics
     -- NOTE: does not wait for `lineRange?` to be fully elaborated, which would be problematic with
     -- fine-grained incremental reporting anyway; instead, the client is obligated to resend the
     -- request when the non-interactive diagnostics of this range have changed
-    return (stickyDiags ++ diags).filter fun diag =>
+    return PersistentArray.toArray <| allDiags.filter fun diag =>
       let r := diag.fullRange
       let diagStartLine := r.start.line
       let diagEndLine   :=
@@ -784,7 +762,7 @@ section MessageHandling
         s ≤ diagStartLine ∧ diagStartLine < e ∨
         diagStartLine ≤ s ∧ s < diagEndLine
 
-  def handlePreRequestSpecialCases? (ctx : WorkerContext) (st : WorkerState)
+  def handlePreRequestSpecialCases? (st : WorkerState)
       (id : RequestID) (method : String) (params : Json)
       : RequestM (Option (RequestTask SerializedLspResponse)) := do
     match method with
@@ -795,7 +773,7 @@ section MessageHandling
       let some seshRef := st.rpcSessions.get? params.sessionId
         | throw RequestError.rpcNeedsReconnect
       let params ← RequestM.parseRequestParams Widget.GetInteractiveDiagnosticsParams params.params
-      let resp ← handleGetInteractiveDiagnosticsRequest ctx params
+      let resp ← handleGetInteractiveDiagnosticsRequest st.doc params
       let resp ← seshRef.modifyGet fun st =>
         rpcEncode resp st.objects |>.map (·) ({st with objects := ·})
       return some <| .pure { response? := resp, serialized := resp.compress, isComplete := true }
@@ -925,7 +903,7 @@ section MessageHandling
       serverRequestEmitter := sendUntypedServerRequest ctx
     }
     let requestTask? ← EIO.toIO' <| RequestM.run (rc := rc) do
-      if let some response ← handlePreRequestSpecialCases? ctx st id method params then
+      if let some response ← handlePreRequestSpecialCases? st id method params then
         return response
       let task ← handleLspRequest method params
       let task ← handlePostRequestSpecialCases id method params task

src/Lean/Server/FileWorker/Utils.lean

@@ -10,6 +10,7 @@ prelude
 public import Lean.Language.Lean.Types
 public import Lean.Server.Snapshots
 public import Lean.Server.AsyncList
+public import Std.Sync.Mutex
 
 public section
 
@@ -39,6 +40,26 @@ where
         | some next => .delayed <| next.task.asServerTask.bindCheap go
         | none => .nil)
 
+/--
+Tracks diagnostics and incremental diagnostic reporting state for a single document version.
+
+The sticky diagnostics are shared across all document versions via an `IO.Ref`, while per-version
+diagnostics are stored directly. The whole state is wrapped in a `Std.Mutex` on
+`EditableDocumentCore` to ensure atomic updates.
+-/
+structure DiagnosticsState where
+  /--
+  Diagnostics that persist across document versions (e.g. stale dependency warnings).
+  Shared across all versions via an `IO.Ref`.
+  -/
+  stickyDiagsRef : IO.Ref (PersistentArray Widget.InteractiveDiagnostic)
+  /-- Diagnostics accumulated during snapshot reporting. -/
+  diags : PersistentArray Widget.InteractiveDiagnostic := {}
+  /-- Whether the next `publishDiagnostics` call should be incremental. -/
+  isIncremental : Bool := false
+  /-- Amount of diagnostics reported in `publishDiagnostics` so far. -/
+  publishedDiagsAmount : Nat := 0
+
 /--
 A document bundled with processing information. Turned into `EditableDocument` as soon as the
 reporter task has been started.
@@ -50,11 +71,94 @@ structure EditableDocumentCore where
   initSnap : Language.Lean.InitialSnapshot
   /-- Old representation for backward compatibility. -/
   cmdSnaps : AsyncList IO.Error Snapshot := private_decl% mkCmdSnaps initSnap
-  /--
-  Interactive versions of diagnostics reported so far. Filled by `reportSnapshots` and read by
-  `handleGetInteractiveDiagnosticsRequest`.
-  -/
-  diagnosticsRef : IO.Ref (Array Widget.InteractiveDiagnostic)
+  /-- Per-version diagnostics state, protected by a mutex. -/
+  diagnosticsMutex : Std.Mutex DiagnosticsState
+
+namespace EditableDocumentCore
+open Widget
+
+/-- Appends new non-sticky diagnostics. -/
+def appendDiagnostics (doc : EditableDocumentCore) (diags : Array InteractiveDiagnostic) :
+    BaseIO Unit :=
+  doc.diagnosticsMutex.atomically do
+    modify fun ds => { ds with diags := diags.foldl (init := ds.diags) fun acc d => acc.push d }
+
+/--
+Appends a sticky diagnostic and marks the next publish as non-incremental.
+Removes any existing sticky diagnostic whose `message.stripTags` matches the new one.
+-/
+def appendStickyDiagnostic (doc : EditableDocumentCore) (diagnostic : InteractiveDiagnostic) :
+    BaseIO Unit :=
+  doc.diagnosticsMutex.atomically do
+    let ds ← get
+    ds.stickyDiagsRef.modify fun stickyDiags =>
+      let stickyDiags := stickyDiags.filter
+        (·.message.stripTags != diagnostic.message.stripTags)
+      stickyDiags.push diagnostic
+    set { ds with isIncremental := false }
+
+/-- Returns all current diagnostics (sticky ++ doc). -/
+def collectCurrentDiagnostics (doc : EditableDocumentCore) :
+    BaseIO (PersistentArray InteractiveDiagnostic) :=
+  doc.diagnosticsMutex.atomically do
+    let ds ← get
+    let stickyDiags ← ds.stickyDiagsRef.get
+    return stickyDiags ++ ds.diags
+
+/--
+Creates a new `EditableDocumentCore` for a new document version, sharing the same sticky
+diagnostics with the previous version.
+-/
+def update (doc : EditableDocumentCore) (newMeta : DocumentMeta)
+    (newInitSnap : Language.Lean.InitialSnapshot) : BaseIO EditableDocumentCore := do
+  let stickyDiagsRef ← doc.diagnosticsMutex.atomically do
+    return (← get).stickyDiagsRef
+  let diagnosticsMutex ← Std.Mutex.new { stickyDiagsRef }
+  return { «meta» := newMeta, initSnap := newInitSnap, diagnosticsMutex }
+
+/--
+Collects diagnostics for a `textDocument/publishDiagnostics` notification, updates
+the incremental tracking fields and writes the notification to the client.
+
+When `incrementalDiagnosticSupport` is `true` and the state allows it, sends only
+the newly added diagnostics with `isIncremental? := some true`. Otherwise, sends
+all sticky and non-sticky diagnostics non-incrementally.
+
+The state update and the write are performed atomically under the diagnostics mutex
+to prevent reordering between concurrent publishers (the reporter task and the main thread).
+-/
+def publishDiagnostics (doc : EditableDocumentCore) (incrementalDiagnosticSupport : Bool)
+    (writeDiagnostics : JsonRpc.Notification Lsp.PublishDiagnosticsParams → BaseIO Unit) :
+    BaseIO Unit := do
+  -- The mutex must be held across both the state update and the write to ensure that concurrent
+  -- publishers (e.g. the reporter task and the main thread) cannot interleave their state reads
+  -- and writes, which would reorder incremental/non-incremental messages and corrupt client state.
+  doc.diagnosticsMutex.atomically do
+    let ds ← get
+    let useIncremental := incrementalDiagnosticSupport && ds.isIncremental
+    let stickyDiags ← ds.stickyDiagsRef.get
+    let diags := ds.diags
+    let publishedDiagsAmount := ds.publishedDiagsAmount
+    set <| { ds with publishedDiagsAmount := diags.size, isIncremental := true }
+    let (diagsToSend, isIncremental) :=
+      if useIncremental then
+        let newDiags := diags.foldl (init := #[]) (start := publishedDiagsAmount) fun acc d =>
+          acc.push d.toDiagnostic
+        (newDiags, true)
+      else
+        let allDiags := stickyDiags.foldl (init := #[]) fun acc d =>
+          acc.push d.toDiagnostic
+        let allDiags := diags.foldl (init := allDiags) fun acc d =>
+          acc.push d.toDiagnostic
+        (allDiags, false)
+    let isIncremental? :=
+      if incrementalDiagnosticSupport then
+        some isIncremental
+      else
+        none
+    writeDiagnostics <| mkPublishDiagnosticsNotification doc.meta diagsToSend isIncremental?
+
+end EditableDocumentCore
 
 /-- `EditableDocumentCore` with reporter task. -/
 structure EditableDocument extends EditableDocumentCore where

src/Lean/Server/ProtocolOverview.lean

@@ -152,9 +152,9 @@ def protocolOverview : Array MessageOverview := #[
   .notification {
     method := "textDocument/publishDiagnostics"
     direction := .serverToClient
-    kinds := #[.extendedParameterType #[``PublishDiagnosticsParams.diagnostics, ``DiagnosticWith.fullRange?, ``DiagnosticWith.isSilent?, ``DiagnosticWith.leanTags?]]
+    kinds := #[.extendedParameterType #[``PublishDiagnosticsParams.isIncremental?, ``PublishDiagnosticsParams.diagnostics, ``DiagnosticWith.fullRange?, ``DiagnosticWith.isSilent?, ``DiagnosticWith.leanTags?]]
     parameterType := PublishDiagnosticsParams
-    description := "Emitted by the language server whenever a new set of diagnostics becomes available for a file. Unlike most language servers, the Lean language server emits this notification incrementally while processing the file, not only when the full file has been processed."
+    description := "Emitted by the language server whenever a new set of diagnostics becomes available for a file. Unlike most language servers, the Lean language server emits this notification incrementally while processing the file, not only when the full file has been processed. If the client sets `LeanClientCapabilities.incrementalDiagnosticSupport` and `isIncremental` is `true`, the diagnostics in the notification should be appended to the existing diagnostics for the same document version rather than replacing them."
   },
   .notification {
     method := "$/lean/fileProgress"

src/Lean/Server/Test/Runner.lean

@@ -723,6 +723,7 @@ partial def main (args : List String) : IO Unit := do
         }
       }
       lean? := some {
+        incrementalDiagnosticSupport? := some true
         silentDiagnosticSupport? := some true
         rpcWireFormat? := some .v1
       }

src/Lean/Server/Utils.lean

@@ -133,12 +133,14 @@ def foldDocumentChanges (changes : Array Lsp.TextDocumentContentChangeEvent) (ol
   changes.foldl applyDocumentChange oldText
 
 /-- Constructs a `textDocument/publishDiagnostics` notification. -/
-def mkPublishDiagnosticsNotification (m : DocumentMeta) (diagnostics : Array Lsp.Diagnostic) :
+def mkPublishDiagnosticsNotification (m : DocumentMeta) (diagnostics : Array Lsp.Diagnostic)
+    (isIncremental : Option Bool := none) :
     JsonRpc.Notification Lsp.PublishDiagnosticsParams where
   method := "textDocument/publishDiagnostics"
   param  := {
     uri         := m.uri
     version?    := some m.version
+    isIncremental? := isIncremental
     diagnostics := diagnostics
   }
 

tests/server/diags.lean.content_diag.json

@@ -1,6 +1,7 @@
 {"params":
  {"version": 1,
   "uri": "file:///test.lean",
+  "isIncremental": false,
   "diagnostics":
   [{"source": "Lean 4",
     "severity": 3,

tests/server_interactive/2058.lean.out.expected

@@ -1,5 +1,6 @@
 {"version": 1,
  "uri": "file:///2058.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 1,

tests/server_interactive/4880.lean.out.expected

@@ -1,5 +1,6 @@
 {"version": 1,
  "uri": "file:///4880.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 1,

tests/server_interactive/5659.lean.out.expected

@@ -1,5 +1,6 @@
 {"version": 1,
  "uri": "file:///5659.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 1,

tests/server_interactive/cancellation.lean.out.expected

@@ -3,6 +3,7 @@ cancelled!
 rerun!
 {"version": 2,
  "uri": "file:///cancellation.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 3,
@@ -28,6 +29,7 @@ blocked!
 unblocking!
 {"version": 2,
  "uri": "file:///cancellation.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 1,
@@ -56,6 +58,7 @@ unblocking!
 unblocking!
 {"version": 2,
  "uri": "file:///cancellation.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 1,
@@ -77,6 +80,7 @@ unblocking!
 unblocking!
 {"version": 2,
  "uri": "file:///cancellation.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 1,
@@ -90,6 +94,7 @@ blocked!
 unblocking!
 {"version": 2,
  "uri": "file:///cancellation.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 1,
@@ -119,6 +124,7 @@ blocked!
 cancelled!
 {"version": 2,
  "uri": "file:///cancellation.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 3,
@@ -134,6 +140,7 @@ blocked!
 cancelled!
 {"version": 2,
  "uri": "file:///cancellation.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 3,
@@ -148,6 +155,7 @@ cancelled!
 unblocking!
 {"version": 2,
  "uri": "file:///cancellation.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 1,
@@ -161,6 +169,7 @@ blocked!
 cancelled!
 {"version": 2,
  "uri": "file:///cancellation.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 3,
@@ -176,6 +185,7 @@ blocked!
 cancelled!
 {"version": 2,
  "uri": "file:///cancellation.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 3,
@@ -191,6 +201,7 @@ blocked!
 cancelled!
 {"version": 2,
  "uri": "file:///cancellation.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 3,
@@ -206,6 +217,7 @@ blocked!
 cancelled!
 {"version": 2,
  "uri": "file:///cancellation.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 3,
@@ -218,4 +230,7 @@ cancelled!
    {"start": {"line": 6, "character": 0},
     "end": {"line": 13, "character": 10}}}]}
 cancelled!
-{"version": 2, "uri": "file:///cancellation.lean", "diagnostics": []}
+{"version": 2,
+ "uri": "file:///cancellation.lean",
+ "isIncremental": false,
+ "diagnostics": []}

tests/server_interactive/editAfterError.lean.out.expected

@@ -1,5 +1,6 @@
 {"version": 2,
  "uri": "file:///editAfterError.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 1,

tests/server_interactive/goalsAccomplished.lean.out.expected

@@ -1,5 +1,6 @@
 {"version": 1,
  "uri": "file:///goalsAccomplished.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 3,

tests/server_interactive/haveInfo.lean.out.expected

@@ -1,5 +1,6 @@
 {"version": 1,
  "uri": "file:///haveInfo.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 1,

tests/server_interactive/highlightMatches.lean.out.expected

@@ -1,5 +1,6 @@
 {"version": 1,
  "uri": "file:///highlightMatches.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 3,

tests/server_interactive/incrementalCombinator.lean.out.expected

@@ -4,6 +4,7 @@ c 2
 c 2.5
 {"version": 2,
  "uri": "file:///incrementalCombinator.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 2,
@@ -27,6 +28,7 @@ h 3
 sh
 {"version": 1,
  "uri": "file:///incrementalCombinator.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 1,
@@ -49,6 +51,7 @@ sh
 sh
 {"version": 2,
  "uri": "file:///incrementalCombinator.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 1,
@@ -76,6 +79,7 @@ i 1
 i 1.5
 {"version": 2,
  "uri": "file:///incrementalCombinator.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 3,
@@ -89,6 +93,7 @@ i 1.5
     "end": {"line": 6, "character": 18}}}]}
 {"version": 2,
  "uri": "file:///incrementalCombinator.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 2,

tests/server_interactive/incrementalCommand.lean.out.expected

@@ -1,10 +1,20 @@
-{"version": 2, "uri": "file:///incrementalCommand.lean", "diagnostics": []}
-{"version": 2, "uri": "file:///incrementalCommand.lean", "diagnostics": []}
+{"version": 2,
+ "uri": "file:///incrementalCommand.lean",
+ "isIncremental": false,
+ "diagnostics": []}
+{"version": 2,
+ "uri": "file:///incrementalCommand.lean",
+ "isIncremental": false,
+ "diagnostics": []}
 w
 w
-{"version": 1, "uri": "file:///incrementalCommand.lean", "diagnostics": []}
 {"version": 1,
  "uri": "file:///incrementalCommand.lean",
+ "isIncremental": false,
+ "diagnostics": []}
+{"version": 1,
+ "uri": "file:///incrementalCommand.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 3,
@@ -15,6 +25,7 @@ w
    {"start": {"line": 5, "character": 0}, "end": {"line": 5, "character": 5}}}]}
 {"version": 2,
  "uri": "file:///incrementalCommand.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 3,
@@ -25,6 +36,7 @@ w
    {"start": {"line": 5, "character": 0}, "end": {"line": 5, "character": 5}}}]}
 {"version": 2,
  "uri": "file:///incrementalCommand.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 1,
@@ -33,5 +45,11 @@ w
    "message": "Tactic `assumption` failed\n\n⊢ False",
    "fullRange":
    {"start": {"line": 2, "character": 2}, "end": {"line": 2, "character": 9}}}]}
-{"version": 3, "uri": "file:///incrementalCommand.lean", "diagnostics": []}
-{"version": 2, "uri": "file:///incrementalCommand.lean", "diagnostics": []}
+{"version": 3,
+ "uri": "file:///incrementalCommand.lean",
+ "isIncremental": false,
+ "diagnostics": []}
+{"version": 2,
+ "uri": "file:///incrementalCommand.lean",
+ "isIncremental": false,
+ "diagnostics": []}

tests/server_interactive/incrementalInduction.lean.out.expected

@@ -39,6 +39,7 @@ c 2
 c 2.5
 {"version": 1,
  "uri": "file:///incrementalInduction.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 1,

tests/server_interactive/incrementalMutual.lean.out.expected

@@ -17,8 +17,14 @@ h 1 1
 h 1 0.5
 h 0 1
 h 1 1
-{"version": 1, "uri": "file:///incrementalMutual.lean", "diagnostics": []}
-{"version": 2, "uri": "file:///incrementalMutual.lean", "diagnostics": []}
+{"version": 1,
+ "uri": "file:///incrementalMutual.lean",
+ "isIncremental": false,
+ "diagnostics": []}
+{"version": 2,
+ "uri": "file:///incrementalMutual.lean",
+ "isIncremental": false,
+ "diagnostics": []}
 ns 0
 ns 1
 ns 1.5
@@ -31,6 +37,7 @@ so 1
 so 1.5
 {"version": 2,
  "uri": "file:///incrementalMutual.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 1,

tests/server_interactive/incrementalTactic.lean.out.expected

@@ -8,6 +8,7 @@ t 2
 t 2
 {"version": 3,
  "uri": "file:///incrementalTactic.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 1,
@@ -29,6 +30,7 @@ t 2
     "end": {"line": 4, "character": 13}}}]}
 {"version": 1,
  "uri": "file:///incrementalTactic.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 1,
@@ -40,6 +42,7 @@ t 2
     "end": {"line": 4, "character": 3}}}]}
 {"version": 1,
  "uri": "file:///incrementalTactic.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 1,
@@ -70,6 +73,7 @@ s
    "ctx": {"__rpcref": "1"}}]}
 {"version": 1,
  "uri": "file:///incrementalTactic.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 1,
@@ -82,6 +86,7 @@ s
     "end": {"line": 2, "character": 25}}}]}
 {"version": 1,
  "uri": "file:///incrementalTactic.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 1,
@@ -94,6 +99,7 @@ s
     "end": {"line": 3, "character": 16}}}]}
 {"version": 2,
  "uri": "file:///incrementalTactic.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 1,
@@ -119,6 +125,7 @@ s
    {"start": {"line": 4, "character": 2}, "end": {"line": 4, "character": 8}}}]}
 {"version": 2,
  "uri": "file:///incrementalTactic.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 1,

tests/server_interactive/inlayHints.lean.out.expected

@@ -1,5 +1,6 @@
 {"version": 1,
  "uri": "file:///inlayHints.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 1,

tests/server_interactive/interactiveDiagnostics.lean.out.expected

@@ -1,5 +1,6 @@
 {"version": 1,
  "uri": "file:///interactiveDiagnostics.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 2,

tests/server_interactive/interactiveTraces.lean.out.expected

@@ -1,5 +1,6 @@
 {"version": 1,
  "uri": "file:///interactiveTraces.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 3,

tests/server_interactive/issue4527.lean.out.expected

@@ -1,5 +1,6 @@
 {"version": 1,
  "uri": "file:///issue4527.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 1,

tests/server_interactive/semanticTokens.lean.out.expected

@@ -1,5 +1,6 @@
 {"version": 1,
  "uri": "file:///semanticTokens.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 3,

tests/server_interactive/semanticTokensVersoDocs.lean.out.expected

@@ -1,4 +1,7 @@
-{"version": 1, "uri": "file:///semanticTokensVersoDocs.lean", "diagnostics": []}
+{"version": 1,
+ "uri": "file:///semanticTokensVersoDocs.lean",
+ "isIncremental": false,
+ "diagnostics": []}
 {"textDocument": {"uri": "file:///semanticTokensVersoDocs.lean"},
  "position": {"line": 35, "character": 2}}
 {"data":

tests/server_interactive/strInterpSynthError.lean.out.expected

@@ -1,5 +1,6 @@
 {"version": 1,
  "uri": "file:///strInterpSynthError.lean",
+ "isIncremental": false,
  "diagnostics":
  [{"source": "Lean 4",
    "severity": 1,

tests/server_interactive/unterminatedDocComment.lean.out.expected

@@ -1 +1,4 @@
-{"version": 2, "uri": "file:///unterminatedDocComment.lean", "diagnostics": []}
+{"version": 2,
+ "uri": "file:///unterminatedDocComment.lean",
+ "isIncremental": false,
+ "diagnostics": []}