Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: restart file button in 'fetch cache for focused file' command #543

Merged
merged 2 commits into from
Oct 29, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion vscode-lean4/manual/manual.md
Original file line number Diff line number Diff line change
Expand Up @@ -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/>

Expand Down
4 changes: 2 additions & 2 deletions vscode-lean4/package.json
Original file line number Diff line number Diff line change
Expand Up @@ -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": [
Expand Down
15 changes: 8 additions & 7 deletions vscode-lean4/src/leanclient.ts
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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) {
Expand Down Expand Up @@ -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'
Expand Down
62 changes: 34 additions & 28 deletions vscode-lean4/src/projectoperations.ts
Original file line number Diff line number Diff line change
Expand Up @@ -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 }
Expand All @@ -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()),
)
}

Expand Down Expand Up @@ -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') {
Expand Down Expand Up @@ -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),
)
})
}
Expand Down Expand Up @@ -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() {
Expand Down
25 changes: 22 additions & 3 deletions vscode-lean4/src/utils/clientProvider.ts
Original file line number Diff line number Diff line change
@@ -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,
Expand Down Expand Up @@ -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()),
)
Expand Down Expand Up @@ -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
Expand Down
Loading