feat: client-side support for incremental diagnostics

Author: mhuisi

vscode-lean4/src/diagnostics.ts

@@ -0,0 +1,94 @@
+import { DiagnosticCollection, Disposable, EventEmitter } from 'vscode'
+import { LeanDiagnostic, LeanPublishDiagnosticsParams, p2cConverter } from './utils/converters'
+import { DocumentUri } from 'vscode-languageserver-protocol'
+
+export type DiagnosticChangeKind = 'replace' | 'append'
+
+export class DiagnosticChangeEvent {
+    readonly kind: DiagnosticChangeKind
+    readonly params: LeanPublishDiagnosticsParams
+    private readonly accumulated: LeanDiagnostic[]
+    private readonly amountAccumulated: number
+
+    constructor(kind: DiagnosticChangeKind, params: LeanPublishDiagnosticsParams, accumulated: LeanDiagnostic[]) {
+        this.kind = kind
+        this.params = params
+        this.accumulated = accumulated
+        this.amountAccumulated = accumulated.length
+    }
+
+    private accumulatedDiagnostics(): LeanDiagnostic[] {
+        return this.accumulated.slice(0, this.amountAccumulated)
+    }
+
+    accumulatedParams(): LeanPublishDiagnosticsParams {
+        return { ...this.params, diagnostics: this.accumulatedDiagnostics() }
+    }
+}
+
+export class LeanClientDiagnosticCollection implements Disposable {
+    readonly vsCodeCollection: DiagnosticCollection
+    private diags: Map<DocumentUri, LeanPublishDiagnosticsParams> = new Map()
+
+    private diagnosticsChangedEmitter = new EventEmitter<DiagnosticChangeEvent>()
+    onDidChangeDiagnostics = this.diagnosticsChangedEmitter.event
+
+    constructor(vsCodeCollection: DiagnosticCollection) {
+        this.vsCodeCollection = vsCodeCollection
+    }
+
+    private static determineChangeKind(
+        prev: LeanPublishDiagnosticsParams | undefined,
+        next: LeanPublishDiagnosticsParams,
+    ): DiagnosticChangeKind | 'drop' {
+        if (prev === undefined) {
+            return 'replace'
+        }
+        if (next.version === undefined || prev.version === undefined) {
+            return 'replace'
+        }
+        if (next.version > prev.version) {
+            return 'replace'
+        }
+        if (next.version < prev.version) {
+            return 'drop'
+        }
+        if (!next.isIncremental) {
+            return 'replace'
+        }
+        return 'append'
+    }
+
+    publishDiagnostics(params: LeanPublishDiagnosticsParams): void {
+        const prev = this.diags.get(params.uri)
+        const kind = LeanClientDiagnosticCollection.determineChangeKind(prev, params)
+        if (kind === 'drop') {
+            return
+        }
+
+        let accumulated: LeanDiagnostic[]
+        if (kind === 'append') {
+            accumulated = prev!.diagnostics
+            accumulated.push(...params.diagnostics)
+        } else {
+            accumulated = [...params.diagnostics]
+        }
+
+        const accumulatedParams = { ...params, diagnostics: accumulated }
+
+        this.diags.set(accumulatedParams.uri, accumulatedParams)
+        void this.syncToCollection(accumulatedParams)
+        this.diagnosticsChangedEmitter.fire(new DiagnosticChangeEvent(kind, params, accumulated))
+    }
+
+    private async syncToCollection(p: LeanPublishDiagnosticsParams): Promise<void> {
+        const nonSilent = p.diagnostics.filter(d => !d.isSilent)
+        const uri = p2cConverter.asUri(p.uri)
+        const vsCodeDiags = await p2cConverter.asDiagnostics(nonSilent)
+        this.vsCodeCollection.set(uri, vsCodeDiags)
+    }
+
+    dispose(): void {
+        this.diagnosticsChangedEmitter.dispose()
+    }
+}

vscode-lean4/src/leanclient.ts

