feat: nested lean projects

vscode-lean4/package.json

@@ -65,11 +65,6 @@
                     "default": true,
                     "markdownDescription": "Enable eager replacement of abbreviations that uniquely identify a symbol."
                 },
-                "lean4.fallBackToStringOccurrenceHighlighting": {
-                    "type": "boolean",
-                    "description": "Fall back to string-based occurrence highlighting when there are no semantic symbol occurrences from the Lean language server to highlight.",
-                    "default": false
-                },
                 "lean4.automaticallyBuildDependencies": {
                     "type": "boolean",
                     "default": false,
@@ -1775,7 +1770,7 @@
         "markdown-it": "^14.1.0",
         "markdown-it-anchor": "^9.0.1",
         "semver": "^7.6.0",
-        "vscode-languageclient": "^8.0.2",
+        "vscode-languageclient": "^9.0.1",
         "zod": "^3.22.4"
     },
     "devDependencies": {

vscode-lean4/src/config.ts

@@ -173,10 +173,6 @@ export function shouldShowSetupWarnings(): boolean {
     return workspace.getConfiguration('lean4').get('showSetupWarnings', true)
 }
 
-export function getFallBackToStringOccurrenceHighlighting(): boolean {
-    return workspace.getConfiguration('lean4').get('fallBackToStringOccurrenceHighlighting', false)
-}
-
 export function showDiagnosticGutterDecorations(): boolean {
     return workspace.getConfiguration('lean4').get('showDiagnosticGutterDecorations', true)
 }

vscode-lean4/src/diagnostics/setupDiagnostics.ts

@@ -34,22 +34,6 @@ const ancientLean4ProjectWarningMessage = (origin: string, projectVersion: SemVe
     `${origin} is using a Lean 4 version (${projectVersion.toString()}) from before the first Lean 4 stable release (4.0.0).
 Pre-stable Lean 4 versions are increasingly less supported, so please consider updating to a newer Lean 4 version.`
 
-const oldServerFolderContainsNewServerFolderErrorMessage = (
-    folderUri: FileUri,
-    fileUri: FileUri,
-    clientFolderUri: FileUri,
-) =>
-    `Error while starting language server: The project at '${folderUri.fsPath}' of the file '${fileUri.baseName()}' is contained inside of another project at '${clientFolderUri.fsPath}', for which a language server is already running.
-The Lean 4 VS Code extension does not support nested Lean projects.`
-
-const newServerFolderContainsOldServerFolderErrorMessage = (
-    folderUri: FileUri,
-    fileUri: FileUri,
-    clientFolderUri: FileUri,
-) =>
-    `Error while starting language server: The project at '${folderUri.fsPath}' of the file '${fileUri.baseName()}' contains another project at '${clientFolderUri.fsPath}', for which a language server is already running.
-The Lean 4 VS Code extension does not support nested Lean projects.`
-
 export class SetupDiagnostics {
     private n: SetupNotifier
 
@@ -180,56 +164,6 @@ export class SetupDiagnostics {
         }
     }
 
-    async checkIsNestedProjectFolder(
-        existingFolderUris: ExtUri[],
-        folderUri: ExtUri,
-        fileUri: ExtUri,
-        stopOtherServer: (folderUri: FileUri) => Promise<void>,
-    ): Promise<PreconditionCheckResult> {
-        if (folderUri.scheme === 'untitled' || fileUri.scheme === 'untitled') {
-            if (existingFolderUris.some(existingFolderUri => existingFolderUri.scheme === 'untitled')) {
-                await displayInternalError(
-                    'starting language server',
-                    'Attempting to start new untitled language server while one already exists.',
-                )
-                return 'Fatal'
-            }
-            return 'Fulfilled'
-        }
-
-        for (const existingFolderUri of existingFolderUris) {
-            if (existingFolderUri.scheme !== 'file') {
-                continue
-            }
-            if (existingFolderUri.isInFolder(folderUri)) {
-                return await this.n.displaySetupErrorWithInput(
-                    newServerFolderContainsOldServerFolderErrorMessage(folderUri, fileUri, existingFolderUri),
-                    [
-                        {
-                            input: 'Stop Other Server',
-                            continueDisplaying: false,
-                            action: () => stopOtherServer(existingFolderUri),
-                        },
-                    ],
-                )
-            }
-            if (folderUri.isInFolder(existingFolderUri)) {
-                return await this.n.displaySetupErrorWithInput(
-                    oldServerFolderContainsNewServerFolderErrorMessage(folderUri, fileUri, existingFolderUri),
-                    [
-                        {
-                            input: 'Stop Other Server',
-                            continueDisplaying: false,
-                            action: () => stopOtherServer(existingFolderUri),
-                        },
-                    ],
-                )
-            }
-        }
-
-        return 'Fulfilled'
-    }
-
     async checkIsLeanVersionUpToDate(
         channel: OutputChannel,
         context: string,

vscode-lean4/src/leanclient.ts

@@ -25,6 +25,8 @@ import {
     InitializeResult,
     LanguageClient,
     LanguageClientOptions,
+    LSPErrorCodes,
+    ResponseError,
     RevealOutputChannelOn,
     ServerCapabilities,
     State,
@@ -41,7 +43,6 @@ import {
 import {
     allowedLoggingMethods,
     disallowedLoggingMethods,
-    getFallBackToStringOccurrenceHighlighting,
     isLoggingEnabled,
     loggingDir,
     serverArgs,
@@ -50,6 +51,7 @@ import {
 import { logger } from './utils/logger'
 // @ts-ignore
 import * as fs from 'fs'
+import { glob } from 'glob'
 import { SemVer } from 'semver'
 import { formatCommandExecutionOutput } from './utils/batch'
 import {
@@ -126,6 +128,7 @@ export class LeanClient implements Disposable {
     private client: LanguageClient | undefined
     private outputChannel: OutputChannel
     folderUri: ExtUri
+    private subFolderExclusions: FileUri[] | undefined
     private subscriptions: Disposable[] = []
     private noPrompt: boolean = false
     private showingRestartMessage: boolean = false
@@ -178,9 +181,49 @@ export class LeanClient implements Disposable {
         c.folderUri = folderUri
         c.subscriptions.push(new Disposable(() => c.staleDepNotifier?.dispose()))
         await c.registerRestartServerNotificationWatchers()
+        if (folderUri.scheme === 'file') {
+            // All nested inner projects are excluded from this project so that we do not
+            // get duplicate language server output for files in a nested inner project.
+            const excludedToolchainPaths = await glob('**/lean-toolchain', {
+                cwd: folderUri.fsPath,
+                // TODO for configurable `.lake/packages`: Run `lake update` if no manifest exists, parse the manifest, grab the packages directory from it
+                ignore: ['lean-toolchain', '.lake/packages/**'],
+                dot: true,
+                absolute: true,
+            })
+            const excludedFolderUris = excludedToolchainPaths
+                .map(t => new FileUri(t).join('..'))
+            c.subFolderExclusions = excludedFolderUris
+        }
         return c
     }
 
+    private isExcluded(uri: FileUri): boolean {
+        if (this.subFolderExclusions === undefined) {
+            return false
+        }
+        return this.subFolderExclusions.some(excludedFolderUri => uri.isInFolder(excludedFolderUri))
+    }
+
+    private isParamExcluded<P>(param: P | undefined): boolean {
+        if (typeof param !== 'object' || param === null) {
+            return false
+        }
+        let docUri: ExtUri | undefined
+        if ('uri' in param) {
+            docUri = parseExtUri(param.uri as string)
+        } else if ('textDocument' in param) {
+            const doc = param.textDocument as any
+            if ('uri' in doc) {
+                docUri = parseExtUri(doc.uri as string)
+            }
+        }
+        if (docUri === undefined || docUri.scheme !== 'file') {
+            return false
+        }
+        return this.isExcluded(docUri)
+    }
+
     private async updateConfigFileContents(uri: FileUri): Promise<boolean> {
         let contents: string
         try {
@@ -779,6 +822,8 @@ export class LeanClient implements Disposable {
     }
 
     private obtainClientOptions(): LanguageClientOptions {
+        // TODO for configurable `.lake/packages`:
+        // Run `lake update` if no manifest exists, parse the manifest, grab the packages directory from it and add a selector for it
         const documentSelector: DocumentFilter = {
             language: 'lean4',
         }
@@ -809,6 +854,27 @@ export class LeanClient implements Disposable {
                 cancellationStrategy: undefined as any,
             },
             middleware: {
+                sendRequest: async (type, param, token, next) => {
+                    if (this.isParamExcluded(param)) {
+                        // Major HACK:
+                        // We can't return a value here to make the language client library reject the request,
+                        // but throwing a `ContentModified` exception achieves the same thing:
+                        // the language client library ensures that a default value is returned when this exception occurs and for all request handlers,
+                        // VS Code ignores the handler that returned the default value and tries other ones.
+                        throw new ResponseError(LSPErrorCodes.ContentModified, '')
+                    }
+                    return next(type, param, token)
+                },
+                sendNotification: async (type, next, param) => {
+                    // We also have to repeat this check in all other notification middlewares
+                    // so that these middlewares don't produce any side-effects when this
+                    // check here ends up filtering the notification
+                    // (which we can't tell in the other notification middlewares above this one)
+                    if (this.isParamExcluded(param)) {
+                        return
+                    }
+                    return next(type, param)
+                },
                 handleDiagnostics: (uri, diagnostics, next) => {
                     const diagnosticsInVsCode = diagnostics.filter(d => !('isSilent' in d && d.isSilent))
                     next(uri, diagnosticsInVsCode)
@@ -824,6 +890,10 @@ export class LeanClient implements Disposable {
                 },
 
                 didOpen: async (doc, next) => {
+                    const params = c2pConverter.asOpenTextDocumentParams(doc)
+                    if (this.isParamExcluded(params)) {
+                        return
+                    }
                     const docUri = toExtUri(doc.uri)
                     if (!docUri) {
                         return // This should never happen since the glob we launch the client for ensures that all uris are ext uris
@@ -847,16 +917,23 @@ export class LeanClient implements Disposable {
                 },
 
                 didChange: async (data, next) => {
-                    await next(data)
                     const params = c2pConverter.asChangeTextDocumentParams(
                         data,
                         data.document.uri,
                         data.document.version,
                     )
+                    if (this.isParamExcluded(params)) {
+                        return
+                    }
+                    await next(data)
                     this.didChangeEmitter.fire(params)
                 },
 
                 didClose: async (doc, next) => {
+                    const params = c2pConverter.asCloseTextDocumentParams(doc)
+                    if (this.isParamExcluded(params)) {
+                        return
+                    }
                     const docUri = toExtUri(doc.uri)
                     if (!docUri) {
                         return // This should never happen since the glob we launch the client for ensures that all uris are ext uris
@@ -870,42 +947,9 @@ export class LeanClient implements Disposable {
 
                     await next(doc)
 
-                    const params = c2pConverter.asCloseTextDocumentParams(doc)
                     this.didCloseEmitter.fire(params)
                 },
 
-                provideDocumentHighlights: async (doc, pos, ctok, next) => {
-                    const leanHighlights = await next(doc, pos, ctok)
-                    if (leanHighlights?.length) return leanHighlights
-
-                    // vscode doesn't fall back to textual highlights, so we
-                    // need to do that manually if the user asked for it
-                    if (!getFallBackToStringOccurrenceHighlighting()) {
-                        return []
-                    }
-
-                    await new Promise(res => setTimeout(res, 250))
-                    if (ctok.isCancellationRequested) return
-
-                    const wordRange = doc.getWordRangeAtPosition(pos)
-                    if (!wordRange) return
-                    const word = doc.getText(wordRange)
-
-                    const highlights: DocumentHighlight[] = []
-                    const text = doc.getText()
-                    const nonWordPattern = '[`~@$%^&*()-=+\\[{\\]}⟨⟩⦃⦄⟦⟧⟮⟯‹›\\\\|;:",./\\s]|^|$'
-                    const regexp = new RegExp(`(?<=${nonWordPattern})${escapeRegExp(word)}(?=${nonWordPattern})`, 'g')
-                    for (const match of text.matchAll(regexp)) {
-                        const start = doc.positionAt(match.index ?? 0)
-                        highlights.push({
-                            range: new Range(start, start.translate(0, match[0].length)),
-                            kind: DocumentHighlightKind.Text,
-                        })
-                    }
-
-                    return highlights
-                },
-
                 provideRenameEdits: async (document, position, newName, token, next) => {
                     const edit = await next(document, position, newName, token)
                     if (!edit) {
@@ -947,7 +991,7 @@ export class LeanClient implements Disposable {
             fillClientCapabilities(capabilities: ClientCapabilities & { lean?: LeanClientCapabilties | undefined }) {
                 capabilities.lean = leanClientCapabilities
             },
-            dispose() {},
+            clear() {},
         }
         client.registerFeature(leanCapabilityFeature)