diff --git a/vscode-lean4/manual/manual.md b/vscode-lean4/manual/manual.md index 347e826b..e0cd7c91 100644 --- a/vscode-lean4/manual/manual.md +++ b/vscode-lean4/manual/manual.md @@ -611,7 +611,7 @@ The Lean 4 VS Code extension supports the following commands that can be run in 1. **['Project: Clean Project'](command:lean4.project.clean)**. Removes all build artifacts for the Lean project. If the project is [Mathlib](https://github.com/leanprover-community/mathlib4) or depends on it, it will also offer to download and install the current Mathlib build artifact cache after cleaning the project. 1. **['Project: Update Dependency…'](command:lean4.project.updateDependency)**. Displays a list of all dependencies that can be updated. After selecting a dependency and updating it, if the project is [Mathlib](https://github.com/leanprover-community/mathlib4) or depends on it, it will also download and install the current Mathlib build artifact cache. At the end, if the Lean toolchain of the updated project differs from the Lean toolchain of the project, the command will offer to update the Lean toolchain of the project to that of the updated dependency. 1. **['Project: Fetch Mathlib Build Cache'](command:lean4.project.fetchCache)**. Downloads and installs the current Mathlib build artifact cache if the project is [Mathlib](https://github.com/leanprover-community/mathlib4) or depends on it. -1. **['Project: Fetch Mathlib Build Cache For Focused File'](command:lean4.project.fetchFileCache)**. Downloads and installs the current Mathlib build artifact for the focused file if the project is [Mathlib](https://github.com/leanprover-community/mathlib4). +1. **['Project: Fetch Mathlib Build Cache For Current Imports'](command:lean4.project.fetchFileCache)**. Downloads and installs the current Mathlib build artifact for the focused file and all of its imports if the project is [Mathlib](https://github.com/leanprover-community/mathlib4).
diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json index b9f9131a..1618ea97 100644 --- a/vscode-lean4/package.json +++ b/vscode-lean4/package.json @@ -365,8 +365,8 @@ { "command": "lean4.project.fetchFileCache", "category": "Lean 4", - "title": "Project: Fetch Mathlib Build Cache For Focused File", - "description": "Downloads cached Mathlib build artifacts of the focused file to avoid full elaboration" + "title": "Project: Fetch Mathlib Build Cache For Current Imports", + "description": "Downloads cached Mathlib build artifacts of the focused file and all of its imports to avoid full elaboration" } ], "languages": [ diff --git a/vscode-lean4/src/leanclient.ts b/vscode-lean4/src/leanclient.ts index ff6e815d..52615e1c 100644 --- a/vscode-lean4/src/leanclient.ts +++ b/vscode-lean4/src/leanclient.ts @@ -188,7 +188,7 @@ export class LeanClient implements Disposable { // Should only be called from `restart` const startTime = Date.now() - progress.report({ increment: 0 }) + progress.report({}) this.client = await this.setupClient() let insideRestart = true @@ -215,7 +215,6 @@ export class LeanClient implements Disposable { } } }) - progress.report({ increment: 80 }) await this.client.start() const version = this.client.initializeResult?.serverInfo?.version if (version && new SemVer(version).compare('0.2.0') < 0) { @@ -314,14 +313,16 @@ export class LeanClient implements Disposable { return 'IsRestarting' } this.isRestarting = true // Ensure that client cannot be restarted in the mean-time + try { + if (this.isStarted()) { + await this.stop() + } - if (this.isStarted()) { - await this.stop() + await action() + } finally { + this.isRestarting = false } - await action() - - this.isRestarting = false await this.restart() return 'Success' diff --git a/vscode-lean4/src/projectoperations.ts b/vscode-lean4/src/projectoperations.ts index 7eb11201..9ba2f05b 100644 --- a/vscode-lean4/src/projectoperations.ts +++ b/vscode-lean4/src/projectoperations.ts @@ -7,7 +7,13 @@ import { LeanClientProvider } from './utils/clientProvider' import { toExtUri } from './utils/exturi' import { cacheNotFoundError, lake, LakeRunner } from './utils/lake' import { DirectGitDependency, Manifest, ManifestReadError, parseManifestInFolder } from './utils/manifest' -import { displayError, displayInformation, displayInformationWithInput, displayWarningWithInput } from './utils/notifs' +import { + displayError, + displayInformation, + displayInformationWithInput, + displayInformationWithOptionalInput, + displayWarningWithInput, +} from './utils/notifs' type DependencyToolchainResult = | { kind: 'Success'; dependencyToolchain: string } @@ -27,7 +33,7 @@ export class ProjectOperationProvider implements Disposable { commands.registerCommand('lean4.project.clean', () => this.cleanProject()), commands.registerCommand('lean4.project.updateDependency', () => this.updateDependency()), commands.registerCommand('lean4.project.fetchCache', () => this.fetchMathlibCache()), - commands.registerCommand('lean4.project.fetchFileCache', () => this.fetchMathlibCacheForFocusedFile()), + commands.registerCommand('lean4.project.fetchFileCache', () => this.fetchMathlibCacheForCurrentImports()), ) } @@ -119,8 +125,8 @@ export class ProjectOperationProvider implements Disposable { }) } - private async fetchMathlibCacheForFocusedFile() { - await this.runOperation('Fetch Mathlib Build Cache For Focused File', async lakeRunner => { + private async fetchMathlibCacheForCurrentImports() { + await this.runOperation('Fetch Mathlib Build Cache For Current Imports', async lakeRunner => { const projectUri = lakeRunner.cwdUri! if (!window.activeTextEditor || window.activeTextEditor.document.languageId !== 'lean4') { @@ -182,8 +188,10 @@ export class ProjectOperationProvider implements Disposable { return } - displayInformation( + displayInformationWithOptionalInput( `Mathlib build artifact cache for '${relativeActiveFileUri.fsPath}' fetched successfully.`, + 'Restart File', + () => this.clientProvider.restartFile(activeFileUri), ) }) } @@ -392,34 +400,32 @@ export class ProjectOperationProvider implements Disposable { return } this.isRunningOperation = true + try { + if (!this.clientProvider) { + displayError('Lean client has not loaded yet.') + return + } - if (!this.clientProvider) { - displayError('Lean client has not loaded yet.') - this.isRunningOperation = false - return - } - - const activeClient: LeanClient | undefined = this.clientProvider.getActiveClient() - if (!activeClient) { - displayError('No active client.') - this.isRunningOperation = false - return - } + const activeClient: LeanClient | undefined = this.clientProvider.getActiveClient() + if (!activeClient) { + displayError('No active client.') + return + } - if (activeClient.folderUri.scheme === 'untitled') { - displayError('Cannot run project action for untitled files.') - this.isRunningOperation = false - return - } + if (activeClient.folderUri.scheme === 'untitled') { + displayError('Cannot run project action for untitled files.') + return + } - const lakeRunner: LakeRunner = lake(this.channel, activeClient.folderUri, context) + const lakeRunner: LakeRunner = lake(this.channel, activeClient.folderUri, context) - const result: 'Success' | 'IsRestarting' = await activeClient.withStoppedClient(() => command(lakeRunner)) - if (result === 'IsRestarting') { - displayError('Cannot run project action while restarting the server.') + const result: 'Success' | 'IsRestarting' = await activeClient.withStoppedClient(() => command(lakeRunner)) + if (result === 'IsRestarting') { + displayError('Cannot run project action while restarting the server.') + } + } finally { + this.isRunningOperation = false } - - this.isRunningOperation = false } dispose() { diff --git a/vscode-lean4/src/utils/clientProvider.ts b/vscode-lean4/src/utils/clientProvider.ts index c825bef2..6450a9c0 100644 --- a/vscode-lean4/src/utils/clientProvider.ts +++ b/vscode-lean4/src/utils/clientProvider.ts @@ -1,4 +1,5 @@ import { LeanFileProgressProcessingInfo, ServerStoppedReason } from '@leanprover/infoview-api' +import path from 'path' import { Disposable, EventEmitter, OutputChannel, TextDocument, commands, window, workspace } from 'vscode' import { checkAll, @@ -72,8 +73,8 @@ export class LeanClientProvider implements Disposable { ) this.subscriptions.push( - commands.registerCommand('lean4.restartFile', () => this.restartFile()), - commands.registerCommand('lean4.refreshFileDependencies', () => this.restartFile()), + commands.registerCommand('lean4.restartFile', () => this.restartActiveFile()), + commands.registerCommand('lean4.refreshFileDependencies', () => this.restartActiveFile()), commands.registerCommand('lean4.restartServer', () => this.restartActiveClient()), commands.registerCommand('lean4.stopServer', () => this.stopActiveClient()), ) @@ -143,7 +144,25 @@ export class LeanClientProvider implements Disposable { this.processingInstallChanged = false } - private restartFile() { + restartFile(uri: ExtUri) { + const fileName = uri.scheme === 'file' ? path.basename(uri.fsPath) : 'untitled file' + + const client: LeanClient | undefined = this.findClient(uri) + if (!client || !client.isRunning()) { + displayError(`No active client for '${fileName}'.`) + return + } + + const doc = workspace.textDocuments.find(doc => uri.equalsUri(doc.uri)) + if (!doc) { + displayError(`'${fileName}' was closed in the meantime.`) + return + } + + void client.restartFile(doc) + } + + restartActiveFile() { if (!this.activeClient || !this.activeClient.isRunning()) { displayError('No active client.') return