From f6b12eb4b7d4a479c1739988f9a36b2737a72649 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Tue, 29 Oct 2024 14:13:36 +0100 Subject: [PATCH] feat: restart file button in 'fetch cache for focused file' command (#543) Also fixes some potential bugs caused by exceptions, turns the server startup progress bar into an infinite one and renames the command to make it more clear what it does. --- vscode-lean4/manual/manual.md | 2 +- vscode-lean4/package.json | 4 +- vscode-lean4/src/leanclient.ts | 15 +++--- vscode-lean4/src/projectoperations.ts | 62 +++++++++++++----------- vscode-lean4/src/utils/clientProvider.ts | 25 ++++++++-- 5 files changed, 67 insertions(+), 41 deletions(-) diff --git a/vscode-lean4/manual/manual.md b/vscode-lean4/manual/manual.md index 347e826bb..e0cd7c912 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 b9f9131a6..1618ea972 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 ff6e815da..52615e1c8 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 7eb11201f..9ba2f05b4 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 c825bef23..6450a9c0e 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