feat: errors for nested projects (#607)

mhuisi · web-flow · commit c1d143d5cac8 · 2025-04-15T10:09:31.000+02:00
This PR makes the following adjustments:
- Fix a potential bug where nested workspace folders could lead to
nested language servers (i.e. in core)
- Improve error reporting for nested language servers
- Improve error reporting for the 'Restart File' command
diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json
@@ -231,13 +231,13 @@
                 "command": "lean4.restartServer",
                 "category": "Lean 4",
                 "title": "Server: Restart Server",
-                "description": "Restart the Lean server (for all files)."
+                "description": "Restarts the Lean server (for all files)."
             },
             {
                 "command": "lean4.stopServer",
                 "category": "Lean 4",
                 "title": "Server: Stop Server",
-                "description": "Stop the Lean server (for all files)."
+                "description": "Stops the Lean server (for all files)."
             },
             {
                 "command": "lean4.restartFile",
diff --git a/vscode-lean4/src/diagnostics/setupDiagnostics.ts b/vscode-lean4/src/diagnostics/setupDiagnostics.ts
@@ -1,6 +1,8 @@
+import path from 'path'
 import { SemVer } from 'semver'
 import { OutputChannel, commands } from 'vscode'
 import { ExtUri, FileUri, extUriToCwdUri } from '../utils/exturi'
+import { displayInternalError } from '../utils/internalErrors'
 import { ToolchainUpdateMode } from '../utils/leanCmdRunner'
 import { LeanInstaller } from '../utils/leanInstaller'
 import { diagnose } from './setupDiagnoser'
@@ -32,6 +34,22 @@ 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 '${path.basename(fileUri.fsPath)}' 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 '${path.basename(fileUri.fsPath)}' 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
 
@@ -163,6 +181,56 @@ 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,
diff --git a/vscode-lean4/src/leanclient.ts b/vscode-lean4/src/leanclient.ts
@@ -471,14 +471,32 @@ export class LeanClient implements Disposable {
     }
 
     async restartFile(leanDoc: LeanDocument): Promise<void> {
-        if (this.client === undefined || !this.running) return // there was a problem starting lean server.
+        const extUri = leanDoc.extUri
+        const formattedFileName = extUri.scheme === 'file' ? path.basename(extUri.fsPath) : extUri.toString()
+        const formattedProjectName =
+            this.folderUri.scheme === 'file' ? this.folderUri.fsPath : this.folderUri.toString()
+        if (this.client === undefined || !this.running) {
+            displayNotification(
+                'Error',
+                `Cannot restart '${formattedFileName}': The language server for the project at '${formattedProjectName}' is stopped.`,
+            )
+            return
+        }
 
-        if (!this.isInFolderManagedByThisClient(leanDoc.extUri)) {
+        if (!this.isInFolderManagedByThisClient(extUri)) {
+            displayNotification(
+                'Error',
+                `Cannot restart '${formattedFileName}': The project at '${formattedProjectName}' does not contain the file.`,
+            )
             return
         }
 
-        const uri = leanDoc.extUri.toString()
+        const uri = extUri.toString()
         if (!this.openServerDocuments.delete(uri)) {
+            displayNotification(
+                'Error',
+                `Cannot restart '${formattedFileName}': The file has never been opened in the language server for the project at '${formattedProjectName}'.`,
+            )
             return
         }
         logger.log(`[LeanClient] Restarting File: ${uri}`)
@@ -488,6 +506,10 @@ export class LeanClient implements Disposable {
         )
 
         if (this.openServerDocuments.has(uri)) {
+            displayNotification(
+                'Error',
+                `Cannot restart '${formattedFileName}': The file has already been opened in the language server for the project at '${formattedProjectName}' since initiating the restart.`,
+            )
             return
         }
         this.openServerDocuments.add(uri)
diff --git a/vscode-lean4/src/utils/clientProvider.ts b/vscode-lean4/src/utils/clientProvider.ts
@@ -1,11 +1,11 @@
 import { LeanFileProgressProcessingInfo, ServerStoppedReason } from '@leanprover/infoview-api'
 import path from 'path'
-import { Disposable, EventEmitter, OutputChannel, commands, workspace } from 'vscode'
+import { Disposable, EventEmitter, OutputChannel, commands } from 'vscode'
 import { SetupDiagnostics, checkAll } from '../diagnostics/setupDiagnostics'
 import { PreconditionCheckResult, SetupNotificationOptions } from '../diagnostics/setupNotifs'
 import { LeanClient } from '../leanclient'
 import { LeanPublishDiagnosticsParams } from './converters'
-import { ExtUri, FileUri, UntitledUri, getWorkspaceFolderUri } from './exturi'
+import { ExtUri, FileUri, UntitledUri } from './exturi'
 import { lean } from './leanEditorProvider'
 import { LeanInstaller } from './leanInstaller'
 import { logger } from './logger'
@@ -15,7 +15,10 @@ import { findLeanProjectRoot, willUseLakeServer } from './projectInfo'
 async function checkLean4ProjectPreconditions(
     channel: OutputChannel,
     context: string,
+    existingFolderUris: ExtUri[],
     folderUri: ExtUri,
+    fileUri: ExtUri,
+    stopOtherServer: (folderUri: FileUri) => Promise<void>,
 ): Promise<PreconditionCheckResult> {
     const options: SetupNotificationOptions = {
         errorMode: { mode: 'NonModal' },
@@ -33,6 +36,7 @@ async function checkLean4ProjectPreconditions(
                 toolchainUpdateMode: 'PromptAboutUpdate',
             })
         },
+        () => d.checkIsNestedProjectFolder(existingFolderUris, folderUri, fileUri, stopOtherServer),
     )
 }
 
@@ -84,29 +88,10 @@ export class LeanClientProvider implements Disposable {
             commands.registerCommand('lean4.restartFile', () => this.restartActiveFile()),
             commands.registerCommand('lean4.refreshFileDependencies', () => this.restartActiveFile()),
             commands.registerCommand('lean4.restartServer', () => this.restartActiveClient()),
-            commands.registerCommand('lean4.stopServer', () => this.stopActiveClient()),
+            commands.registerCommand('lean4.stopServer', () => this.stopClient(undefined)),
         )
 
         this.subscriptions.push(lean.onDidOpenLeanDocument(document => this.ensureClient(document.extUri)))
-
-        this.subscriptions.push(
-            workspace.onDidChangeWorkspaceFolders(event => {
-                // Remove all clients that are not referenced by any folder anymore
-                if (event.removed.length === 0) {
-                    return
-                }
-                this.clients.forEach((client, key) => {
-                    if (client.folderUri.scheme === 'untitled' || getWorkspaceFolderUri(client.folderUri)) {
-                        return
-                    }
-
-                    logger.log(`[ClientProvider] onDidChangeWorkspaceFolders removing client for ${key}`)
-                    this.clients.delete(key)
-                    client.dispose()
-                    this.clientRemovedEmitter.fire(client)
-                })
-            }),
-        )
     }
 
     getActiveClient(): LeanClient | undefined {
@@ -115,8 +100,6 @@ export class LeanClientProvider implements Disposable {
     }
 
     private async onInstallChanged(uri: FileUri) {
-        // Uri is a package Uri in the case a lean package file was changed.
-        logger.log(`[ClientProvider] installChanged for ${uri}`)
         this.pendingInstallChanged.push(uri)
         if (this.processingInstallChanged) {
             // avoid re-entrancy.
@@ -135,18 +118,9 @@ export class LeanClientProvider implements Disposable {
                     continue
                 }
 
-                const preconditionCheckResult = await checkLean4ProjectPreconditions(
-                    this.outputChannel,
-                    'Client Restart',
-                    projectUri,
-                )
-                if (preconditionCheckResult !== 'Fatal') {
-                    logger.log('[ClientProvider] got lean version 4')
-                    const [cached, client] = await this.ensureClient(uri)
-                    if (cached && client) {
-                        await client.restart()
-                        logger.log('[ClientProvider] restart complete')
-                    }
+                const [cached, client] = await this.ensureClient(uri)
+                if (cached && client) {
+                    await client.restart()
                 }
             } catch (e) {
                 logger.log(`[ClientProvider] Exception checking lean version: ${e}`)
@@ -185,9 +159,33 @@ export class LeanClientProvider implements Disposable {
         this.restartFile(doc.extUri)
     }
 
-    private async stopActiveClient() {
-        if (this.activeClient && this.activeClient.isStarted()) {
-            await this.activeClient?.stop()
+    private async stopClient(folderUri: ExtUri | undefined) {
+        let clientToStop: LeanClient
+        if (folderUri === undefined) {
+            if (this.activeClient === undefined) {
+                displayNotification('Error', 'Cannot stop language server: No active client.')
+                return
+            }
+            clientToStop = this.activeClient
+        } else {
+            const foundClient = this.getClientForFolder(folderUri)
+            if (foundClient === undefined) {
+                displayNotification(
+                    'Error',
+                    `Cannot stop language server: No client for project at '${folderUri.toString()}'.`,
+                )
+                return
+            }
+            clientToStop = foundClient
+        }
+        if (clientToStop.isStarted()) {
+            await clientToStop.stop()
+        }
+        const key = clientToStop.folderUri.toString()
+        this.clients.delete(key)
+        this.pending.delete(key)
+        if (clientToStop === this.activeClient) {
+            this.activeClient = undefined
         }
     }
 
@@ -264,7 +262,13 @@ export class LeanClientProvider implements Disposable {
         const preconditionCheckResult = await checkLean4ProjectPreconditions(
             this.outputChannel,
             'Client Startup',
+            this.getClients().map(client => client.folderUri),
             folderUri,
+            uri,
+            async (folderUriToStop: FileUri) => {
+                await this.stopClient(folderUriToStop)
+                await this.ensureClient(uri)
+            },
         )
         if (preconditionCheckResult === 'Fatal') {
             this.pending.delete(key)
diff --git a/vscode-lean4/src/utils/exturi.ts b/vscode-lean4/src/utils/exturi.ts
@@ -66,16 +66,15 @@ export class FileUri {
     }
 }
 
-export function getWorkspaceFolderUri(uri: FileUri): FileUri | undefined {
-    const folder = workspace.getWorkspaceFolder(uri.asUri())
-    if (folder === undefined) {
-        return undefined
-    }
-    const folderUri = FileUri.fromUri(folder.uri)
-    if (folderUri === undefined) {
-        return undefined
+export function isInWorkspaceFolder(uri: FileUri): boolean {
+    return workspace.getWorkspaceFolder(uri.asUri()) !== undefined
+}
+
+export function isWorkspaceFolder(uri: FileUri): boolean {
+    if (workspace.workspaceFolders === undefined) {
+        return false
     }
-    return folderUri
+    return workspace.workspaceFolders.some(folder => uri.equalsUri(folder.uri))
 }
 
 export class UntitledUri {
diff --git a/vscode-lean4/src/utils/internalErrors.ts b/vscode-lean4/src/utils/internalErrors.ts
@@ -1,23 +1,27 @@
 import { env } from 'vscode'
 import { displayNotificationWithInput } from './notifs'
 
+export async function displayInternalError(scope: string, e: any) {
+    let msg: string = `Internal error (while ${scope}): ${e}`
+    let fullMsg: string = msg
+    if (e instanceof Error && e.stack !== undefined) {
+        fullMsg += `\n\n${e.stack}`
+    }
+    msg +=
+        "\n\nIf you are using an up-to-date version of the Lean 4 VS Code extension, please copy the full error message using the 'Copy Error to Clipboard' button and report it at https://github.com/leanprover/vscode-lean4/ or https://leanprover.zulipchat.com/."
+    const copyToClipboardInput = 'Copy Error to Clipboard'
+    const closeInput = 'Close'
+    const choice = await displayNotificationWithInput('Error', msg, [copyToClipboardInput], closeInput)
+    if (choice === copyToClipboardInput) {
+        await env.clipboard.writeText(fullMsg)
+    }
+}
+
 export async function displayInternalErrorsIn<T>(scope: string, f: () => Promise<T>): Promise<T> {
     try {
         return await f()
     } catch (e) {
-        let msg: string = `Internal error (while ${scope}): ${e}`
-        let fullMsg: string = msg
-        if (e instanceof Error && e.stack !== undefined) {
-            fullMsg += `\n\n${e.stack}`
-        }
-        msg +=
-            "\n\nIf you are using an up-to-date version of the Lean 4 VS Code extension, please copy the full error message using the 'Copy Error to Clipboard' button and report it at https://github.com/leanprover/vscode-lean4/ or https://leanprover.zulipchat.com/."
-        const copyToClipboardInput = 'Copy Error to Clipboard'
-        const closeInput = 'Close'
-        const choice = await displayNotificationWithInput('Error', msg, [copyToClipboardInput], closeInput)
-        if (choice === copyToClipboardInput) {
-            await env.clipboard.writeText(fullMsg)
-        }
+        await displayInternalError(scope, e)
         throw e
     }
 }
diff --git a/vscode-lean4/src/utils/projectInfo.ts b/vscode-lean4/src/utils/projectInfo.ts
@@ -1,7 +1,7 @@
 import * as fs from 'fs'
-import { ExtUri, FileUri, getWorkspaceFolderUri } from './exturi'
-import { dirExists, fileExists } from './fsHelper'
 import path from 'path'
+import { ExtUri, FileUri, isWorkspaceFolder } from './exturi'
+import { dirExists, fileExists } from './fsHelper'
 
 // Detect lean4 root directory (works for both lean4 repo and nightly distribution)
 
@@ -42,8 +42,6 @@ export async function findLeanProjectRootInfo(uri: FileUri): Promise<ProjectRoot
     const toolchainFileName = 'lean-toolchain'
 
     let path = uri
-    const containingWsFolderUri = getWorkspaceFolderUri(uri)
-
     try {
         if ((await fs.promises.stat(path.fsPath)).isFile()) {
             path = uri.join('..')
@@ -65,7 +63,7 @@ export async function findLeanProjectRootInfo(uri: FileUri): Promise<ProjectRoot
             // Stop searching in case users accidentally created a lean-toolchain file above the core directory
             break
         }
-        if (containingWsFolderUri !== undefined && path.equals(containingWsFolderUri)) {
+        if (isWorkspaceFolder(path)) {
             if (bestLeanToolchain === undefined) {
                 // If we haven't found a toolchain yet, prefer the workspace folder as the project scope for the file,
                 // but keep looking in case there is a lean-toolchain above the workspace folder

Original file line number	Diff line number	Diff line change
`@@ -66,16 +66,15 @@ export class FileUri {`
`66`	`66`	`}`
`67`	`67`	`}`
`68`	`68`
`69`		`-export function getWorkspaceFolderUri(uri: FileUri): FileUri \| undefined {`
`70`		`- const folder = workspace.getWorkspaceFolder(uri.asUri())`
`71`		`- if (folder === undefined) {`
`72`		`- return undefined`
`73`		`- }`
`74`		`- const folderUri = FileUri.fromUri(folder.uri)`
`75`		`- if (folderUri === undefined) {`
`76`		`- return undefined`
	`69`	`+export function isInWorkspaceFolder(uri: FileUri): boolean {`
	`70`	`+ return workspace.getWorkspaceFolder(uri.asUri()) !== undefined`
	`71`	`+}`
	`72`	`+`
	`73`	`+export function isWorkspaceFolder(uri: FileUri): boolean {`
	`74`	`+ if (workspace.workspaceFolders === undefined) {`
	`75`	`+ return false`
`77`	`76`	`}`
`78`		`- return folderUri`
	`77`	`+ return workspace.workspaceFolders.some(folder => uri.equalsUri(folder.uri))`
`79`	`78`	`}`
`80`	`79`
`81`	`80`	`export class UntitledUri {`