From 8716c54ec5c32e4939d95b70084601aacd92b0aa Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Wed, 27 Mar 2024 11:10:05 +0100 Subject: [PATCH] feat: replace stale dep notifs with "restart file" infoview button (#419) --- lean4-infoview-api/package.json | 2 +- lean4-infoview-api/src/infoviewApi.ts | 3 + lean4-infoview/package.json | 5 +- lean4-infoview/src/infoview/index.css | 7 + lean4-infoview/src/infoview/info.tsx | 6 +- lean4-infoview/src/infoview/main.tsx | 8 ++ package-lock.json | 86 +++++++++++-- vscode-lean4/package.json | 4 +- vscode-lean4/src/infoview.ts | 14 ++ vscode-lean4/src/utils/clientProvider.ts | 156 ----------------------- 10 files changed, 116 insertions(+), 175 deletions(-) diff --git a/lean4-infoview-api/package.json b/lean4-infoview-api/package.json index 7e18f60c4..be9952e3e 100644 --- a/lean4-infoview-api/package.json +++ b/lean4-infoview-api/package.json @@ -1,6 +1,6 @@ { "name": "@leanprover/infoview-api", - "version": "0.2.1", + "version": "0.3.0", "description": "Types and API for @leanprover/infoview.", "scripts": { "watch": "tsc --watch", diff --git a/lean4-infoview-api/src/infoviewApi.ts b/lean4-infoview-api/src/infoviewApi.ts index 2f74df3e4..203bfeccc 100644 --- a/lean4-infoview-api/src/infoviewApi.ts +++ b/lean4-infoview-api/src/infoviewApi.ts @@ -57,6 +57,9 @@ export interface EditorApi { /** Highlight a range in a document in the editor. */ showDocument(show: ShowDocumentParams): Promise; + /** Restarts the given file. */ + restartFile(uri: string): Promise + /** * Creates an RPC session for the given uri and returns the session id. * The extension takes care of keeping the RPC session alive. diff --git a/lean4-infoview/package.json b/lean4-infoview/package.json index 187077ac3..a0d2e1f8c 100644 --- a/lean4-infoview/package.json +++ b/lean4-infoview/package.json @@ -1,6 +1,6 @@ { "name": "@leanprover/infoview", - "version": "0.4.5", + "version": "0.5.0", "description": "An interactive display for the Lean 4 theorem prover.", "scripts": { "watch": "rollup --config --environment NODE_ENV:development --watch", @@ -47,8 +47,9 @@ "typescript": "^4.9.5" }, "dependencies": { - "@leanprover/infoview-api": "~0.2.1", + "@leanprover/infoview-api": "~0.3.0", "@vscode/codicons": "^0.0.32", + "@vscode/webview-ui-toolkit": "^1.4.0", "es-module-shims": "^1.7.3", "marked": "^4.3.0", "react-fast-compare": "^3.2.2", diff --git a/lean4-infoview/src/infoview/index.css b/lean4-infoview/src/infoview/index.css index e6d3899e1..ad87c00c7 100644 --- a/lean4-infoview/src/infoview/index.css +++ b/lean4-infoview/src/infoview/index.css @@ -108,6 +108,13 @@ html,body { /* Headers for infoview */ +.restart-file-button { + position: fixed; + bottom: 10px; + right: 10px; + z-index: 37; +} + select { background-color: var(--vscode-dropdown-background); color: var(--vscode-dropdown-foreground); diff --git a/lean4-infoview/src/infoview/info.tsx b/lean4-infoview/src/infoview/info.tsx index 85700245d..e6d96d4e2 100644 --- a/lean4-infoview/src/infoview/info.tsx +++ b/lean4-infoview/src/infoview/info.tsx @@ -300,9 +300,11 @@ function InfoAux(props: InfoProps) { // While `lake print-paths` is running, the output of Lake is shown as // info diagnostics on line 1. However, all RPC requests block until // Lake is finished, so we don't see these diagnostics while Lake is - // building. Therefore we show the LSP diagnostics on line 1 if the + // building. Therefore we show the LSP diagnostics on line 1 if the // server does not respond within half a second. - if (pos.line === 0 && lspDiagsHere.length) { + // The same is true for fatal header diagnostics like the stale dependency notification. + const isAllHeaderDiags = lspDiagsHere.length > 0 && lspDiagsHere.every(diag => diag.range.start.line === 0) + if (isAllHeaderDiags) { setTimeout(() => resolve({ pos, status: 'updating', diff --git a/lean4-infoview/src/infoview/main.tsx b/lean4-infoview/src/infoview/main.tsx index 3d89f7685..57915dd32 100644 --- a/lean4-infoview/src/infoview/main.tsx +++ b/lean4-infoview/src/infoview/main.tsx @@ -1,6 +1,7 @@ import * as React from 'react'; import * as ReactDOM from 'react-dom/client'; import type { DidCloseTextDocumentParams, Location, DocumentUri } from 'vscode-languageserver-protocol'; +import { VSCodeButton } from '@vscode/webview-ui-toolkit/react' import 'tachyons/css/tachyons.css'; import '@vscode/codicons/dist/codicon.ttf'; @@ -65,6 +66,13 @@ function Main(props: {}) { {curUri &&
} + {curUri && + ec.api.restartFile(curUri)} + title='Restarts this file, rebuilding all of its outdated dependencies.'> + Restart File + } } diff --git a/package-lock.json b/package-lock.json index 261779011..58d08112d 100644 --- a/package-lock.json +++ b/package-lock.json @@ -21,11 +21,12 @@ }, "lean4-infoview": { "name": "@leanprover/infoview", - "version": "0.4.5", + "version": "0.5.0", "license": "Apache-2.0", "dependencies": { - "@leanprover/infoview-api": "~0.2.1", + "@leanprover/infoview-api": "~0.3.0", "@vscode/codicons": "^0.0.32", + "@vscode/webview-ui-toolkit": "^1.4.0", "es-module-shims": "^1.7.3", "marked": "^4.3.0", "react-fast-compare": "^3.2.2", @@ -53,7 +54,7 @@ }, "lean4-infoview-api": { "name": "@leanprover/infoview-api", - "version": "0.2.1", + "version": "0.3.0", "license": "Apache-2.0", "devDependencies": { "typescript": "^4.9.5", @@ -767,6 +768,47 @@ "node": ">=12" } }, + "node_modules/@microsoft/fast-element": { + "version": "1.12.0", + "resolved": "https://registry.npmjs.org/@microsoft/fast-element/-/fast-element-1.12.0.tgz", + "integrity": "sha512-gQutuDHPKNxUEcQ4pypZT4Wmrbapus+P9s3bR/SEOLsMbNqNoXigGImITygI5zhb+aA5rzflM6O8YWkmRbGkPA==" + }, + "node_modules/@microsoft/fast-foundation": { + "version": "2.49.5", + "resolved": "https://registry.npmjs.org/@microsoft/fast-foundation/-/fast-foundation-2.49.5.tgz", + "integrity": "sha512-3PpG1BNmZ5kUM1goYU3SsxjsM2H7Rk0ZmpDJ7mnRhWDgKiM5SzJ02KvALRUqDrJQoeDnkW0Q2Q+r9SkEd68Gpg==", + "dependencies": { + "@microsoft/fast-element": "^1.12.0", + "@microsoft/fast-web-utilities": "^5.4.1", + "tabbable": "^5.2.0", + "tslib": "^1.13.0" + } + }, + "node_modules/@microsoft/fast-foundation/node_modules/tabbable": { + "version": "5.3.3", + "resolved": "https://registry.npmjs.org/tabbable/-/tabbable-5.3.3.tgz", + "integrity": "sha512-QD9qKY3StfbZqWOPLp0++pOrAVb/HbUi5xCc8cUo4XjP19808oaMiDzn0leBY5mCespIBM0CIZePzZjgzR83kA==" + }, + "node_modules/@microsoft/fast-react-wrapper": { + "version": "0.3.23", + "resolved": "https://registry.npmjs.org/@microsoft/fast-react-wrapper/-/fast-react-wrapper-0.3.23.tgz", + "integrity": "sha512-iuL+J2AFKJ1mwUBxSp+bqzt4X93kQwj1jpVgHgw2VRzCOTl7wzta6X+lvRIVg4eoyLfmeVSMkB+q3PD87T/MyQ==", + "dependencies": { + "@microsoft/fast-element": "^1.12.0", + "@microsoft/fast-foundation": "^2.49.5" + }, + "peerDependencies": { + "react": ">=16.9.0" + } + }, + "node_modules/@microsoft/fast-web-utilities": { + "version": "5.4.1", + "resolved": "https://registry.npmjs.org/@microsoft/fast-web-utilities/-/fast-web-utilities-5.4.1.tgz", + "integrity": "sha512-ReWYncndjV3c8D8iq9tp7NcFNc1vbVHvcBFPME2nNFKNbS1XCesYZGlIlf3ot5EmuOXPlrzUHOWzQ2vFpIkqDg==", + "dependencies": { + "exenv-es6": "^1.1.1" + } + }, "node_modules/@nodelib/fs.scandir": { "version": "2.1.5", "resolved": "https://registry.npmjs.org/@nodelib/fs.scandir/-/fs.scandir-2.1.5.tgz", @@ -2510,6 +2552,25 @@ "node": ">=4" } }, + "node_modules/@vscode/webview-ui-toolkit": { + "version": "1.4.0", + "resolved": "https://registry.npmjs.org/@vscode/webview-ui-toolkit/-/webview-ui-toolkit-1.4.0.tgz", + "integrity": "sha512-modXVHQkZLsxgmd5yoP3ptRC/G8NBDD+ob+ngPiWNQdlrH6H1xR/qgOBD85bfU3BhOB5sZzFWBwwhp9/SfoHww==", + "dependencies": { + "@microsoft/fast-element": "^1.12.0", + "@microsoft/fast-foundation": "^2.49.4", + "@microsoft/fast-react-wrapper": "^0.3.22", + "tslib": "^2.6.2" + }, + "peerDependencies": { + "react": ">=16.9.0" + } + }, + "node_modules/@vscode/webview-ui-toolkit/node_modules/tslib": { + "version": "2.6.2", + "resolved": "https://registry.npmjs.org/tslib/-/tslib-2.6.2.tgz", + "integrity": "sha512-AEYxH93jGFPn/a2iVAwW87VuUIkR1FVUKB77NwMF7nBTDkDrrT/Hpt/IrCJ0QXhW27jTBDcf5ZY7w6RiqTMw2Q==" + }, "node_modules/@webassemblyjs/ast": { "version": "1.12.1", "resolved": "https://registry.npmjs.org/@webassemblyjs/ast/-/ast-1.12.1.tgz", @@ -4925,6 +4986,11 @@ "url": "https://github.com/sindresorhus/execa?sponsor=1" } }, + "node_modules/exenv-es6": { + "version": "1.1.1", + "resolved": "https://registry.npmjs.org/exenv-es6/-/exenv-es6-1.1.1.tgz", + "integrity": "sha512-vlVu3N8d6yEMpMsEm+7sUBAI81aqYYuEvfK0jNqmdb/OPXzzH7QWDDnVjMvDSY47JdHEqx/dfC/q8WkfoTmpGQ==" + }, "node_modules/expand-template": { "version": "2.0.3", "resolved": "https://registry.npmjs.org/expand-template/-/expand-template-2.0.3.tgz", @@ -6423,8 +6489,7 @@ "node_modules/js-tokens": { "version": "4.0.0", "resolved": "https://registry.npmjs.org/js-tokens/-/js-tokens-4.0.0.tgz", - "integrity": "sha512-RdJUflcE3cUzKiMqQgsCu06FPu9UdIJO0beYbPhHN4k6apgJtifcoCtT9bcxOpYBtpD2kCM6Sbzg4CausW/PKQ==", - "dev": true + "integrity": "sha512-RdJUflcE3cUzKiMqQgsCu06FPu9UdIJO0beYbPhHN4k6apgJtifcoCtT9bcxOpYBtpD2kCM6Sbzg4CausW/PKQ==" }, "node_modules/js-yaml": { "version": "4.1.0", @@ -7131,7 +7196,6 @@ "version": "1.4.0", "resolved": "https://registry.npmjs.org/loose-envify/-/loose-envify-1.4.0.tgz", "integrity": "sha512-lyuxPGr/Wfhrlem2CL/UcnUc1zcqKAImBDzukY7Y5F/yQiNdko6+fRLevlw1HgMySw7f611UIY408EtxRSoK3Q==", - "dev": true, "dependencies": { "js-tokens": "^3.0.0 || ^4.0.0" }, @@ -9863,7 +9927,6 @@ "version": "18.2.0", "resolved": "https://registry.npmjs.org/react/-/react-18.2.0.tgz", "integrity": "sha512-/3IjMdb2L9QbBdWiW5e3P2/npwMBaU9mHCSCUzNln0ZCYbcfTsGbTJrU/kGemdH2IWmB2ioZ+zkxtmq6g09fGQ==", - "dev": true, "dependencies": { "loose-envify": "^1.1.0" }, @@ -11646,8 +11709,7 @@ "node_modules/tslib": { "version": "1.14.1", "resolved": "https://registry.npmjs.org/tslib/-/tslib-1.14.1.tgz", - "integrity": "sha512-Xni35NKzjgMrwevysHTCArtLDpPvye8zV/0E4EyYn43P7/7qvQwPh9BGkHewbMulVntbigmcT7rdX3BNo9wRJg==", - "dev": true + "integrity": "sha512-Xni35NKzjgMrwevysHTCArtLDpPvye8zV/0E4EyYn43P7/7qvQwPh9BGkHewbMulVntbigmcT7rdX3BNo9wRJg==" }, "node_modules/tsutils": { "version": "3.21.0", @@ -12691,11 +12753,11 @@ }, "vscode-lean4": { "name": "lean4", - "version": "0.0.134", + "version": "0.0.135", "license": "Apache-2.0", "dependencies": { - "@leanprover/infoview": "~0.4.5", - "@leanprover/infoview-api": "~0.2.1", + "@leanprover/infoview": "~0.5.0", + "@leanprover/infoview-api": "~0.3.0", "axios": "^1.6.7", "cheerio": "^1.0.0-rc.12", "mobx": "^5.15.7", diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json index f7c57112b..da8c75558 100644 --- a/vscode-lean4/package.json +++ b/vscode-lean4/package.json @@ -894,8 +894,8 @@ "test": "node ./out/test/suite/runTest.js" }, "dependencies": { - "@leanprover/infoview": "~0.4.5", - "@leanprover/infoview-api": "~0.2.1", + "@leanprover/infoview": "~0.5.0", + "@leanprover/infoview-api": "~0.3.0", "axios": "^1.6.7", "cheerio": "^1.0.0-rc.12", "mobx": "^5.15.7", diff --git a/vscode-lean4/src/infoview.ts b/vscode-lean4/src/infoview.ts index 4d7bf1ff9..b1f7f548f 100644 --- a/vscode-lean4/src/infoview.ts +++ b/vscode-lean4/src/infoview.ts @@ -230,6 +230,20 @@ export class InfoProvider implements Disposable { p2cConverter.asRange(show.selection) ); }, + restartFile: async (uri) => { + const client = this.clientProvider.findClient(uri) + if (!client) { + return + } + + const path = Uri.parse(uri).fsPath + const document = workspace.textDocuments.find(doc => doc.uri.fsPath === path) + if (!document || document.isClosed) { + return + } + + await client.restartFile(document) + }, createRpcSession: async uri => { const client = this.clientProvider.findClient(uri); diff --git a/vscode-lean4/src/utils/clientProvider.ts b/vscode-lean4/src/utils/clientProvider.ts index 6b284aaca..a263deffa 100644 --- a/vscode-lean4/src/utils/clientProvider.ts +++ b/vscode-lean4/src/utils/clientProvider.ts @@ -28,17 +28,6 @@ export class LeanClientProvider implements Disposable { private pendingInstallChanged: Uri[] = []; private processingInstallChanged: boolean = false; private activeClient: LeanClient | undefined = undefined; - /** - * `Set` to avoid issuing multiple notifications - * for the "same" (same uri, diagnostic code and data) diagnostic. The language server issues - * diagnostics after every `didChange`, so we must ensure that we do not issue notifications - * over and over again. - */ - private notificationDiagnostics: Map>> = new Map() - /** - * Notifications that will be discharged as soon as the file denoted by a key in the map is selected. - */ - private pendingNotifications: Map = new Map() private progressChangedEmitter = new EventEmitter<[string, LeanFileProgressProcessingInfo[]]>() progressChanged = this.progressChangedEmitter.event @@ -72,7 +61,6 @@ export class LeanClientProvider implements Disposable { ); workspace.onDidOpenTextDocument(document => this.didOpenEditor(document)); - workspace.onDidCloseTextDocument(document => this.didCloseEditor(document.uri)) workspace.onDidChangeWorkspaceFolders((event) => { for (const folder of event.removed) { @@ -183,11 +171,6 @@ export class LeanClientProvider implements Disposable { void this.activeClient?.isStarted(); } - private async didCloseEditor(uri: Uri) { - this.notificationDiagnostics.delete(uri.fsPath) - this.pendingNotifications.delete(uri.fsPath) - } - async didOpenEditor(document: TextDocument) { // bail as quickly as possible on non-lean files. if (document.languageId !== 'lean' && document.languageId !== 'lean4') { @@ -225,8 +208,6 @@ export class LeanClientProvider implements Disposable { await client.openLean4Document(document) - await this.dischargePendingNotifications(document.uri) - await this.checkIsValidProjectFolder(client.folderUri) } catch (e) { logger.log(`[ClientProvider] ### Error opening document: ${e}`); @@ -376,37 +357,6 @@ export class LeanClientProvider implements Disposable { this.progressChangedEmitter.fire(arg); }); - client.diagnostics(async params => { - if (!client) { - return - } - - const fileUri = Uri.parse(params.uri) - - const doc: TextDocument | undefined = workspace.textDocuments.find(doc => doc.uri.fsPath === fileUri.fsPath) - if (!doc) { - return - } - const version = doc.version - - for (const d of params.diagnostics) { - if (!this.isNotificationDiagnostic(d)) { - continue - } - - const n = { - client, - uri: fileUri, - version, - diagnostic: d - } - - await this.addPendingNotificationDiagnostic(n) - } - }) - - client.restartedWorker(uri => this.didCloseEditor(Uri.parse(uri))) - this.pending.delete(key); logger.log('[ClientProvider] firing clientAddedEmitter event'); this.clientAddedEmitter.fire(client); @@ -459,112 +409,6 @@ Open this project instead?` } } - private async addPendingNotificationDiagnostic(newPendingNotification: NotificationDiagnostic) { - const uri = newPendingNotification.uri - const pendingNotifications = this.pendingNotifications.get(uri.fsPath) ?? [] - pendingNotifications.push(newPendingNotification) - this.pendingNotifications.set(uri.fsPath, pendingNotifications) - - // File is already open => immediately discharge notification - if (window.visibleTextEditors.some(e => e.document.uri.fsPath === uri.fsPath)) { - await this.dischargePendingNotifications(uri) - } - } - - private async dischargePendingNotifications(uri: Uri) { - const pendingNotifications = this.pendingNotifications.get(uri.fsPath) ?? [] - this.pendingNotifications.delete(uri.fsPath) - - const importsOutdatedErrors = pendingNotifications.filter(n => this.isImportsOutdatedError(n.diagnostic)) - if (importsOutdatedErrors.length > 0) { - void this.issueImportsOutdatedError(importsOutdatedErrors[0].client, uri) - } - - const importOutdatedWarnings = pendingNotifications.filter(n => this.isImportOutdatedWarning(n.diagnostic)) - if (importOutdatedWarnings.length > 0) { - let maxVersionWarning = importOutdatedWarnings[0] - for (const importOutdatedWarning of importOutdatedWarnings) { - if (importOutdatedWarning.version > maxVersionWarning.version) { - maxVersionWarning = importOutdatedWarning - } - } - const code = maxVersionWarning.diagnostic.code as string // ensured by isImportOutdatedWarning - const data = maxVersionWarning.diagnostic.data - const isOldImportOutdatedWarning = this.isKnownNotificationDiagnostic(uri, code, data) - if (!isOldImportOutdatedWarning) { - this.addNotificationDiagnostic(uri, code, data) - void this.issueImportOutdatedWarning(maxVersionWarning.client, uri, maxVersionWarning.diagnostic) - } - } - - } - - private isNotificationDiagnostic(d: Diagnostic): boolean { - return this.isImportOutdatedWarning(d) || this.isImportsOutdatedError(d) - } - - private isImportOutdatedWarning(d: Diagnostic): boolean { - return d.severity === DiagnosticSeverity.Warning && d.code === 'LanguageServer_ImportOutOfDate' - } - - private isImportsOutdatedError(d: Diagnostic): boolean { - return d.severity === DiagnosticSeverity.Error - && d.message.includes('Imports are out of date and must be rebuilt') - && d.range.start.line === 0 - && d.range.start.character === 0 - && d.range.end.line === 0 - && d.range.end.character === 0 - } - - private async issueImportsOutdatedError(client: LeanClient, fileUri: Uri) { - const fileName = path.basename(fileUri.fsPath) - const message = `Imports of '${fileName}' are out of date and must be rebuilt. Restarting the file will rebuild them.` - const input = 'Restart File' - const choice = await window.showInformationMessage(message, input) - if (choice !== input) { - return - } - - const document = workspace.textDocuments.find(doc => doc.uri.fsPath === fileUri.fsPath) - if (!document || document.isClosed) { - void window.showErrorMessage(`'${fileName}' was closed in the meantime. Imports will not be rebuilt.`) - return - } - - await client.restartFile(document) - } - - private async issueImportOutdatedWarning(client: LeanClient, fileUri: Uri, d: Diagnostic) { - const fileName = path.basename(fileUri.fsPath) - - const message = `Import '${d.data}' of '${fileName}' is out of date. Restarting the file will update it.` - const input = 'Restart File' - const choice = await window.showInformationMessage(message, input) - if (choice !== input) { - return - } - - const document = workspace.textDocuments.find(doc => doc.uri.fsPath === fileUri.fsPath) - if (!document || document.isClosed) { - void window.showErrorMessage(`'${fileName}' was closed in the meantime. File will not be restarted.`) - return - } - - await client.restartFile(document) - } - - private isKnownNotificationDiagnostic(uri: Uri, code: string, data?: string | undefined): boolean { - return this.notificationDiagnostics.get(uri.fsPath)?.get(code)?.has(data) ?? false - } - - private addNotificationDiagnostic(uri: Uri, code: string, data?: string | undefined) { - const map: Map> = this.notificationDiagnostics.get(uri.fsPath) ?? new Map() - const set = map.get(code) ?? new Set() - set.add(data) - map.set(code, set) - this.notificationDiagnostics.set(uri.fsPath, map) - } - dispose(): void { for (const s of this.subscriptions) { s.dispose(); } }