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.
leanprover · Oct 29, 2024 · f6b12eb · f6b12eb
1 parent 9ea8703
commit f6b12eb
Show file tree

Hide file tree

Showing 5 changed files with 67 additions and 41 deletions.
diff --git 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).
 
 <br/>
 

diff --git 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
@@ -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
@@ -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
@@ -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