@@ -4,6 +4,7 @@ import {
     Disposable,
     EventEmitter,
     FileSystemWatcher,
+    languages,
     OutputChannel,
     Progress,
     ProgressLocation,
@@ -32,7 +33,6 @@ import {
 } from 'vscode-languageclient/node'
 
 import {
-    LeanDiagnostic,
     LeanFileProgressParams,
     LeanFileProgressProcessingInfo,
     LeanServerCapabilities,
@@ -52,6 +52,7 @@ import { logger } from './utils/logger'
 import * as fs from 'fs'
 import { glob } from 'glob'
 import { SemVer } from 'semver'
+import { DiagnosticChangeEvent, LeanClientDiagnosticCollection } from './diagnostics'
 import { formatCommandExecutionOutput } from './utils/batch'
 import {
     c2pConverter,
@@ -98,11 +99,13 @@ function logConfig(): LogConfig | undefined {
 }
 
 interface LeanClientCapabilties {
+    incrementalDiagnosticSupport?: boolean
     silentDiagnosticSupport?: boolean
     rpcWireFormat?: RpcWireFormat
 }
 
 const leanClientCapabilities: LeanClientCapabilties = {
+    incrementalDiagnosticSupport: true,
     silentDiagnosticSupport: true,
     rpcWireFormat: 'v1'
 }
@@ -140,6 +143,8 @@ export class LeanClient implements Disposable {
     private didChangeEmitter = new EventEmitter<DidChangeTextDocumentParams>()
     didChange = this.didChangeEmitter.event
 
+    private diagnosticCollection: LeanClientDiagnosticCollection | undefined
+
     private diagnosticsEmitter = new EventEmitter<LeanPublishDiagnosticsParams>()
     diagnostics = this.diagnosticsEmitter.event
 
@@ -540,7 +545,18 @@ export class LeanClient implements Disposable {
                     }
                 }
             })
+            this.diagnosticCollection?.dispose()
+            const vsCodeCollection = languages.createDiagnosticCollection('lean4')
+            this.diagnosticCollection = new LeanClientDiagnosticCollection(vsCodeCollection)
+            this.diagnosticCollection.onDidChangeDiagnostics((e: DiagnosticChangeEvent) => {
+                this.diagnosticsEmitter.fire(e.accumulatedParams())
+            })
+            this.client.onNotification('textDocument/publishDiagnostics', (params: LeanPublishDiagnosticsParams) => {
+                this.diagnosticCollection?.publishDiagnostics(params)
+            })
+
             await this.client.start()
+
             const version = this.client.initializeResult?.serverInfo?.version
             if (version && new SemVer(version).compare('0.2.0') < 0) {
                 if (this.staleDepNotifier) {
@@ -708,6 +724,9 @@ export class LeanClient implements Disposable {
 
         this.noPrompt = false
         this.progress = new Map()
+        this.diagnosticCollection?.vsCodeCollection.dispose()
+        this.diagnosticCollection?.dispose()
+        this.diagnosticCollection = undefined
         this.client = undefined
         this.openServerDocuments = new Set()
         this.running = false
@@ -779,7 +798,7 @@ export class LeanClient implements Disposable {
     }
 
     getDiagnostics(): DiagnosticCollection | undefined {
-        return this.running ? this.client?.diagnostics : undefined
+        return this.running ? this.diagnosticCollection?.vsCodeCollection : undefined
     }
 
     get initializeResult(): InitializeResult | undefined {
@@ -873,18 +892,11 @@ export class LeanClient implements Disposable {
                     }
                     return next(type, param)
                 },
-                handleDiagnostics: (uri, diagnostics, next) => {
-                    const diagnosticsInVsCode = diagnostics.filter(d => !('isSilent' in d && d.isSilent))
-                    next(uri, diagnosticsInVsCode)
-                    const uri_ = c2pConverter.asUri(uri)
-                    const diagnostics_: LeanDiagnostic[] = []
-                    for (const d of diagnostics) {
-                        const d_: LeanDiagnostic = {
-                            ...c2pConverter.asDiagnostic(d),
-                        }
-                        diagnostics_.push(d_)
-                    }
-                    this.diagnosticsEmitter.fire({ uri: uri_, diagnostics: diagnostics_ })
+                handleDiagnostics: () => {
+                    // Suppress the default diagnostics handling by the LanguageClient.
+                    // We handle diagnostics ourselves via a custom notification handler
+                    // so that we can access the full LeanPublishDiagnosticsParams
+                    // (including version and isIncremental).
                 },
 
                 didOpen: async (doc, next) => {

vscode-lean4/src/utils/converters.ts

@@ -32,6 +32,7 @@ export interface LeanDiagnostic extends ls.Diagnostic {
 export interface LeanPublishDiagnosticsParams {
     uri: ls.DocumentUri
     version?: ls.integer
+    isIncremental?: boolean
     diagnostics: LeanDiagnostic[]
 }