diff --git a/package-lock.json b/package-lock.json index 44b594a3..2c5f1034 100644 --- a/package-lock.json +++ b/package-lock.json @@ -15648,17 +15648,17 @@ } }, "node_modules/vscode-languageclient": { - "version": "8.1.0", - "resolved": "https://registry.npmjs.org/vscode-languageclient/-/vscode-languageclient-8.1.0.tgz", - "integrity": "sha512-GL4QdbYUF/XxQlAsvYWZRV3V34kOkpRlvV60/72ghHfsYFnS/v2MANZ9P6sHmxFcZKOse8O+L9G7Czg0NUWing==", + "version": "9.0.1", + "resolved": "https://registry.npmjs.org/vscode-languageclient/-/vscode-languageclient-9.0.1.tgz", + "integrity": "sha512-JZiimVdvimEuHh5olxhxkht09m3JzUGwggb5eRUkzzJhZ2KjCN0nh55VfiED9oez9DyF8/fz1g1iBV3h+0Z2EA==", "license": "MIT", "dependencies": { "minimatch": "^5.1.0", "semver": "^7.3.7", - "vscode-languageserver-protocol": "3.17.3" + "vscode-languageserver-protocol": "3.17.5" }, "engines": { - "vscode": "^1.67.0" + "vscode": "^1.82.0" } }, "node_modules/vscode-languageclient/node_modules/minimatch": { @@ -15673,31 +15673,6 @@ "node": ">=10" } }, - "node_modules/vscode-languageclient/node_modules/vscode-jsonrpc": { - "version": "8.1.0", - "resolved": "https://registry.npmjs.org/vscode-jsonrpc/-/vscode-jsonrpc-8.1.0.tgz", - "integrity": "sha512-6TDy/abTQk+zDGYazgbIPc+4JoXdwC8NHU9Pbn4UJP1fehUyZmM4RHp5IthX7A6L5KS30PRui+j+tbbMMMafdw==", - "license": "MIT", - "engines": { - "node": ">=14.0.0" - } - }, - "node_modules/vscode-languageclient/node_modules/vscode-languageserver-protocol": { - "version": "3.17.3", - "resolved": "https://registry.npmjs.org/vscode-languageserver-protocol/-/vscode-languageserver-protocol-3.17.3.tgz", - "integrity": "sha512-924/h0AqsMtA5yK22GgMtCYiMdCOtWTSGgUOkgEDX+wk2b0x4sAfLiO4NxBxqbiVtz7K7/1/RgVrVI0NClZwqA==", - "license": "MIT", - "dependencies": { - "vscode-jsonrpc": "8.1.0", - "vscode-languageserver-types": "3.17.3" - } - }, - "node_modules/vscode-languageclient/node_modules/vscode-languageserver-types": { - "version": "3.17.3", - "resolved": "https://registry.npmjs.org/vscode-languageserver-types/-/vscode-languageserver-types-3.17.3.tgz", - "integrity": "sha512-SYU4z1dL0PyIMd4Vj8YOqFvHu7Hz/enbWtpfnVbJHU4Nd1YNYx8u0ennumc6h48GQNeOLxmwySmnADouT/AuZA==", - "license": "MIT" - }, "node_modules/vscode-languageserver-protocol": { "version": "3.17.5", "resolved": "https://registry.npmjs.org/vscode-languageserver-protocol/-/vscode-languageserver-protocol-3.17.5.tgz", @@ -16468,7 +16443,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": { diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json index a5d701bd..b9213a55 100644 --- a/vscode-lean4/package.json +++ b/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": { diff --git a/vscode-lean4/src/config.ts b/vscode-lean4/src/config.ts index c3561195..597b9be5 100644 --- a/vscode-lean4/src/config.ts +++ b/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) } diff --git a/vscode-lean4/src/diagnostics/setupDiagnostics.ts b/vscode-lean4/src/diagnostics/setupDiagnostics.ts index 069832fb..35c14522 100644 --- a/vscode-lean4/src/diagnostics/setupDiagnostics.ts +++ b/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, - ): Promise { - 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 index b1168c77..6111c106 100644 --- a/vscode-lean4/src/leanclient.ts +++ b/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

(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 { 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) diff --git a/vscode-lean4/src/utils/clientProvider.ts b/vscode-lean4/src/utils/clientProvider.ts index c9402a1a..8a8de53a 100644 --- a/vscode-lean4/src/utils/clientProvider.ts +++ b/vscode-lean4/src/utils/clientProvider.ts @@ -34,7 +34,6 @@ async function checkLean4ProjectPreconditions( toolchainUpdateMode: 'PromptAboutUpdate', }) }, - () => d.checkIsNestedProjectFolder(existingFolderUris, folderUri, fileUri, stopOtherServer), ) } @@ -200,10 +199,10 @@ export class LeanClientProvider implements Disposable { } // Find the client for a given document. - findClient(path: ExtUri) { + findClient(path: ExtUri): LeanClient | undefined { const candidates = this.getClients().filter(client => client.isInFolderManagedByThisClient(path)) // All candidate folders are a prefix of `path`, so they must necessarily be prefixes of one another - // => the best candidate (the most top-level client folder) is just the one with the shortest path + // => the best candidate (the innermost client folder) is just the one with the longest path let bestCandidate: LeanClient | undefined for (const candidate of candidates) { if (!bestCandidate) { @@ -215,7 +214,7 @@ export class LeanClientProvider implements Disposable { if ( folder.scheme === 'file' && bestFolder.scheme === 'file' && - folder.fsPath.length < bestFolder.fsPath.length + folder.fsPath.length > bestFolder.fsPath.length ) { bestCandidate = candidate } diff --git a/vscode-lean4/src/utils/exturi.ts b/vscode-lean4/src/utils/exturi.ts index 1b4259a3..23198d70 100644 --- a/vscode-lean4/src/utils/exturi.ts +++ b/vscode-lean4/src/utils/exturi.ts @@ -58,6 +58,10 @@ export class FileUri { return FileUri.fromUriOrError(Uri.joinPath(this.asUri(), ...pathSegments)) } + normalize(): FileUri { + return this.join() + } + isInFolder(folderUri: FileUri): boolean { return isFileInFolder(this.fsPath, folderUri.fsPath) } @@ -82,6 +86,14 @@ export function isWorkspaceFolder(uri: FileUri): boolean { return workspace.workspaceFolders.some(folder => uri.equalsUri(folder.uri)) } +export function getWorkspaceFolderUri(uri: FileUri): FileUri | undefined { + const workspaceFolder = workspace.getWorkspaceFolder(uri.asUri()) + if (workspaceFolder === undefined) { + return undefined + } + return FileUri.fromUri(workspaceFolder.uri) +} + export class UntitledUri { scheme: 'untitled' path: string diff --git a/vscode-lean4/src/utils/projectInfo.ts b/vscode-lean4/src/utils/projectInfo.ts index 164014ed..82cbfd9f 100644 --- a/vscode-lean4/src/utils/projectInfo.ts +++ b/vscode-lean4/src/utils/projectInfo.ts @@ -1,6 +1,6 @@ import * as fs from 'fs' import path from 'path' -import { ExtUri, FileUri, isWorkspaceFolder, UntitledUri } from './exturi' +import { ExtUri, FileUri, getWorkspaceFolderUri, UntitledUri } from './exturi' import { dirExists, fileExists } from './fsHelper' // Detect lean4 root directory (works for both lean4 repo and nightly distribution) @@ -51,59 +51,84 @@ export function lakefileLeanUri(projectUri: FileUri) { return projectUri.join('lakefile.lean') } +function parentDirOf(uri: FileUri, subpath: string): FileUri | undefined { + const numComponents = subpath.split(path.sep).length + let p = uri.normalize().fsPath + const i = p.indexOf(subpath) + if (i === -1) { + return undefined + } + p = p.slice(0, i + subpath.length) + // Ensures that there is no trailing `/`. + for (let n = 0; n < numComponents; n++) { + p = path.dirname(p) + } + return new FileUri(p) +} + +function routePackagesDir(uri: FileUri): FileUri { + // `lean-toolchain` files in `.lake/packages` are ignored because + // the appropriate project scope for dependencies of a project is the root directory of the project. + // Technically, Lake allows configuring the location of the packages directory, so the extension may not be able to figure out + // the correct project scope for a dependency when this setting is set. + // In the future, Lake may maintain a back-link from the directory of dependencies back to the project root, + // but for now, this heuristic must suffice. + return parentDirOf(uri, path.join('.lake', 'packages')) ?? uri +} + // Find the root of a Lean project and the Uri for the 'lean-toolchain' file found there. export async function findLeanProjectRootInfo(uri: ExtUri): Promise { if (uri.scheme === 'untitled') { return { kind: 'Success', projectRootUri: new UntitledUri(), toolchainUri: undefined } } - let path = uri + + let uriDir: FileUri try { - if ((await fs.promises.stat(path.fsPath)).isFile()) { - path = uri.join('..') + if ((await fs.promises.stat(uri.fsPath)).isFile()) { + uriDir = uri.join('..') + } else { + uriDir = uri } } catch (e) { return { kind: 'FileNotFound' } } - let bestFolder = path - let bestLeanToolchain: FileUri | undefined + let currentDir = routePackagesDir(uriDir) + while (true) { - const leanToolchain = leanToolchainUri(path) - const lakefileLean = lakefileLeanUri(path) - const lakefileToml = lakefileTomlUri(path) + const leanToolchain = leanToolchainUri(currentDir) + const lakefileLean = lakefileLeanUri(currentDir) + const lakefileToml = lakefileTomlUri(currentDir) if (await fileExists(leanToolchain.fsPath)) { - bestFolder = path - bestLeanToolchain = leanToolchain - } else if (await isCoreLean4Directory(path)) { - bestFolder = path - bestLeanToolchain = undefined - // Stop searching in case users accidentally created a lean-toolchain file above the core directory - break - } else if (await fileExists(lakefileLean.fsPath)) { - return { kind: 'LakefileWithoutToolchain', projectRootUri: path, lakefileUri: lakefileLean } - } else if (await fileExists(lakefileToml.fsPath)) { - return { kind: 'LakefileWithoutToolchain', projectRootUri: path, lakefileUri: lakefileToml } + return { kind: 'Success', projectRootUri: currentDir, toolchainUri: leanToolchain } } - 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 - // (New users sometimes accidentally open sub-folders of projects) - bestFolder = path - } else { - // Stop looking above the barrier if we have a toolchain. This is necessary for the nested lean-toolchain setup of core. - break - } + if (await isCoreLean4Directory(currentDir)) { + return { kind: 'Success', projectRootUri: currentDir, toolchainUri: undefined } + } + if (await fileExists(lakefileLean.fsPath)) { + return { kind: 'LakefileWithoutToolchain', projectRootUri: currentDir, lakefileUri: lakefileLean } } - const parent = path.join('..') - if (parent.equals(path)) { - // no project file found. + if (await fileExists(lakefileToml.fsPath)) { + return { kind: 'LakefileWithoutToolchain', projectRootUri: currentDir, lakefileUri: lakefileToml } + } + + const parentDir = currentDir.join('..') + if (parentDir.equals(currentDir)) { break } - path = parent + currentDir = parentDir + } + + // No `lean-toolchain` or core directory found. + // If the file is in a workspace folder, we use the workspace folder, + // and otherwise we use the immediate directory that the file is contained in. + // In nested workspace folders, VS Code yields the innermost one. + const workspaceDir = getWorkspaceFolderUri(uri) + if (workspaceDir !== undefined) { + return { kind: 'Success', projectRootUri: workspaceDir, toolchainUri: undefined } } - return { kind: 'Success', projectRootUri: bestFolder, toolchainUri: bestLeanToolchain } + return { kind: 'Success', projectRootUri: uriDir, toolchainUri: undefined } } export async function findLeanProjectInfo(uri: FileUri): Promise {