From 5875bfa614bc0b44cd2e48190f35bca4f96ee792 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Sat, 8 Mar 2025 12:29:56 +0100 Subject: [PATCH 01/36] fix: use 1ch unsolved goal padding instead of 1em (#587) I somehow reverted this by accident during testing. `1ch` of padding feels much more consistent for the unsolved goal symbol. --- vscode-lean4/src/taskgutter.ts | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/vscode-lean4/src/taskgutter.ts b/vscode-lean4/src/taskgutter.ts index 474e4dc72..20d46d114 100644 --- a/vscode-lean4/src/taskgutter.ts +++ b/vscode-lean4/src/taskgutter.ts @@ -467,14 +467,14 @@ export class LeanTaskGutter implements Disposable { after: { contentText: '🛠', color: unsolvedGoalsDecorationDarkThemeColor(), - margin: '0 0 0 1em', + margin: '0 0 0 1ch', }, }, light: { after: { contentText: '🛠', color: unsolvedGoalsDecorationLightThemeColor(), - margin: '0 0 0 1em', + margin: '0 0 0 1ch', }, }, isWholeLine: true, From ad0a17f84a6cef365c37235f5bd3ce5ef71d2728 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Sat, 8 Mar 2025 12:30:28 +0100 Subject: [PATCH 02/36] Release 0.0.197 (pre-release) --- vscode-lean4/package.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json index de845a894..a016a3027 100644 --- a/vscode-lean4/package.json +++ b/vscode-lean4/package.json @@ -2,7 +2,7 @@ "name": "lean4", "displayName": "Lean 4", "description": "Lean 4 language support for VS Code", - "version": "0.0.196", + "version": "0.0.197", "publisher": "leanprover", "engines": { "vscode": "^1.75.0" From 96d35bd98f2e7d1b574e6da8753c35268474960e Mon Sep 17 00:00:00 2001 From: Johannes Choo Date: Tue, 11 Mar 2025 16:50:21 +0800 Subject: [PATCH 03/36] =?UTF-8?q?feat:=20add=20abbreviation=20`xs`=20for?= =?UTF-8?q?=20`=C3=97=CB=A2`,=20denoting=20the=20product=20set=20(#588)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- lean4-unicode-input/src/abbreviations.json | 1 + 1 file changed, 1 insertion(+) diff --git a/lean4-unicode-input/src/abbreviations.json b/lean4-unicode-input/src/abbreviations.json index 65ae7905d..78661097e 100644 --- a/lean4-unicode-input/src/abbreviations.json +++ b/lean4-unicode-input/src/abbreviations.json @@ -1819,6 +1819,7 @@ "X": "⨯", "vectorproduct": "⨯", "crossproduct": "⨯", + "xs": "×ˢ", "coprod": "⨿", "sigmaobj": "∐", "xf": "×ᶠ", From 681200b12c7e645cfac6a42f7e9e0be998168b8e Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Tue, 11 Mar 2025 10:55:02 +0100 Subject: [PATCH 04/36] feat: expose client-side language server logging in config (#589) The language client library has a very convenient setting for tracing language server messages on the client-side, but I'm getting tired of having to edit the `settings.json` to use it. This PR exposes the client-side logging setting in the vscode-lean4 config. --- vscode-lean4/package.json | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json index a016a3027..0bc4b849e 100644 --- a/vscode-lean4/package.json +++ b/vscode-lean4/package.json @@ -95,6 +95,17 @@ "description": "an argument to pass to the server" } }, + "lean4.trace.server": { + "type": "string", + "default": "off", + "enum": [ + "off", + "messages", + "compact", + "verbose" + ], + "markdownDescription": "Whether to enable client-side logging for language server messages." + }, "lean4.serverLogging.enabled": { "type": "boolean", "default": false, From 1bbb32fc5a26a7cd253acefbeca934b24dce2693 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Tue, 11 Mar 2025 11:13:11 +0100 Subject: [PATCH 05/36] chore: bump unicode input versions and add publish action for unicode packages (#590) --- .github/workflows/on-push.yml | 12 ++++++++++++ lean4-unicode-input-component/package.json | 4 ++-- lean4-unicode-input/package.json | 2 +- package-lock.json | 14 +++++++------- vscode-lean4/package.json | 4 ++-- 5 files changed, 24 insertions(+), 12 deletions(-) diff --git a/.github/workflows/on-push.yml b/.github/workflows/on-push.yml index 8f868df54..7e61993ec 100644 --- a/.github/workflows/on-push.yml +++ b/.github/workflows/on-push.yml @@ -55,6 +55,18 @@ jobs: run: | npm publish --workspace=lean4-infoview --access=public + - name: Try publishing unicode-input + if: ${{ startsWith(github.ref, 'refs/tags/v') && !endsWith(github.ref, '-pre') && matrix.os == 'ubuntu-latest' }} + continue-on-error: true + run: | + npm publish --workspace=lean4-unicode-input --access=public + + - name: Try publishing unicode-input-component + if: ${{ startsWith(github.ref, 'refs/tags/v') && !endsWith(github.ref, '-pre') && matrix.os == 'ubuntu-latest' }} + continue-on-error: true + run: | + npm publish --workspace=lean4-unicode-input-component --access=public + - name: Package run: npm run package --workspace=lean4 if: ${{ !startsWith(github.ref, 'refs/tags/v') || !endsWith(github.ref, '-pre') }} diff --git a/lean4-unicode-input-component/package.json b/lean4-unicode-input-component/package.json index a32008b8f..1ecdc3054 100644 --- a/lean4-unicode-input-component/package.json +++ b/lean4-unicode-input-component/package.json @@ -1,6 +1,6 @@ { "name": "@leanprover/unicode-input-component", - "version": "0.1.2", + "version": "0.1.3", "description": "Typescript support for contenteditable divs with the Unicode input support of the Lean 4 theorem prover", "scripts": { "watch": "tsc --watch", @@ -14,7 +14,7 @@ ], "license": "Apache-2.0", "dependencies": { - "@leanprover/unicode-input": "^0.1.2" + "@leanprover/unicode-input": "^0.1.3" }, "devDependencies": { "typescript": "^5.4.5" diff --git a/lean4-unicode-input/package.json b/lean4-unicode-input/package.json index a682157af..a85b563dd 100644 --- a/lean4-unicode-input/package.json +++ b/lean4-unicode-input/package.json @@ -1,6 +1,6 @@ { "name": "@leanprover/unicode-input", - "version": "0.1.2", + "version": "0.1.3", "description": "Unicode input mechanism for the Lean 4 theorem prover", "scripts": { "watch": "tsc --watch", diff --git a/package-lock.json b/package-lock.json index aaefc8fc2..54294370b 100644 --- a/package-lock.json +++ b/package-lock.json @@ -76,7 +76,7 @@ }, "lean4-unicode-input": { "name": "@leanprover/unicode-input", - "version": "0.1.2", + "version": "0.1.3", "license": "Apache-2.0", "devDependencies": { "typescript": "^5.4.5" @@ -84,10 +84,10 @@ }, "lean4-unicode-input-component": { "name": "@leanprover/unicode-input-component", - "version": "0.1.2", + "version": "0.1.3", "license": "Apache-2.0", "dependencies": { - "@leanprover/unicode-input": "^0.1.2" + "@leanprover/unicode-input": "^0.1.3" }, "devDependencies": { "typescript": "^5.4.5" @@ -16903,13 +16903,13 @@ }, "vscode-lean4": { "name": "lean4", - "version": "0.0.195", + "version": "0.0.197", "license": "Apache-2.0", "dependencies": { "@leanprover/infoview": "~0.8.3", "@leanprover/infoview-api": "~0.6.0", - "@leanprover/unicode-input": "~0.1.2", - "@leanprover/unicode-input-component": "~0.1.2", + "@leanprover/unicode-input": "~0.1.3", + "@leanprover/unicode-input-component": "~0.1.3", "@vscode-elements/elements": "^1.7.1", "@vscode/codicons": "^0.0.36", "markdown-it": "^14.1.0", @@ -17034,4 +17034,4 @@ } } } -} \ No newline at end of file +} diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json index 0bc4b849e..f1308727a 100644 --- a/vscode-lean4/package.json +++ b/vscode-lean4/package.json @@ -1126,8 +1126,8 @@ "dependencies": { "@leanprover/infoview": "~0.8.3", "@leanprover/infoview-api": "~0.6.0", - "@leanprover/unicode-input": "~0.1.2", - "@leanprover/unicode-input-component": "~0.1.2", + "@leanprover/unicode-input": "~0.1.3", + "@leanprover/unicode-input-component": "~0.1.3", "@vscode/codicons": "^0.0.36", "@vscode-elements/elements": "^1.7.1", "markdown-it": "^14.1.0", From e844f6abe874fde8fda34160e82888476dd9c676 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Tue, 11 Mar 2025 11:15:27 +0100 Subject: [PATCH 06/36] Release 0.0.198 (pre-release) --- vscode-lean4/package.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json index f1308727a..d7f57b469 100644 --- a/vscode-lean4/package.json +++ b/vscode-lean4/package.json @@ -2,7 +2,7 @@ "name": "lean4", "displayName": "Lean 4", "description": "Lean 4 language support for VS Code", - "version": "0.0.197", + "version": "0.0.198", "publisher": "leanprover", "engines": { "vscode": "^1.75.0" From a58d976474fe7cd37f5d655c6447e42438b2b23b Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Wed, 19 Mar 2025 17:36:56 +0100 Subject: [PATCH 07/36] feat: adjust edit delay and make it configurable (#593) This PR makes the edit delay for the "unsolved goal" decoration adjustable for testing purposes, reduces it to 750ms and fixes a bug that caused the decoration to sometimes be displayed in the wrong location for a moment. --- vscode-lean4/package.json | 5 +++++ vscode-lean4/src/config.ts | 4 ++++ vscode-lean4/src/taskgutter.ts | 21 ++++++++++++++------- 3 files changed, 23 insertions(+), 7 deletions(-) diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json index d7f57b469..978f332ab 100644 --- a/vscode-lean4/package.json +++ b/vscode-lean4/package.json @@ -218,6 +218,11 @@ ], "default": "Double Checkmark", "markdownDescription": "Style of icon used in 'Goals accomplished' decoration." + }, + "lean4.decorationEditDelay": { + "type": "number", + "default": 750, + "markdownDescription": "Delay after an edit in milliseconds until certain editor decorations (like the 'unsolved goals' decoration) update." } } }, diff --git a/vscode-lean4/src/config.ts b/vscode-lean4/src/config.ts index 0dc885c37..bac1bdce5 100644 --- a/vscode-lean4/src/config.ts +++ b/vscode-lean4/src/config.ts @@ -129,6 +129,10 @@ export function goalsAccomplishedDecorationKind(): string { return workspace.getConfiguration('lean4').get('goalsAccomplishedDecorationKind', 'Double Checkmark') } +export function decorationEditDelay(): number { + return workspace.getConfiguration('lean4').get('decorationEditDelay', 750) +} + export function isRunningTest(): boolean { return typeof process.env.LEAN4_TEST_FOLDER === 'string' } diff --git a/vscode-lean4/src/taskgutter.ts b/vscode-lean4/src/taskgutter.ts index 20d46d114..125855b2c 100644 --- a/vscode-lean4/src/taskgutter.ts +++ b/vscode-lean4/src/taskgutter.ts @@ -13,6 +13,7 @@ import { } from 'vscode' import { DiagnosticSeverity, Range as LspRange } from 'vscode-languageclient' import { + decorationEditDelay, goalsAccomplishedDecorationKind, showDiagnosticGutterDecorations, showUnsolvedGoalsDecoration, @@ -34,9 +35,10 @@ interface DecorationState { } class LeanFileTaskGutter implements Disposable { - private readonly editDelayMs: number = 3000 + private readonly editDelayMs: number = decorationEditDelay() private timeout: NodeJS.Timeout | undefined private editDelayTimeout: NodeJS.Timeout | undefined + private lastEditTimestampMs: number | undefined private subscriptions: Disposable[] = [] private decorationStates: DecorationState[] = [] @@ -51,10 +53,7 @@ class LeanFileTaskGutter implements Disposable { private onDidChange() { clearTimeout(this.editDelayTimeout) - this.editDelayTimeout = setTimeout(() => { - this.editDelayTimeout = undefined - this.displayDecorations('EditDelayed') - }, this.editDelayMs) + this.lastEditTimestampMs = Date.now() } onDidReveal() { @@ -85,9 +84,17 @@ class LeanFileTaskGutter implements Disposable { this.displayDecorations('Instantaneous') }, ms) } - if (this.editDelayTimeout === undefined) { - this.displayDecorations('EditDelayed') + if (this.editDelayTimeout !== undefined) { + clearTimeout(this.editDelayTimeout) } + const remainingDelayMs = + this.lastEditTimestampMs !== undefined + ? Math.max(0, this.editDelayMs - (Date.now() - this.lastEditTimestampMs)) + : 0 + this.editDelayTimeout = setTimeout(() => { + this.editDelayTimeout = undefined + this.displayDecorations('EditDelayed') + }, remainingDelayMs) } private updateDecorationStates(newDecorationStates: DecorationState[]) { From bdc7471df82e096d71688594b41e8a75f67ee4e0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Wed, 19 Mar 2025 10:37:56 -0600 Subject: [PATCH 08/36] =?UTF-8?q?feat:=20add=20`\tiny`=20and=20`\miny`=20f?= =?UTF-8?q?or=20`=E2=A7=BE`=20and=20`=E2=A7=BF`=20(#591)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit These symbols are in use within combinatorial game theory, and are used in the [CGT repo](https://github.com/vihdzp/combinatorial-games). --- lean4-unicode-input/src/abbreviations.json | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/lean4-unicode-input/src/abbreviations.json b/lean4-unicode-input/src/abbreviations.json index 78661097e..0b4bec815 100644 --- a/lean4-unicode-input/src/abbreviations.json +++ b/lean4-unicode-input/src/abbreviations.json @@ -1830,5 +1830,7 @@ "goal": "⊢", "Vdash": "⊩", "Vert": "‖", - "Vvdash": "⊪" + "Vvdash": "⊪", + "tiny": "⧾", + "miny": "⧿" } From 36b777de2bf6f3333e36c86c1529ccfdcb9f0f87 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Wed, 19 Mar 2025 17:42:49 +0100 Subject: [PATCH 09/36] Release 0.0.199 (pre-release) --- vscode-lean4/package.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json index 978f332ab..97d68f484 100644 --- a/vscode-lean4/package.json +++ b/vscode-lean4/package.json @@ -2,7 +2,7 @@ "name": "lean4", "displayName": "Lean 4", "description": "Lean 4 language support for VS Code", - "version": "0.0.198", + "version": "0.0.199", "publisher": "leanprover", "engines": { "vscode": "^1.75.0" From 4a53e11c9999a9aa2bba615d85bdbd714fc6ba14 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Wed, 26 Mar 2025 09:51:08 +0100 Subject: [PATCH 10/36] feat: theme colors in 'unsolved goals' decoration (#595) This PR allows theme colors in the color settings for the 'unsolved goals' decoration and changes the default color of the 'unsolved goals' decoration to `editorInfo.foreground`. --- vscode-lean4/package.json | 8 ++++---- vscode-lean4/src/config.ts | 22 +++++++++++++++------- 2 files changed, 19 insertions(+), 11 deletions(-) diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json index 97d68f484..a596c9470 100644 --- a/vscode-lean4/package.json +++ b/vscode-lean4/package.json @@ -199,13 +199,13 @@ }, "lean4.unsolvedGoalsDecorationLightThemeColor": { "type": "string", - "default": "#1A85FF88", - "markdownDescription": "Color used in unsolved goal decorations when using a light theme." + "default": "editorInfo.foreground", + "markdownDescription": "Color used in unsolved goal decorations when using a light theme. Can either denote a CSS color or a [VS Code theme color](https://code.visualstudio.com/api/references/theme-color)." }, "lean4.unsolvedGoalsDecorationDarkThemeColor": { "type": "string", - "default": "#3794FF88", - "markdownDescription": "Color used in unsolved goal decorations when using a dark theme." + "default": "editorInfo.foreground", + "markdownDescription": "Color used in unsolved goal decorations when using a dark theme. Can either denote a CSS color or a [VS Code theme color](https://code.visualstudio.com/api/references/theme-color)." }, "lean4.goalsAccomplishedDecorationKind": { "type": "string", diff --git a/vscode-lean4/src/config.ts b/vscode-lean4/src/config.ts index bac1bdce5..e1877fb51 100644 --- a/vscode-lean4/src/config.ts +++ b/vscode-lean4/src/config.ts @@ -1,9 +1,13 @@ -import { ConfigurationTarget, workspace } from 'vscode' +import { ConfigurationTarget, ThemeColor, workspace } from 'vscode' import { elanStableChannel } from './utils/elan' import { PATH } from './utils/envPath' -// TODO: does currently not contain config options for `./abbreviation` -// so that it is easy to keep it in sync with vscode-lean. +function processConfigColor(c: string): ThemeColor | string { + if (c.match(/^(#|rgb\(|rgba\(|hsl\(|hsla\()/)) { + return c + } + return new ThemeColor(c) +} export function getPowerShellPath(): string { const windir = process.env.windir @@ -117,12 +121,16 @@ export function showUnsolvedGoalsDecoration(): boolean { return workspace.getConfiguration('lean4').get('showUnsolvedGoalsDecoration', true) } -export function unsolvedGoalsDecorationLightThemeColor(): string { - return workspace.getConfiguration('lean4').get('unsolvedGoalsDecorationLightThemeColor', '#1A85FF88') +export function unsolvedGoalsDecorationLightThemeColor(): ThemeColor | string { + return processConfigColor( + workspace.getConfiguration('lean4').get('unsolvedGoalsDecorationLightThemeColor', 'editorInfo.foreground'), + ) } -export function unsolvedGoalsDecorationDarkThemeColor(): string { - return workspace.getConfiguration('lean4').get('unsolvedGoalsDecorationDarkThemeColor', '#3794FF88') +export function unsolvedGoalsDecorationDarkThemeColor(): ThemeColor | string { + return processConfigColor( + workspace.getConfiguration('lean4').get('unsolvedGoalsDecorationDarkThemeColor', 'editorInfo.foreground'), + ) } export function goalsAccomplishedDecorationKind(): string { From 917858c48a0262ff124c42bbbe62847667d7fa12 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Wed, 26 Mar 2025 09:56:55 +0100 Subject: [PATCH 11/36] Release 0.0.200 (pre-release) --- vscode-lean4/package.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json index a596c9470..9f7a607f8 100644 --- a/vscode-lean4/package.json +++ b/vscode-lean4/package.json @@ -2,7 +2,7 @@ "name": "lean4", "displayName": "Lean 4", "description": "Lean 4 language support for VS Code", - "version": "0.0.199", + "version": "0.0.200", "publisher": "leanprover", "engines": { "vscode": "^1.75.0" From 82a347b7d406a2f23a124e772fec0dc2ea7b136f Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Thu, 27 Mar 2025 14:23:36 +0100 Subject: [PATCH 12/36] Release 0.0.201 --- vscode-lean4/package.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json index 9f7a607f8..6a5a54012 100644 --- a/vscode-lean4/package.json +++ b/vscode-lean4/package.json @@ -2,7 +2,7 @@ "name": "lean4", "displayName": "Lean 4", "description": "Lean 4 language support for VS Code", - "version": "0.0.200", + "version": "0.0.201", "publisher": "leanprover", "engines": { "vscode": "^1.75.0" From de1093ab125af5a72eb0078e91ea055d6df62379 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Sat, 29 Mar 2025 05:26:37 -0300 Subject: [PATCH 13/36] feat: add uri handler for the setup-guide (#596) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit I’m not certain whether this is the best place to add a new `registerUriHandler`. However, it's a hook for the URI `vscode://leanprover.lean4/setup-guide`, which will open the setup guide. This is useful for future documentation in the web, especially when detailing the installation process. --- vscode-lean4/src/extension.ts | 4 +++ vscode-lean4/src/utils/uriHandlerService.ts | 27 +++++++++++++++++++++ 2 files changed, 31 insertions(+) create mode 100644 vscode-lean4/src/utils/uriHandlerService.ts diff --git a/vscode-lean4/src/extension.ts b/vscode-lean4/src/extension.ts index 6f1b0a3b6..467d0dd93 100644 --- a/vscode-lean4/src/extension.ts +++ b/vscode-lean4/src/extension.ts @@ -34,6 +34,7 @@ import { } from './utils/notifs' import { PathExtensionProvider } from './utils/pathExtensionProvider' import { findLeanProjectRoot } from './utils/projectInfo' +import { UriHandlerService } from './utils/uriHandlerService' async function setLeanFeatureSetActive(isActive: boolean) { await commands.executeCommand('setContext', 'lean4.isLeanFeatureSetActive', isActive) @@ -152,6 +153,9 @@ function activateAlwaysEnabledFeatures(context: ExtensionContext): AlwaysEnabled const elanCommandProvider = new ElanCommandProvider(outputChannel) context.subscriptions.push(elanCommandProvider) + const uriHandlerService = new UriHandlerService() + context.subscriptions.push(uriHandlerService) + return { projectInitializationProvider, outputChannel, installer, fullDiagnosticsProvider, elanCommandProvider } } diff --git a/vscode-lean4/src/utils/uriHandlerService.ts b/vscode-lean4/src/utils/uriHandlerService.ts new file mode 100644 index 000000000..d51a493fb --- /dev/null +++ b/vscode-lean4/src/utils/uriHandlerService.ts @@ -0,0 +1,27 @@ +import { commands, Disposable, Uri, window } from 'vscode' + +export class UriHandlerService implements Disposable { + private subscriptions: Disposable[] = [] + + constructor() { + this.registerUriHandler() + } + + dispose(): void { + for (const s of this.subscriptions) { + s.dispose() + } + } + + private registerUriHandler() { + this.subscriptions.push( + window.registerUriHandler({ + async handleUri(uri: Uri) { + if (uri.path === '/setup-guide') { + await commands.executeCommand('lean4.docs.showSetupGuide') + } + }, + }), + ) + } +} From a56f7eadcb7047590908f836867d5d64b1bcb9fa Mon Sep 17 00:00:00 2001 From: euprunin Date: Mon, 7 Apr 2025 10:44:01 +0200 Subject: [PATCH 14/36] =?UTF-8?q?chore:=20rename=20the=20unused=20"8<"=20a?= =?UTF-8?q?bbreviation=20as=20"scissor"=20to=20fix=20subscript=20=E2=82=88?= =?UTF-8?q?=20conflict=20(#599)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Rename the unused "8<" abbreviation as "scissor". This resolves the need for an extra space when typing "\8" to get ₈, and makes "\8" = ₈ work like all other subscript digits (e.g. "\0" = ₀, "\1" = ₁). "8<" is not used in Mathlib or Lean. Co-authored-by: euprunin --- lean4-unicode-input/src/abbreviations.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean4-unicode-input/src/abbreviations.json b/lean4-unicode-input/src/abbreviations.json index 0b4bec815..669a7f830 100644 --- a/lean4-unicode-input/src/abbreviations.json +++ b/lean4-unicode-input/src/abbreviations.json @@ -579,7 +579,6 @@ "pitchfork": "⋔", "psi": "ψ", "phi": "φ", - "8<": "✂", "leqn": "≰", "leqq": "≦", "leqslant": "≤", @@ -710,6 +709,7 @@ ">~": "≳", ">>": "⟫", "root": "√", + "scissor": "✂", "ssubn": "⊄", "ssub": "⊂", "ssupn": "⊅", From 389bb4d444bb8a1ee561cf40e6cfe55d592b2c2a Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Tue, 8 Apr 2025 15:47:42 +0200 Subject: [PATCH 15/36] test: make tests more stable (#601) This PR adjusts tests that check the contents of 'All Messages' to check the content of 'Messages' instead, which (when initializing the InfoView for the first time) is sometimes subject to a race condition that makes it not display any messages. This is a known, albeit minor, issue. --- .../test/suite/bootstrap/bootstrap.test.ts | 19 ++-------- vscode-lean4/test/suite/info/info.test.ts | 32 ++++++++++------- vscode-lean4/test/suite/multi/multi.test.ts | 6 ++-- .../test/suite/restarts/restarts.test.ts | 20 ++++++----- vscode-lean4/test/suite/simple/simple.test.ts | 11 +++--- .../test/suite/toolchains/toolchain.test.ts | 12 +++---- vscode-lean4/test/suite/utils/helpers.ts | 35 +++++++++++++++++-- 7 files changed, 82 insertions(+), 53 deletions(-) diff --git a/vscode-lean4/test/suite/bootstrap/bootstrap.test.ts b/vscode-lean4/test/suite/bootstrap/bootstrap.test.ts index c5042bdce..4a06acccc 100644 --- a/vscode-lean4/test/suite/bootstrap/bootstrap.test.ts +++ b/vscode-lean4/test/suite/bootstrap/bootstrap.test.ts @@ -10,7 +10,7 @@ import { initLean4Untitled, waitForActiveClient, waitForActiveClientRunning, - waitForInfoviewHtml, + waitForInfoviewHtmlAt, } from '../utils/helpers' suite('Lean4 Bootstrap Test Suite', () => { @@ -32,20 +32,7 @@ suite('Lean4 Bootstrap Test Suite', () => { await waitForActiveClient(features.clientProvider, 120) await waitForActiveClientRunning(features.clientProvider, 300) - const hackNeeded = false - if (hackNeeded) { - // this is a hack we can do if it turns out this bootstrap test is unreliable. - // The hack would be covering a product bug, which is why we'd prefer not to use it. - // if it times out at 600 seconds then waitForInfoviewHtml prints the contents of the InfoView so we can see what happened. - // await waitForInfoviewHtml(info, expected, 10, 60000, true, async () => { - // // 60 seconds elapsed, and infoview is not updating, try and re-edit - // // the file to force the LSP to update. - // await deleteAllText(); - // await insertText('#eval Lean.versionString'); - // }); - } else { - await waitForInfoviewHtml(info, expected, 600) - } + await waitForInfoviewHtmlAt('#eval', info, expected, 600) logger.log('Lean installation is complete.') @@ -74,7 +61,7 @@ suite('Lean4 Bootstrap Test Suite', () => { assert(info, 'No InfoProvider export') logger.log('Wait for Lean nightly build server to start...') - await waitForInfoviewHtml(info, '4.0.0-nightly-', 120) + await waitForInfoviewHtmlAt('#eval', info, '4.0.0-nightly-', 120) logger.log('Lean nightly build server is running.') // make sure test is always run in predictable state, which is no file or folder open diff --git a/vscode-lean4/test/suite/info/info.test.ts b/vscode-lean4/test/suite/info/info.test.ts index 17f9027a2..e1d16a1bd 100644 --- a/vscode-lean4/test/suite/info/info.test.ts +++ b/vscode-lean4/test/suite/info/info.test.ts @@ -4,6 +4,7 @@ import * as vscode from 'vscode' import { logger } from '../../../src/utils/logger' import { assertStringInInfoview, + assertStringInInfoviewAt, clickInfoViewButton, closeActiveEditor, closeAllEditors, @@ -12,8 +13,10 @@ import { gotoPosition, initLean4Untitled, insertText, + insertTextAfter, waitForActiveEditor, waitForInfoviewHtml, + waitForInfoviewHtmlAt, waitForInfoviewNotHtml, } from '../utils/helpers' @@ -29,7 +32,7 @@ suite('InfoView Test Suite', () => { const info = features.infoProvider assert(info, 'No InfoProvider export') - await assertStringInInfoview(info, expectedEval1) + await assertStringInInfoviewAt('#eval', info, expectedEval1) logger.log('Clicking copyToComment button in InfoView') await clickInfoViewButton(info, 'copy-to-comment') @@ -50,7 +53,8 @@ suite('InfoView Test Suite', () => { const c = 77 const d = 7 - const features = await initLean4Untitled(`#eval ${a}*${b}`) + const evalLine1 = `#eval ${a}*${b}` + const features = await initLean4Untitled(evalLine1) const info = features.infoProvider assert(info, 'No InfoProvider export') @@ -61,11 +65,12 @@ suite('InfoView Test Suite', () => { await clickInfoViewButton(info, 'toggle-pinned') logger.log('Insert another couple lines and another eval') - await insertText(`\n\n/- add another unpinned eval -/\n#eval ${c}*${d}`) + const evalLine2 = `#eval ${c}*${d}` + await insertTextAfter(evalLine1, `\n\n/- add another unpinned eval -/\n${evalLine2}`) logger.log('wait for the new expression to appear') const expectedEval2 = (c * d).toString() - await assertStringInInfoview(info, expectedEval2) + await assertStringInInfoviewAt(evalLine2, info, expectedEval2) logger.log('make sure pinned expression is still there') await assertStringInInfoview(info, expectedEval1) @@ -75,7 +80,7 @@ suite('InfoView Test Suite', () => { logger.log('Make sure pinned eval is gone, but unpinned eval remains') await waitForInfoviewNotHtml(info, expectedEval1) - await assertStringInInfoview(info, expectedEval2) + await assertStringInInfoviewAt(evalLine2, info, expectedEval2) await closeAllEditors() }).timeout(60000) @@ -92,7 +97,7 @@ suite('InfoView Test Suite', () => { const info = features.infoProvider assert(info, 'No InfoProvider export') - await waitForInfoviewHtml(info, expectedEval, 30, 1000, false) + await waitForInfoviewHtmlAt('#eval', info, expectedEval, 30, 1000, false) logger.log('Pin this info') await clickInfoViewButton(info, 'toggle-pinned') @@ -106,7 +111,7 @@ suite('InfoView Test Suite', () => { logger.log('wait for the new expression to appear') const expectedEval2 = '[4, 1, 2, 3]' - await waitForInfoviewHtml(info, expectedEval2, 30, 1000, false) + await waitForInfoviewHtmlAt('#eval', info, expectedEval2, 30, 1000, false) logger.log('make sure pinned expression is not showing an error') await waitForInfoviewNotHtml(info, 'Incorrect position') @@ -116,7 +121,7 @@ suite('InfoView Test Suite', () => { editor.selection = new vscode.Selection(newLastLine.start, newLastLine.start) logger.log('make sure pinned value reverts after an undo') - await waitForInfoviewHtml(info, expectedEval, 30, 1000, false) + await waitForInfoviewHtmlAt('#eval', info, expectedEval, 30, 1000, false) await closeAllEditors() }).timeout(60000) @@ -128,21 +133,22 @@ suite('InfoView Test Suite', () => { const b = 95 const prefix = 'Lean version is:' - const features = await initLean4Untitled(`#eval ${a}*${b}`) + const evalLine = `#eval ${a}*${b}` + const features = await initLean4Untitled(evalLine) const info = features.infoProvider assert(info, 'No InfoProvider export') const expectedEval = (a * b).toString() - await assertStringInInfoview(info, expectedEval) + await assertStringInInfoviewAt('#eval', info, expectedEval) logger.log('Pin this info') await clickInfoViewButton(info, 'toggle-pinned') logger.log('Insert another eval') - await insertText('\n\n#eval s!"' + prefix + ': {Lean.versionString}"') + await insertTextAfter(evalLine, '\n\n#eval s!"' + prefix + ': {Lean.versionString}"') logger.log('make sure output of versionString is also there') - await assertStringInInfoview(info, prefix) + await assertStringInInfoviewAt('#eval s!', info, prefix) logger.log('make sure pinned expression is not showing an error') await waitForInfoviewNotHtml(info, 'Incorrect position') @@ -177,7 +183,7 @@ suite('InfoView Test Suite', () => { const info = features.infoProvider assert(info, 'No InfoProvider export') - gotoPosition(0, text.indexOf('by')) + gotoPosition('by') await assertStringInInfoview(info, 'issue461') logger.log('Opening tooltip for goal type') diff --git a/vscode-lean4/test/suite/multi/multi.test.ts b/vscode-lean4/test/suite/multi/multi.test.ts index 067371982..c44f0946b 100644 --- a/vscode-lean4/test/suite/multi/multi.test.ts +++ b/vscode-lean4/test/suite/multi/multi.test.ts @@ -4,7 +4,7 @@ import * as path from 'path' import * as vscode from 'vscode' import { logger } from '../../../src/utils/logger' import { displayNotification } from '../../../src/utils/notifs' -import { assertStringInInfoview, closeAllEditors, getAltBuildVersion, initLean4 } from '../utils/helpers' +import { assertStringInInfoviewAt, closeAllEditors, getAltBuildVersion, initLean4 } from '../utils/helpers' suite('Multi-Folder Test Suite', () => { test('Load a multi-project workspace', async () => { @@ -19,7 +19,7 @@ suite('Multi-Folder Test Suite', () => { // verify we have a nightly build running in this folder. const info = features.infoProvider assert(info, 'No InfoProvider export') - await assertStringInInfoview(info, '4.0.0-nightly-') + await assertStringInInfoviewAt('#eval Lean.versionString', info, '4.0.0-nightly-') // Now open a file from the other project const doc2 = await vscode.workspace.openTextDocument(path.join(multiRoot, 'foo', 'Foo.lean')) @@ -28,7 +28,7 @@ suite('Multi-Folder Test Suite', () => { await vscode.window.showTextDocument(doc2, options) logger.log(`wait for version ${version} to load...`) - await assertStringInInfoview(info, version) + await assertStringInInfoviewAt('#eval', info, version) // Now verify we have 2 LeanClients running. const clients = features.clientProvider diff --git a/vscode-lean4/test/suite/restarts/restarts.test.ts b/vscode-lean4/test/suite/restarts/restarts.test.ts index aeecc5ca0..7be61a433 100644 --- a/vscode-lean4/test/suite/restarts/restarts.test.ts +++ b/vscode-lean4/test/suite/restarts/restarts.test.ts @@ -7,12 +7,14 @@ import { logger } from '../../../src/utils/logger' import { displayNotification } from '../../../src/utils/notifs' import { assertStringInInfoview, + assertStringInInfoviewAt, closeAllEditors, deleteAllText, extractPhrase, initLean4, initLean4Untitled, insertText, + insertTextAfter, restartFile, restartLeanServer, waitForActiveClient, @@ -29,18 +31,19 @@ suite('Lean Server Restart Test Suite', () => { // add normal values to initialize lean4 file const hello = 'Hello World' - const features = await initLean4Untitled(`#eval "${hello}"`) + const evalLine = `#eval "${hello}"` + const features = await initLean4Untitled(evalLine) const info = features.infoProvider assert(info, 'No InfoProvider export') logger.log('make sure language server is up and running.') - await assertStringInInfoview(info, hello) + await assertStringInInfoviewAt('#eval', info, hello) const clients = features.clientProvider assert(clients, 'No LeanClientProvider export') logger.log('Insert eval that causes crash.') - await insertText('\n\n#eval (unsafeCast 0 : String)') + await insertTextAfter(evalLine, '\n\n#eval (unsafeCast 0 : String)') const expectedMessage = 'The Lean Server has stopped processing this file' await assertStringInInfoview(info, expectedMessage) @@ -60,7 +63,7 @@ suite('Lean Server Restart Test Suite', () => { await restartLeanServer(client) logger.log('checking that Hello World comes back after restart') - await assertStringInInfoview(info, hello) + await assertStringInInfoviewAt('#eval', info, hello) // make sure test is always run in predictable state, which is no file or folder open await closeAllEditors() @@ -74,18 +77,19 @@ suite('Lean Server Restart Test Suite', () => { // add normal values to initialize lean4 file const hello = 'Hello World' - const features = await initLean4Untitled(`#eval "${hello}"`) + const evalLine = `#eval "${hello}"` + const features = await initLean4Untitled(evalLine) const info = features.infoProvider assert(info, 'No InfoProvider export') logger.log('make sure language server is up and running.') - await assertStringInInfoview(info, hello) + await assertStringInInfoviewAt('#eval', info, hello) const clients = features.clientProvider assert(clients, 'No LeanClientProvider export') logger.log('Insert eval that causes crash.') - await insertText('\n\n#eval (unsafeCast 0 : String)') + await insertTextAfter(evalLine, '\n\n#eval (unsafeCast 0 : String)') const expectedMessage = 'The Lean Server has stopped processing this file' await assertStringInInfoview(info, expectedMessage) @@ -105,7 +109,7 @@ suite('Lean Server Restart Test Suite', () => { await restartFile() logger.log('checking that Hello World comes back after restart') - await assertStringInInfoview(info, hello) + await assertStringInInfoviewAt('#eval', info, hello) // make sure test is always run in predictable state, which is no file or folder open await closeAllEditors() diff --git a/vscode-lean4/test/suite/simple/simple.test.ts b/vscode-lean4/test/suite/simple/simple.test.ts index 513495504..bea9ec667 100644 --- a/vscode-lean4/test/suite/simple/simple.test.ts +++ b/vscode-lean4/test/suite/simple/simple.test.ts @@ -6,7 +6,7 @@ import { elanInstalledToolchains } from '../../../src/utils/elan' import { logger } from '../../../src/utils/logger' import { displayNotification } from '../../../src/utils/notifs' import { - assertStringInInfoview, + assertStringInInfoviewAt, closeAllEditors, extractPhrase, gotoDefinition, @@ -14,6 +14,7 @@ import { initLean4Untitled, waitForActiveEditor, waitForInfoviewHtml, + waitForInfoviewHtmlAt, } from '../utils/helpers' suite('Lean4 Basics Test Suite', () => { @@ -25,7 +26,7 @@ suite('Lean4 Basics Test Suite', () => { const info = features.infoProvider assert(info, 'No InfoProvider export') - await assertStringInInfoview(info, '4.0.0-nightly-') + await assertStringInInfoviewAt('#eval', info, '4.0.0-nightly-') // test goto definition to lean toolchain works await waitForActiveEditor() @@ -60,7 +61,7 @@ suite('Lean4 Basics Test Suite', () => { const info = features.infoProvider assert(info, 'No InfoProvider export') const expectedVersion = '5040' // the factorial function works. - const html = await waitForInfoviewHtml(info, expectedVersion) + const html = await waitForInfoviewHtmlAt('#eval factorial 7', info, expectedVersion) const installer = features.installer assert(installer, 'No LeanInstaller export') @@ -73,7 +74,7 @@ suite('Lean4 Basics Test Suite', () => { defaultToolchain = defaultToolchain.replace('/', '--') defaultToolchain = defaultToolchain.replace(':', '---') // make sure this string exists in the info view. - await waitForInfoviewHtml(info, defaultToolchain) + await waitForInfoviewHtmlAt('#eval IO.appPath', info, defaultToolchain) } // make sure test is always run in predictable state, which is no file or folder open @@ -97,7 +98,7 @@ suite('Lean4 Basics Test Suite', () => { const info = features.infoProvider assert(info, 'No InfoProvider export') let expectedVersion = 'Hello:' - let html = await waitForInfoviewHtml(info, expectedVersion) + let html = await waitForInfoviewHtmlAt('#eval main', info, expectedVersion) const versionString = extractPhrase(html, 'Hello:', '<').trim() logger.log(`>>> Found "${versionString}" in infoview`) diff --git a/vscode-lean4/test/suite/toolchains/toolchain.test.ts b/vscode-lean4/test/suite/toolchains/toolchain.test.ts index 90173bf65..76fe66ed3 100644 --- a/vscode-lean4/test/suite/toolchains/toolchain.test.ts +++ b/vscode-lean4/test/suite/toolchains/toolchain.test.ts @@ -5,12 +5,12 @@ import * as path from 'path' import { logger } from '../../../src/utils/logger' import { displayNotification } from '../../../src/utils/notifs' import { - assertStringInInfoview, + assertStringInInfoviewAt, closeAllEditors, extractPhrase, getAltBuildVersion, initLean4, - waitForInfoviewHtml, + waitForInfoviewHtmlAt, } from '../utils/helpers' // Expects to be launched with folder: ${workspaceFolder}/vscode-lean4/test/suite/simple @@ -30,11 +30,11 @@ suite('Toolchain Test Suite', () => { assert(installer, 'No LeanInstaller export') // wait for info view to show up. - await assertStringInInfoview(info, 'Hello') + await assertStringInInfoviewAt('#eval main', info, 'Hello') // verify we have a nightly build running in this folder. const expectedVersion = '4.0.0-nightly-' - const html = await waitForInfoviewHtml(info, expectedVersion) + const html = await waitForInfoviewHtmlAt('#eval main', info, expectedVersion) const foundVersion = extractPhrase(html, expectedVersion, '\n') // Now edit the lean-toolchain file. @@ -48,7 +48,7 @@ suite('Toolchain Test Suite', () => { try { logger.log(`verify that we switched to alt version ${version}`) - const html = await assertStringInInfoview(info, version) + const html = await assertStringInInfoviewAt('#eval main', info, version) // check the path to lean.exe from the `eval IO.appPath` const leanPath = extractPhrase(html, 'FilePath.mk', '<').trim() @@ -61,7 +61,7 @@ suite('Toolchain Test Suite', () => { } logger.log(`Wait for version to appear, it should be ${foundVersion}`) - await assertStringInInfoview(info, foundVersion) + await assertStringInInfoviewAt('#eval main', info, foundVersion) // make sure test is always run in predictable state, which is no file or folder open await closeAllEditors() diff --git a/vscode-lean4/test/suite/utils/helpers.ts b/vscode-lean4/test/suite/utils/helpers.ts index 14c5db816..673e9a008 100644 --- a/vscode-lean4/test/suite/utils/helpers.ts +++ b/vscode-lean4/test/suite/utils/helpers.ts @@ -90,13 +90,23 @@ export async function deleteAllText(): Promise { }) } -export function gotoPosition(line: number, character: number): void { +export function gotoPosition(searchString: string, after: boolean = false): void { const editor = vscode.window.activeTextEditor assertAndLog(editor !== undefined, 'no active editor') - const position = new vscode.Position(line, character) + const text = editor.document.getText() + let offset = text.indexOf(searchString) + if (after) { + offset += searchString.length + } + const position = editor.document.positionAt(offset) editor.selection = new vscode.Selection(position, position) } +export async function insertTextAfter(searchString: string, text: string): Promise { + gotoPosition(searchString, true) + await insertText(text) +} + export async function initLean4Untitled(contents: string): Promise { // make sure test is always run in predictable state, which is no file or folder open await closeAllEditors() @@ -371,6 +381,19 @@ export async function waitForInfoviewHtml( assertAndLog(false, `Missing "${toFind}" in infoview after ${timeout} seconds`) } +export async function waitForInfoviewHtmlAt( + positionSearchString: string, + infoView: InfoProvider, + toFind: string, + retries = 60, + delay = 1000, + expand = true, + retryHandler = nullHandler, +): Promise { + gotoPosition(positionSearchString) + return await waitForInfoviewHtml(infoView, toFind, retries, delay, expand, retryHandler) +} + export async function waitForInfoviewNotHtml( infoView: InfoProvider, toFind: string, @@ -499,6 +522,14 @@ export async function assertStringInInfoview(infoView: InfoProvider, expectedVer return await waitForInfoviewHtml(infoView, expectedVersion) } +export async function assertStringInInfoviewAt( + positionSearchString: string, + infoView: InfoProvider, + expectedVersion: string, +): Promise { + return await waitForInfoviewHtmlAt(positionSearchString, infoView, expectedVersion) +} + export async function clickInfoViewButton(info: InfoProvider, name: string): Promise { await assertStringInInfoview(info, name) let retries = 5 From 4c7cbdd533c2290c44bda5edcdc99e096ef6cde7 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Tue, 8 Apr 2025 15:47:53 +0200 Subject: [PATCH 16/36] chore: bump unicode input version (#600) --- lean4-unicode-input-component/package.json | 4 ++-- lean4-unicode-input/package.json | 2 +- package-lock.json | 12 ++++++------ vscode-lean4/package.json | 4 ++-- 4 files changed, 11 insertions(+), 11 deletions(-) diff --git a/lean4-unicode-input-component/package.json b/lean4-unicode-input-component/package.json index 1ecdc3054..52a857384 100644 --- a/lean4-unicode-input-component/package.json +++ b/lean4-unicode-input-component/package.json @@ -1,6 +1,6 @@ { "name": "@leanprover/unicode-input-component", - "version": "0.1.3", + "version": "0.1.4", "description": "Typescript support for contenteditable divs with the Unicode input support of the Lean 4 theorem prover", "scripts": { "watch": "tsc --watch", @@ -14,7 +14,7 @@ ], "license": "Apache-2.0", "dependencies": { - "@leanprover/unicode-input": "^0.1.3" + "@leanprover/unicode-input": "^0.1.4" }, "devDependencies": { "typescript": "^5.4.5" diff --git a/lean4-unicode-input/package.json b/lean4-unicode-input/package.json index a85b563dd..16644628c 100644 --- a/lean4-unicode-input/package.json +++ b/lean4-unicode-input/package.json @@ -1,6 +1,6 @@ { "name": "@leanprover/unicode-input", - "version": "0.1.3", + "version": "0.1.4", "description": "Unicode input mechanism for the Lean 4 theorem prover", "scripts": { "watch": "tsc --watch", diff --git a/package-lock.json b/package-lock.json index 54294370b..bd57f5062 100644 --- a/package-lock.json +++ b/package-lock.json @@ -76,7 +76,7 @@ }, "lean4-unicode-input": { "name": "@leanprover/unicode-input", - "version": "0.1.3", + "version": "0.1.4", "license": "Apache-2.0", "devDependencies": { "typescript": "^5.4.5" @@ -84,10 +84,10 @@ }, "lean4-unicode-input-component": { "name": "@leanprover/unicode-input-component", - "version": "0.1.3", + "version": "0.1.4", "license": "Apache-2.0", "dependencies": { - "@leanprover/unicode-input": "^0.1.3" + "@leanprover/unicode-input": "^0.1.4" }, "devDependencies": { "typescript": "^5.4.5" @@ -16903,13 +16903,13 @@ }, "vscode-lean4": { "name": "lean4", - "version": "0.0.197", + "version": "0.0.201", "license": "Apache-2.0", "dependencies": { "@leanprover/infoview": "~0.8.3", "@leanprover/infoview-api": "~0.6.0", - "@leanprover/unicode-input": "~0.1.3", - "@leanprover/unicode-input-component": "~0.1.3", + "@leanprover/unicode-input": "~0.1.4", + "@leanprover/unicode-input-component": "~0.1.4", "@vscode-elements/elements": "^1.7.1", "@vscode/codicons": "^0.0.36", "markdown-it": "^14.1.0", diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json index 6a5a54012..4c4c58396 100644 --- a/vscode-lean4/package.json +++ b/vscode-lean4/package.json @@ -1131,8 +1131,8 @@ "dependencies": { "@leanprover/infoview": "~0.8.3", "@leanprover/infoview-api": "~0.6.0", - "@leanprover/unicode-input": "~0.1.3", - "@leanprover/unicode-input-component": "~0.1.3", + "@leanprover/unicode-input": "~0.1.4", + "@leanprover/unicode-input-component": "~0.1.4", "@vscode/codicons": "^0.0.36", "@vscode-elements/elements": "^1.7.1", "markdown-it": "^14.1.0", From ccbfe24d0f9a583432d6fdff44fa0a48c8183985 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Tue, 8 Apr 2025 15:56:15 +0200 Subject: [PATCH 17/36] feat: improve decoration computation performance (#604) This PR improves the performance of the new editor decorations that were introduced in #585. Specifically, it makes the following adjustments: - The result of `workspace.getConfiguration` is cached. This VS Code API is slower than expected, so we can't call it for every single decoration. - The decoration debounce delay is increased. - The decoration debounce delay applies to 'unsolved goals' decorations as well. - The work to compute the decorations is slightly reduced. --- vscode-lean4/src/taskgutter.ts | 288 +++++++++++++++++---------------- 1 file changed, 148 insertions(+), 140 deletions(-) diff --git a/vscode-lean4/src/taskgutter.ts b/vscode-lean4/src/taskgutter.ts index 125855b2c..7e9acc7b0 100644 --- a/vscode-lean4/src/taskgutter.ts +++ b/vscode-lean4/src/taskgutter.ts @@ -61,7 +61,7 @@ class LeanFileTaskGutter implements Disposable { } onDidUpdateState(newDecorationStates: DecorationState[]) { - this.scheduleUpdate(newDecorationStates, 20) + this.scheduleUpdate(newDecorationStates, 100) } clear(clearedDecorationTypes: TextEditorDecorationType[]) { @@ -84,13 +84,11 @@ class LeanFileTaskGutter implements Disposable { this.displayDecorations('Instantaneous') }, ms) } - if (this.editDelayTimeout !== undefined) { - clearTimeout(this.editDelayTimeout) - } + clearTimeout(this.editDelayTimeout) const remainingDelayMs = this.lastEditTimestampMs !== undefined - ? Math.max(0, this.editDelayMs - (Date.now() - this.lastEditTimestampMs)) - : 0 + ? Math.max(ms, this.editDelayMs - (Date.now() - this.lastEditTimestampMs)) + : ms this.editDelayTimeout = setTimeout(() => { this.editDelayTimeout = undefined this.displayDecorations('EditDelayed') @@ -214,19 +212,7 @@ function mergeDiagnosticGutterDecos(a: DiagnosticGutterDeco, b: DiagnosticGutter } function isGoalsAccomplishedDiagnostic(d: LeanDiagnostic): boolean { - return ( - d.leanTags !== undefined && - d.leanTags.some(t => t === LeanTag.GoalsAccomplished) && - goalsAccomplishedDecorationKind() !== 'Off' - ) -} - -function isGutterDecoDiagnostic(d: LeanDiagnostic): boolean { - return ( - d.severity === DiagnosticSeverity.Error || - d.severity === DiagnosticSeverity.Warning || - isGoalsAccomplishedDiagnostic(d) - ) + return d.leanTags !== undefined && d.leanTags.some(t => t === LeanTag.GoalsAccomplished) } function determineDiagStart(d: LeanDiagnostic, startLine: number, endLine: number, line: number): DiagStart { @@ -276,29 +262,14 @@ function determineDiagnosticGutterDeco( } } -function computeDiagnosticGutterDecos(diagnostics: LeanDiagnostic[]): DiagnosticGutterDeco[] { - const decos: Map = new Map() - for (const d of diagnostics) { - if (!isGutterDecoDiagnostic(d)) { - continue - } - const range = diagRange(d) - const startLine = range.start.line - const endLine = inclusiveEndLine(range) - for (let line = startLine; line <= endLine; line++) { - const deco = determineDiagnosticGutterDeco(d, startLine, endLine, line) - const oldDeco = decos.get(deco.line) - if (oldDeco === undefined) { - decos.set(deco.line, deco) - } else { - const mergedDeco = mergeDiagnosticGutterDecos(oldDeco, deco) - decos.set(deco.line, mergedDeco) - } - } +function updateDecos(decos: Map, deco: DiagnosticGutterDeco) { + const oldDeco = decos.get(deco.line) + if (oldDeco === undefined) { + decos.set(deco.line, deco) + } else { + const mergedDeco = mergeDiagnosticGutterDecos(oldDeco, deco) + decos.set(deco.line, mergedDeco) } - const result: DiagnosticGutterDeco[] = [...decos.values()] - result.sort((a, b) => a.line - b.line) - return result } const diagnosticGutterDecoKinds = [ @@ -333,103 +304,6 @@ const diagnosticGutterDecoKinds = [ ] as const type DiagnosticGutterDecoKind = (typeof diagnosticGutterDecoKinds)[number] -function getGoalsAccomplishedDiagnosticGutterDecoKindName(): string { - const configName = goalsAccomplishedDecorationKind() - if (configName === 'Double Checkmark') { - return 'goals-accomplished-checkmark' - } - if (configName === 'Circled Checkmark') { - return 'goals-accomplished-circled-checkmark' - } - if (configName === 'Octopus') { - return 'goals-accomplished-octopus' - } - if (configName === 'Tada') { - return 'goals-accomplished-tada' - } - return 'goals-accomplished-checkmark' -} - -function determineSingleLineDiagnosticGutterDecoKind(d: DiagnosticGutterDeco, name: string): DiagnosticGutterDecoKind { - const c = d.isPreviousDiagContinue - const e = d.isPreviousDiagEnd - if (!c && !e) { - return name as DiagnosticGutterDecoKind - } - if (!c && e) { - return `${name}-l-passthrough` as DiagnosticGutterDecoKind - } - if (c && !e) { - return `${name}-i-passthrough` as DiagnosticGutterDecoKind - } - if (c && e) { - return `${name}-t-passthrough` as DiagnosticGutterDecoKind - } - assert(false) -} - -function determineDiagnosticGutterDecoKind(d: DiagnosticGutterDeco): DiagnosticGutterDecoKind | undefined { - const s = d.diagStart - const c = d.isPreviousDiagContinue - const e = d.isPreviousDiagEnd - if (s !== 'None') { - const k = s.kind - const r = s.range - if (k === 'Error') { - if (!c && !e) { - if (r === 'SingleLine') { - return 'error' - } - if (r === 'MultiLine') { - return 'error-init' - } - r satisfies never - } - if (!c && e) { - if (r === 'SingleLine') { - return 'error-l-passthrough' - } - if (r === 'MultiLine') { - return 'error-t-passthrough' - } - r satisfies never - } - if (c && !e) { - // All designs I can think of that would distinguish `SingleLine` and `MultiLine` in this case - // have too much visual complexity for the small gutter. - return 'error-i-passthrough' - } - if (c && e) { - // All designs I can think of that would distinguish `SingleLine` and `MultiLine` in this case - // have too much visual complexity for the small gutter. - return 'error-t-passthrough' - } - assert(false) - } - if (k === 'Warning') { - return determineSingleLineDiagnosticGutterDecoKind(d, 'warning') - } - if (k === 'GoalsAccomplished') { - return determineSingleLineDiagnosticGutterDecoKind(d, getGoalsAccomplishedDiagnosticGutterDecoKindName()) - } - k satisfies never - } - assert(s === 'None') - if (!c && !e) { - return undefined - } - if (!c && e) { - return 'error-l' - } - if (c && !e) { - return 'error-i' - } - if (c && e) { - return 'error-t' - } - assert(false) -} - export class LeanTaskGutter implements Disposable { private processingDecorationType: TextEditorDecorationType private fatalErrorDecorationType: TextEditorDecorationType @@ -439,6 +313,7 @@ export class LeanTaskGutter implements Disposable { private gutters: Map = new Map() private subscriptions: Disposable[] = [] private showDiagnosticGutterDecorations: boolean = true + private goalsAccomplishedDecorationKind: string private showUnsolvedGoalsDecoration: boolean = true constructor( @@ -542,6 +417,7 @@ export class LeanTaskGutter implements Disposable { errorLensExtensions.isActive && workspace.getConfiguration('errorLens').get('gutterIconsEnabled', false) this.showDiagnosticGutterDecorations = !isErrorLensGutterEnabled && showDiagnosticGutterDecorations() + this.goalsAccomplishedDecorationKind = goalsAccomplishedDecorationKind() this.showUnsolvedGoalsDecoration = showUnsolvedGoalsDecoration() if (!this.showDiagnosticGutterDecorations) { for (const gutter of this.gutters.values()) { @@ -622,9 +498,9 @@ export class LeanTaskGutter implements Disposable { decos: [], }) } - const decos = computeDiagnosticGutterDecos(diagnostics) + const decos = this.computeDiagnosticGutterDecos(diagnostics) for (const deco of decos) { - const kind = determineDiagnosticGutterDecoKind(deco) + const kind = this.determineDiagnosticGutterDecoKind(deco) if (kind === undefined) { continue } @@ -635,6 +511,138 @@ export class LeanTaskGutter implements Disposable { return [...decoStates.values()] } + computeDiagnosticGutterDecos(diagnostics: LeanDiagnostic[]): DiagnosticGutterDeco[] { + const decos: Map = new Map() + for (const d of diagnostics) { + if (!this.isGutterDecoDiagnostic(d)) { + continue + } + const range = diagRange(d) + const startLine = range.start.line + const endLine = inclusiveEndLine(range) + const startDeco = determineDiagnosticGutterDeco(d, startLine, endLine, startLine) + updateDecos(decos, startDeco) + if (startDeco.diagStart !== 'None' && startDeco.diagStart.range === 'SingleLine') { + continue + } + for (let line = startLine + 1; line <= endLine; line++) { + const deco = determineDiagnosticGutterDeco(d, startLine, endLine, line) + updateDecos(decos, deco) + } + } + const result: DiagnosticGutterDeco[] = [...decos.values()] + result.sort((a, b) => a.line - b.line) + return result + } + + isGutterDecoDiagnostic(d: LeanDiagnostic): boolean { + return ( + d.severity === DiagnosticSeverity.Error || + d.severity === DiagnosticSeverity.Warning || + (isGoalsAccomplishedDiagnostic(d) && this.goalsAccomplishedDecorationKind !== 'Off') + ) + } + + getGoalsAccomplishedDiagnosticGutterDecoKindName(): string { + const configName = this.goalsAccomplishedDecorationKind + if (configName === 'Double Checkmark') { + return 'goals-accomplished-checkmark' + } + if (configName === 'Circled Checkmark') { + return 'goals-accomplished-circled-checkmark' + } + if (configName === 'Octopus') { + return 'goals-accomplished-octopus' + } + if (configName === 'Tada') { + return 'goals-accomplished-tada' + } + return 'goals-accomplished-checkmark' + } + + determineSingleLineDiagnosticGutterDecoKind(d: DiagnosticGutterDeco, name: string): DiagnosticGutterDecoKind { + const c = d.isPreviousDiagContinue + const e = d.isPreviousDiagEnd + if (!c && !e) { + return name as DiagnosticGutterDecoKind + } + if (!c && e) { + return `${name}-l-passthrough` as DiagnosticGutterDecoKind + } + if (c && !e) { + return `${name}-i-passthrough` as DiagnosticGutterDecoKind + } + if (c && e) { + return `${name}-t-passthrough` as DiagnosticGutterDecoKind + } + assert(false) + } + + determineDiagnosticGutterDecoKind(d: DiagnosticGutterDeco): DiagnosticGutterDecoKind | undefined { + const s = d.diagStart + const c = d.isPreviousDiagContinue + const e = d.isPreviousDiagEnd + if (s !== 'None') { + const k = s.kind + const r = s.range + if (k === 'Error') { + if (!c && !e) { + if (r === 'SingleLine') { + return 'error' + } + if (r === 'MultiLine') { + return 'error-init' + } + r satisfies never + } + if (!c && e) { + if (r === 'SingleLine') { + return 'error-l-passthrough' + } + if (r === 'MultiLine') { + return 'error-t-passthrough' + } + r satisfies never + } + if (c && !e) { + // All designs I can think of that would distinguish `SingleLine` and `MultiLine` in this case + // have too much visual complexity for the small gutter. + return 'error-i-passthrough' + } + if (c && e) { + // All designs I can think of that would distinguish `SingleLine` and `MultiLine` in this case + // have too much visual complexity for the small gutter. + return 'error-t-passthrough' + } + assert(false) + } + if (k === 'Warning') { + return this.determineSingleLineDiagnosticGutterDecoKind(d, 'warning') + } + if (k === 'GoalsAccomplished') { + return this.determineSingleLineDiagnosticGutterDecoKind( + d, + this.getGoalsAccomplishedDiagnosticGutterDecoKindName(), + ) + } + k satisfies never + } + assert(s === 'None') + if (!c && !e) { + return undefined + } + if (!c && e) { + return 'error-l' + } + if (c && !e) { + return 'error-i' + } + if (c && e) { + return 'error-t' + } + assert(false) + } + private computeUnsolvedGoalsDecoState(diagnostics: LeanDiagnostic[]): DecorationState { const unsolvedGoalsLines = diagnostics .filter(d => { From c1d143d5cac836517f5f1cd7d58a507dad481f9d Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Tue, 15 Apr 2025 10:09:31 +0200 Subject: [PATCH 18/36] feat: errors for nested projects (#607) This PR makes the following adjustments: - Fix a potential bug where nested workspace folders could lead to nested language servers (i.e. in core) - Improve error reporting for nested language servers - Improve error reporting for the 'Restart File' command --- vscode-lean4/package.json | 4 +- .../src/diagnostics/setupDiagnostics.ts | 68 +++++++++++++++ vscode-lean4/src/leanclient.ts | 28 ++++++- vscode-lean4/src/utils/clientProvider.ts | 82 ++++++++++--------- vscode-lean4/src/utils/exturi.ts | 17 ++-- vscode-lean4/src/utils/internalErrors.ts | 30 ++++--- vscode-lean4/src/utils/projectInfo.ts | 8 +- 7 files changed, 166 insertions(+), 71 deletions(-) diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json index 4c4c58396..313fdc92d 100644 --- a/vscode-lean4/package.json +++ b/vscode-lean4/package.json @@ -231,13 +231,13 @@ "command": "lean4.restartServer", "category": "Lean 4", "title": "Server: Restart Server", - "description": "Restart the Lean server (for all files)." + "description": "Restarts the Lean server (for all files)." }, { "command": "lean4.stopServer", "category": "Lean 4", "title": "Server: Stop Server", - "description": "Stop the Lean server (for all files)." + "description": "Stops the Lean server (for all files)." }, { "command": "lean4.restartFile", diff --git a/vscode-lean4/src/diagnostics/setupDiagnostics.ts b/vscode-lean4/src/diagnostics/setupDiagnostics.ts index be09f94c4..4aff05a3e 100644 --- a/vscode-lean4/src/diagnostics/setupDiagnostics.ts +++ b/vscode-lean4/src/diagnostics/setupDiagnostics.ts @@ -1,6 +1,8 @@ +import path from 'path' import { SemVer } from 'semver' import { OutputChannel, commands } from 'vscode' import { ExtUri, FileUri, extUriToCwdUri } from '../utils/exturi' +import { displayInternalError } from '../utils/internalErrors' import { ToolchainUpdateMode } from '../utils/leanCmdRunner' import { LeanInstaller } from '../utils/leanInstaller' import { diagnose } from './setupDiagnoser' @@ -32,6 +34,22 @@ const ancientLean4ProjectWarningMessage = (origin: string, projectVersion: SemVe `${origin} is using a Lean 4 version (${projectVersion.toString()}) from before the first Lean 4 stable release (4.0.0). Pre-stable Lean 4 versions are increasingly less supported, so please consider updating to a newer Lean 4 version.` +const oldServerFolderContainsNewServerFolderErrorMessage = ( + folderUri: FileUri, + fileUri: FileUri, + clientFolderUri: FileUri, +) => + `Error while starting language server: The project at '${folderUri.fsPath}' of the file '${path.basename(fileUri.fsPath)}' is contained inside of another project at '${clientFolderUri.fsPath}', for which a language server is already running. +The Lean 4 VS Code extension does not support nested Lean projects.` + +const newServerFolderContainsOldServerFolderErrorMessage = ( + folderUri: FileUri, + fileUri: FileUri, + clientFolderUri: FileUri, +) => + `Error while starting language server: The project at '${folderUri.fsPath}' of the file '${path.basename(fileUri.fsPath)}' contains another project at '${clientFolderUri.fsPath}', for which a language server is already running. +The Lean 4 VS Code extension does not support nested Lean projects.` + export class SetupDiagnostics { private n: SetupNotifier @@ -163,6 +181,56 @@ export class SetupDiagnostics { } } + async checkIsNestedProjectFolder( + existingFolderUris: ExtUri[], + folderUri: ExtUri, + fileUri: ExtUri, + stopOtherServer: (folderUri: FileUri) => Promise, + ): Promise { + if (folderUri.scheme === 'untitled' || fileUri.scheme === 'untitled') { + if (existingFolderUris.some(existingFolderUri => existingFolderUri.scheme === 'untitled')) { + await displayInternalError( + 'starting language server', + 'Attempting to start new untitled language server while one already exists.', + ) + return 'Fatal' + } + return 'Fulfilled' + } + + for (const existingFolderUri of existingFolderUris) { + if (existingFolderUri.scheme !== 'file') { + continue + } + if (existingFolderUri.isInFolder(folderUri)) { + return await this.n.displaySetupErrorWithInput( + newServerFolderContainsOldServerFolderErrorMessage(folderUri, fileUri, existingFolderUri), + [ + { + input: 'Stop Other Server', + continueDisplaying: false, + action: () => stopOtherServer(existingFolderUri), + }, + ], + ) + } + if (folderUri.isInFolder(existingFolderUri)) { + return await this.n.displaySetupErrorWithInput( + oldServerFolderContainsNewServerFolderErrorMessage(folderUri, fileUri, existingFolderUri), + [ + { + input: 'Stop Other Server', + continueDisplaying: false, + action: () => stopOtherServer(existingFolderUri), + }, + ], + ) + } + } + + return 'Fulfilled' + } + async checkIsLeanVersionUpToDate( channel: OutputChannel, context: string, diff --git a/vscode-lean4/src/leanclient.ts b/vscode-lean4/src/leanclient.ts index 408a1bdd2..d8963648e 100644 --- a/vscode-lean4/src/leanclient.ts +++ b/vscode-lean4/src/leanclient.ts @@ -471,14 +471,32 @@ export class LeanClient implements Disposable { } async restartFile(leanDoc: LeanDocument): Promise { - if (this.client === undefined || !this.running) return // there was a problem starting lean server. + const extUri = leanDoc.extUri + const formattedFileName = extUri.scheme === 'file' ? path.basename(extUri.fsPath) : extUri.toString() + const formattedProjectName = + this.folderUri.scheme === 'file' ? this.folderUri.fsPath : this.folderUri.toString() + if (this.client === undefined || !this.running) { + displayNotification( + 'Error', + `Cannot restart '${formattedFileName}': The language server for the project at '${formattedProjectName}' is stopped.`, + ) + return + } - if (!this.isInFolderManagedByThisClient(leanDoc.extUri)) { + if (!this.isInFolderManagedByThisClient(extUri)) { + displayNotification( + 'Error', + `Cannot restart '${formattedFileName}': The project at '${formattedProjectName}' does not contain the file.`, + ) return } - const uri = leanDoc.extUri.toString() + const uri = extUri.toString() if (!this.openServerDocuments.delete(uri)) { + displayNotification( + 'Error', + `Cannot restart '${formattedFileName}': The file has never been opened in the language server for the project at '${formattedProjectName}'.`, + ) return } logger.log(`[LeanClient] Restarting File: ${uri}`) @@ -488,6 +506,10 @@ export class LeanClient implements Disposable { ) if (this.openServerDocuments.has(uri)) { + displayNotification( + 'Error', + `Cannot restart '${formattedFileName}': The file has already been opened in the language server for the project at '${formattedProjectName}' since initiating the restart.`, + ) return } this.openServerDocuments.add(uri) diff --git a/vscode-lean4/src/utils/clientProvider.ts b/vscode-lean4/src/utils/clientProvider.ts index e6426647c..1dd512057 100644 --- a/vscode-lean4/src/utils/clientProvider.ts +++ b/vscode-lean4/src/utils/clientProvider.ts @@ -1,11 +1,11 @@ import { LeanFileProgressProcessingInfo, ServerStoppedReason } from '@leanprover/infoview-api' import path from 'path' -import { Disposable, EventEmitter, OutputChannel, commands, workspace } from 'vscode' +import { Disposable, EventEmitter, OutputChannel, commands } from 'vscode' import { SetupDiagnostics, checkAll } from '../diagnostics/setupDiagnostics' import { PreconditionCheckResult, SetupNotificationOptions } from '../diagnostics/setupNotifs' import { LeanClient } from '../leanclient' import { LeanPublishDiagnosticsParams } from './converters' -import { ExtUri, FileUri, UntitledUri, getWorkspaceFolderUri } from './exturi' +import { ExtUri, FileUri, UntitledUri } from './exturi' import { lean } from './leanEditorProvider' import { LeanInstaller } from './leanInstaller' import { logger } from './logger' @@ -15,7 +15,10 @@ import { findLeanProjectRoot, willUseLakeServer } from './projectInfo' async function checkLean4ProjectPreconditions( channel: OutputChannel, context: string, + existingFolderUris: ExtUri[], folderUri: ExtUri, + fileUri: ExtUri, + stopOtherServer: (folderUri: FileUri) => Promise, ): Promise { const options: SetupNotificationOptions = { errorMode: { mode: 'NonModal' }, @@ -33,6 +36,7 @@ async function checkLean4ProjectPreconditions( toolchainUpdateMode: 'PromptAboutUpdate', }) }, + () => d.checkIsNestedProjectFolder(existingFolderUris, folderUri, fileUri, stopOtherServer), ) } @@ -84,29 +88,10 @@ export class LeanClientProvider implements Disposable { commands.registerCommand('lean4.restartFile', () => this.restartActiveFile()), commands.registerCommand('lean4.refreshFileDependencies', () => this.restartActiveFile()), commands.registerCommand('lean4.restartServer', () => this.restartActiveClient()), - commands.registerCommand('lean4.stopServer', () => this.stopActiveClient()), + commands.registerCommand('lean4.stopServer', () => this.stopClient(undefined)), ) this.subscriptions.push(lean.onDidOpenLeanDocument(document => this.ensureClient(document.extUri))) - - this.subscriptions.push( - workspace.onDidChangeWorkspaceFolders(event => { - // Remove all clients that are not referenced by any folder anymore - if (event.removed.length === 0) { - return - } - this.clients.forEach((client, key) => { - if (client.folderUri.scheme === 'untitled' || getWorkspaceFolderUri(client.folderUri)) { - return - } - - logger.log(`[ClientProvider] onDidChangeWorkspaceFolders removing client for ${key}`) - this.clients.delete(key) - client.dispose() - this.clientRemovedEmitter.fire(client) - }) - }), - ) } getActiveClient(): LeanClient | undefined { @@ -115,8 +100,6 @@ export class LeanClientProvider implements Disposable { } private async onInstallChanged(uri: FileUri) { - // Uri is a package Uri in the case a lean package file was changed. - logger.log(`[ClientProvider] installChanged for ${uri}`) this.pendingInstallChanged.push(uri) if (this.processingInstallChanged) { // avoid re-entrancy. @@ -135,18 +118,9 @@ export class LeanClientProvider implements Disposable { continue } - const preconditionCheckResult = await checkLean4ProjectPreconditions( - this.outputChannel, - 'Client Restart', - projectUri, - ) - if (preconditionCheckResult !== 'Fatal') { - logger.log('[ClientProvider] got lean version 4') - const [cached, client] = await this.ensureClient(uri) - if (cached && client) { - await client.restart() - logger.log('[ClientProvider] restart complete') - } + const [cached, client] = await this.ensureClient(uri) + if (cached && client) { + await client.restart() } } catch (e) { logger.log(`[ClientProvider] Exception checking lean version: ${e}`) @@ -185,9 +159,33 @@ export class LeanClientProvider implements Disposable { this.restartFile(doc.extUri) } - private async stopActiveClient() { - if (this.activeClient && this.activeClient.isStarted()) { - await this.activeClient?.stop() + private async stopClient(folderUri: ExtUri | undefined) { + let clientToStop: LeanClient + if (folderUri === undefined) { + if (this.activeClient === undefined) { + displayNotification('Error', 'Cannot stop language server: No active client.') + return + } + clientToStop = this.activeClient + } else { + const foundClient = this.getClientForFolder(folderUri) + if (foundClient === undefined) { + displayNotification( + 'Error', + `Cannot stop language server: No client for project at '${folderUri.toString()}'.`, + ) + return + } + clientToStop = foundClient + } + if (clientToStop.isStarted()) { + await clientToStop.stop() + } + const key = clientToStop.folderUri.toString() + this.clients.delete(key) + this.pending.delete(key) + if (clientToStop === this.activeClient) { + this.activeClient = undefined } } @@ -264,7 +262,13 @@ export class LeanClientProvider implements Disposable { const preconditionCheckResult = await checkLean4ProjectPreconditions( this.outputChannel, 'Client Startup', + this.getClients().map(client => client.folderUri), folderUri, + uri, + async (folderUriToStop: FileUri) => { + await this.stopClient(folderUriToStop) + await this.ensureClient(uri) + }, ) if (preconditionCheckResult === 'Fatal') { this.pending.delete(key) diff --git a/vscode-lean4/src/utils/exturi.ts b/vscode-lean4/src/utils/exturi.ts index 5ec3501be..905513d89 100644 --- a/vscode-lean4/src/utils/exturi.ts +++ b/vscode-lean4/src/utils/exturi.ts @@ -66,16 +66,15 @@ export class FileUri { } } -export function getWorkspaceFolderUri(uri: FileUri): FileUri | undefined { - const folder = workspace.getWorkspaceFolder(uri.asUri()) - if (folder === undefined) { - return undefined - } - const folderUri = FileUri.fromUri(folder.uri) - if (folderUri === undefined) { - return undefined +export function isInWorkspaceFolder(uri: FileUri): boolean { + return workspace.getWorkspaceFolder(uri.asUri()) !== undefined +} + +export function isWorkspaceFolder(uri: FileUri): boolean { + if (workspace.workspaceFolders === undefined) { + return false } - return folderUri + return workspace.workspaceFolders.some(folder => uri.equalsUri(folder.uri)) } export class UntitledUri { diff --git a/vscode-lean4/src/utils/internalErrors.ts b/vscode-lean4/src/utils/internalErrors.ts index 3cd111fd1..a71ea1e49 100644 --- a/vscode-lean4/src/utils/internalErrors.ts +++ b/vscode-lean4/src/utils/internalErrors.ts @@ -1,23 +1,27 @@ import { env } from 'vscode' import { displayNotificationWithInput } from './notifs' +export async function displayInternalError(scope: string, e: any) { + let msg: string = `Internal error (while ${scope}): ${e}` + let fullMsg: string = msg + if (e instanceof Error && e.stack !== undefined) { + fullMsg += `\n\n${e.stack}` + } + msg += + "\n\nIf you are using an up-to-date version of the Lean 4 VS Code extension, please copy the full error message using the 'Copy Error to Clipboard' button and report it at https://github.com/leanprover/vscode-lean4/ or https://leanprover.zulipchat.com/." + const copyToClipboardInput = 'Copy Error to Clipboard' + const closeInput = 'Close' + const choice = await displayNotificationWithInput('Error', msg, [copyToClipboardInput], closeInput) + if (choice === copyToClipboardInput) { + await env.clipboard.writeText(fullMsg) + } +} + export async function displayInternalErrorsIn(scope: string, f: () => Promise): Promise { try { return await f() } catch (e) { - let msg: string = `Internal error (while ${scope}): ${e}` - let fullMsg: string = msg - if (e instanceof Error && e.stack !== undefined) { - fullMsg += `\n\n${e.stack}` - } - msg += - "\n\nIf you are using an up-to-date version of the Lean 4 VS Code extension, please copy the full error message using the 'Copy Error to Clipboard' button and report it at https://github.com/leanprover/vscode-lean4/ or https://leanprover.zulipchat.com/." - const copyToClipboardInput = 'Copy Error to Clipboard' - const closeInput = 'Close' - const choice = await displayNotificationWithInput('Error', msg, [copyToClipboardInput], closeInput) - if (choice === copyToClipboardInput) { - await env.clipboard.writeText(fullMsg) - } + await displayInternalError(scope, e) throw e } } diff --git a/vscode-lean4/src/utils/projectInfo.ts b/vscode-lean4/src/utils/projectInfo.ts index d4e3a5fb9..6bedafff7 100644 --- a/vscode-lean4/src/utils/projectInfo.ts +++ b/vscode-lean4/src/utils/projectInfo.ts @@ -1,7 +1,7 @@ import * as fs from 'fs' -import { ExtUri, FileUri, getWorkspaceFolderUri } from './exturi' -import { dirExists, fileExists } from './fsHelper' import path from 'path' +import { ExtUri, FileUri, isWorkspaceFolder } from './exturi' +import { dirExists, fileExists } from './fsHelper' // Detect lean4 root directory (works for both lean4 repo and nightly distribution) @@ -42,8 +42,6 @@ export async function findLeanProjectRootInfo(uri: FileUri): Promise Date: Tue, 15 Apr 2025 10:11:23 +0200 Subject: [PATCH 19/36] Release 0.0.202 --- vscode-lean4/package.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json index 313fdc92d..0dcf60746 100644 --- a/vscode-lean4/package.json +++ b/vscode-lean4/package.json @@ -2,7 +2,7 @@ "name": "lean4", "displayName": "Lean 4", "description": "Lean 4 language support for VS Code", - "version": "0.0.201", + "version": "0.0.202", "publisher": "leanprover", "engines": { "vscode": "^1.75.0" From 17ffa265f9c8d176f5e7ca83ac675a3e9faa30ed Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Thu, 17 Apr 2025 14:27:29 +0200 Subject: [PATCH 20/36] feat: make lean files in `.lake` and `.elan` read-only (#608) This PR prevents users from accidentally editing dependencies in `.lake` and `.elan` when jumping to them, e.g. using go-to-definition. --- vscode-lean4/package.json | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json index 0dcf60746..e4c5f5650 100644 --- a/vscode-lean4/package.json +++ b/vscode-lean4/package.json @@ -1009,6 +1009,10 @@ } ], "configurationDefaults": { + "files.readonlyInclude": { + "**/.lake/**/*.lean": true, + "**/.elan/**/*.lean": true + }, "[lean4]": { "editor.unicodeHighlight.ambiguousCharacters": false, "editor.tabSize": 2, From 9cf599c7f1d5ae8e1b2672a6e142c3c6c55ecb1c Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Thu, 17 Apr 2025 14:28:51 +0200 Subject: [PATCH 21/36] feat: error when opening project that contains lakefile but no lean-toolchain (#610) This PR ensures that an error is displayed when users open a project that has a lakefile but no lean-toolchain file. --- .../src/diagnostics/fullDiagnostics.ts | 22 +++++++---- .../src/diagnostics/setupDiagnostics.ts | 5 +-- vscode-lean4/src/extension.ts | 39 +++++++------------ vscode-lean4/src/leanclient.ts | 7 ++-- vscode-lean4/src/projectinit.ts | 5 +-- vscode-lean4/src/utils/clientProvider.ts | 24 ++++++------ vscode-lean4/src/utils/configwatchservice.ts | 14 +++++-- vscode-lean4/src/utils/exturi.ts | 5 +++ vscode-lean4/src/utils/lake.ts | 3 +- vscode-lean4/src/utils/leanCmdRunner.ts | 2 +- vscode-lean4/src/utils/projectInfo.ts | 37 +++++++++--------- 11 files changed, 86 insertions(+), 77 deletions(-) diff --git a/vscode-lean4/src/diagnostics/fullDiagnostics.ts b/vscode-lean4/src/diagnostics/fullDiagnostics.ts index 0ab72590b..9beef9ff6 100644 --- a/vscode-lean4/src/diagnostics/fullDiagnostics.ts +++ b/vscode-lean4/src/diagnostics/fullDiagnostics.ts @@ -1,11 +1,11 @@ import { SemVer } from 'semver' -import { Disposable, OutputChannel, commands, env } from 'vscode' +import { commands, Disposable, env, OutputChannel } from 'vscode' import { ExecutionExitCode, ExecutionResult } from '../utils/batch' import { ElanInstalledToolchain, ElanToolchains, ElanUnresolvedToolchain } from '../utils/elan' -import { FileUri } from '../utils/exturi' +import { extUriToCwdUri, FileUri } from '../utils/exturi' import { lean } from '../utils/leanEditorProvider' import { displayNotification, displayNotificationWithInput } from '../utils/notifs' -import { findLeanProjectRoot } from '../utils/projectInfo' +import { findLeanProjectRootInfo } from '../utils/projectInfo' import { ElanDumpStateWithoutNetQueryResult, ElanVersionDiagnosis, @@ -228,17 +228,25 @@ export class FullDiagnosticsProvider implements Disposable { // in which case we still want to provide adequate diagnostics. Hence, we use the last active Lean document, // regardless of whether there is an actual `LeanClient` managing it. const lastActiveLeanDocumentUri = lean.lastActiveLeanDocument?.extUri - const projectUri = - lastActiveLeanDocumentUri !== undefined && lastActiveLeanDocumentUri.scheme === 'file' - ? await findLeanProjectRoot(lastActiveLeanDocumentUri) + const projectInfo = + lastActiveLeanDocumentUri !== undefined + ? await findLeanProjectRootInfo(lastActiveLeanDocumentUri) : undefined - if (projectUri === 'FileNotFound') { + if (projectInfo?.kind === 'FileNotFound') { displayNotification( 'Error', `Cannot display setup information for file that does not exist in the file system: ${lastActiveLeanDocumentUri}. Please choose a different file to display the setup information for.`, ) return } + if (projectInfo?.kind === 'LakefileWithoutToolchain') { + displayNotification( + 'Error', + `Cannot display setup information for file in invalid project: Project at ${projectInfo.projectRootUri} has a Lakefile, but no 'lean-toolchain' file. Please create one with the Lean version that you would like the project to use.`, + ) + return + } + const projectUri = projectInfo !== undefined ? extUriToCwdUri(projectInfo.projectRootUri) : undefined const fullDiagnostics = await performFullDiagnosis(this.outputChannel, projectUri) const formattedFullDiagnostics = formatFullDiagnostics(fullDiagnostics) const copyToClipboardInput = 'Copy to Clipboard' diff --git a/vscode-lean4/src/diagnostics/setupDiagnostics.ts b/vscode-lean4/src/diagnostics/setupDiagnostics.ts index 4aff05a3e..d0c6c38ed 100644 --- a/vscode-lean4/src/diagnostics/setupDiagnostics.ts +++ b/vscode-lean4/src/diagnostics/setupDiagnostics.ts @@ -1,4 +1,3 @@ -import path from 'path' import { SemVer } from 'semver' import { OutputChannel, commands } from 'vscode' import { ExtUri, FileUri, extUriToCwdUri } from '../utils/exturi' @@ -39,7 +38,7 @@ const oldServerFolderContainsNewServerFolderErrorMessage = ( fileUri: FileUri, clientFolderUri: FileUri, ) => - `Error while starting language server: The project at '${folderUri.fsPath}' of the file '${path.basename(fileUri.fsPath)}' is contained inside of another project at '${clientFolderUri.fsPath}', for which a language server is already running. + `Error while starting language server: The project at '${folderUri.fsPath}' of the file '${fileUri.baseName()}' is contained inside of another project at '${clientFolderUri.fsPath}', for which a language server is already running. The Lean 4 VS Code extension does not support nested Lean projects.` const newServerFolderContainsOldServerFolderErrorMessage = ( @@ -47,7 +46,7 @@ const newServerFolderContainsOldServerFolderErrorMessage = ( fileUri: FileUri, clientFolderUri: FileUri, ) => - `Error while starting language server: The project at '${folderUri.fsPath}' of the file '${path.basename(fileUri.fsPath)}' contains another project at '${clientFolderUri.fsPath}', for which a language server is already running. + `Error while starting language server: The project at '${folderUri.fsPath}' of the file '${fileUri.baseName()}' contains another project at '${clientFolderUri.fsPath}', for which a language server is already running. The Lean 4 VS Code extension does not support nested Lean projects.` export class SetupDiagnostics { diff --git a/vscode-lean4/src/extension.ts b/vscode-lean4/src/extension.ts index 467d0dd93..5b6b5a700 100644 --- a/vscode-lean4/src/extension.ts +++ b/vscode-lean4/src/extension.ts @@ -21,10 +21,10 @@ import { LeanConfigWatchService } from './utils/configwatchservice' import { ElanCommandProvider } from './utils/elanCommands' import { PATH, setProcessEnvPATH } from './utils/envPath' import { onEventWhile, withoutReentrancy } from './utils/events' -import { FileUri } from './utils/exturi' +import { ExtUri, extUriToCwdUri, FileUri } from './utils/exturi' import { displayInternalErrorsIn } from './utils/internalErrors' import { registerLeanCommandRunner } from './utils/leanCmdRunner' -import { lean, LeanEditor, registerLeanEditorProvider } from './utils/leanEditorProvider' +import { lean, registerLeanEditorProvider } from './utils/leanEditorProvider' import { LeanInstaller } from './utils/leanInstaller' import { displayActiveStickyNotification, @@ -33,37 +33,28 @@ import { setStickyNotificationActiveButHidden, } from './utils/notifs' import { PathExtensionProvider } from './utils/pathExtensionProvider' -import { findLeanProjectRoot } from './utils/projectInfo' +import { findLeanProjectRootInfo } from './utils/projectInfo' import { UriHandlerService } from './utils/uriHandlerService' async function setLeanFeatureSetActive(isActive: boolean) { await commands.executeCommand('setContext', 'lean4.isLeanFeatureSetActive', isActive) } -async function findLeanEditorProjectUri(editor: LeanEditor): Promise { - const docUri = editor.documentExtUri - const projectUri = docUri.scheme === 'file' ? await findLeanProjectRoot(docUri) : undefined - if (projectUri === 'FileNotFound') { - return 'InvalidProject' - } - return projectUri -} - -async function findOpenLeanProjectUri(): Promise { +async function findOpenLeanProjectUri(): Promise { const activeEditor = lean.activeLeanEditor if (activeEditor !== undefined) { - const projectUri = await findLeanEditorProjectUri(activeEditor) - if (projectUri !== 'InvalidProject') { - return projectUri + const info = await findLeanProjectRootInfo(activeEditor.documentExtUri) + if (info.kind !== 'FileNotFound') { + return info.projectRootUri } } // This happens if vscode starts with a lean file open // but the "Getting Started" page is active. for (const editor of lean.visibleLeanEditors) { - const projectUri = await findLeanEditorProjectUri(editor) - if (projectUri !== 'InvalidProject') { - return projectUri + const info = await findLeanProjectRootInfo(editor.documentExtUri) + if (info.kind !== 'FileNotFound') { + return info.projectRootUri } } @@ -220,12 +211,12 @@ async function tryActivatingLean4FeaturesInProject( elanCommandProvider: ElanCommandProvider, resolve: (value: Lean4EnabledFeatures) => void, d: SetupDiagnostics, - projectUri: FileUri | undefined, + projectUri: ExtUri, ) { const preconditionCheckResult = await checkLean4FeaturePreconditions( installer, 'Activate Lean 4 Extension', - projectUri, + extUriToCwdUri(projectUri), d, ) if (preconditionCheckResult === 'Fatal') { @@ -260,8 +251,8 @@ async function tryActivatingLean4Features( onEventWhile( lean.onDidRevealLeanEditor, withoutReentrancy('Continue', async editor => { - const projectUri = await findLeanEditorProjectUri(editor) - if (projectUri === 'InvalidProject') { + const info = await findLeanProjectRootInfo(editor.documentExtUri) + if (info.kind === 'FileNotFound') { return 'Continue' } await tryActivatingLean4FeaturesInProject( @@ -270,7 +261,7 @@ async function tryActivatingLean4Features( elanCommandProvider, resolve, d, - projectUri, + info.projectRootUri, ) return 'Stop' }), diff --git a/vscode-lean4/src/leanclient.ts b/vscode-lean4/src/leanclient.ts index d8963648e..57fb93602 100644 --- a/vscode-lean4/src/leanclient.ts +++ b/vscode-lean4/src/leanclient.ts @@ -43,7 +43,6 @@ import { } from './config' import { logger } from './utils/logger' // @ts-ignore -import path from 'path' import { SemVer } from 'semver' import { c2pConverter, @@ -368,7 +367,7 @@ export class LeanClient implements Disposable { return } - const fileName = fileUri.scheme === 'file' ? path.basename(fileUri.fsPath) : 'untitled' + const fileName = fileUri.scheme === 'file' ? fileUri.baseName() : 'untitled' const isImportsOutdatedError = params.diagnostics.some( d => d.severity === DiagnosticSeverity.Error && @@ -472,7 +471,7 @@ export class LeanClient implements Disposable { async restartFile(leanDoc: LeanDocument): Promise { const extUri = leanDoc.extUri - const formattedFileName = extUri.scheme === 'file' ? path.basename(extUri.fsPath) : extUri.toString() + const formattedFileName = extUri.scheme === 'file' ? extUri.baseName() : extUri.toString() const formattedProjectName = this.folderUri.scheme === 'file' ? this.folderUri.fsPath : this.folderUri.toString() if (this.client === undefined || !this.running) { @@ -592,7 +591,7 @@ export class LeanClient implements Disposable { documentSelector.pattern = `${escapedPath}/**/*` workspaceFolder = { uri: this.folderUri.asUri(), - name: path.basename(this.folderUri.fsPath), + name: this.folderUri.baseName(), index: 0, // the language client library does not actually need this index } } diff --git a/vscode-lean4/src/projectinit.ts b/vscode-lean4/src/projectinit.ts index 41b014e6f..f6ed1d819 100644 --- a/vscode-lean4/src/projectinit.ts +++ b/vscode-lean4/src/projectinit.ts @@ -14,7 +14,6 @@ import { lake } from './utils/lake' import { LeanInstaller } from './utils/leanInstaller' import { displayNotification, displayNotificationWithInput } from './utils/notifs' import { checkParentFoldersForLeanProject, isValidLeanProject } from './utils/projectInfo' -import path from 'path' const projectInitNotificationOptions: SetupNotificationOptions = { errorMode: { mode: 'NonModal' }, @@ -192,7 +191,7 @@ export class ProjectInitializationProvider implements Disposable { return 'DidNotComplete' } - const projectName: string = path.basename(projectFolder.fsPath) + const projectName: string = projectFolder.baseName() const result: ExecutionResult = await lake({ channel: this.channel, cwdUri: projectFolder, @@ -431,7 +430,7 @@ Open this project instead?` } private static async openNewFolder(projectFolder: FileUri) { - const message = `Project initialized. Open new project folder '${path.basename(projectFolder.fsPath)}'?` + const message = `Project initialized. Open new project folder '${projectFolder.baseName()}'?` const input = 'Open project folder' const choice: string | undefined = await displayNotificationWithInput('Information', message, [input]) if (choice === input) { diff --git a/vscode-lean4/src/utils/clientProvider.ts b/vscode-lean4/src/utils/clientProvider.ts index 1dd512057..6fbb0c2d6 100644 --- a/vscode-lean4/src/utils/clientProvider.ts +++ b/vscode-lean4/src/utils/clientProvider.ts @@ -1,16 +1,15 @@ import { LeanFileProgressProcessingInfo, ServerStoppedReason } from '@leanprover/infoview-api' -import path from 'path' import { Disposable, EventEmitter, OutputChannel, commands } from 'vscode' import { SetupDiagnostics, checkAll } from '../diagnostics/setupDiagnostics' import { PreconditionCheckResult, SetupNotificationOptions } from '../diagnostics/setupNotifs' import { LeanClient } from '../leanclient' import { LeanPublishDiagnosticsParams } from './converters' -import { ExtUri, FileUri, UntitledUri } from './exturi' +import { ExtUri, FileUri } from './exturi' import { lean } from './leanEditorProvider' import { LeanInstaller } from './leanInstaller' import { logger } from './logger' import { displayNotification } from './notifs' -import { findLeanProjectRoot, willUseLakeServer } from './projectInfo' +import { findLeanProjectRootInfo, willUseLakeServer } from './projectInfo' async function checkLean4ProjectPreconditions( channel: OutputChannel, @@ -113,11 +112,6 @@ export class LeanClientProvider implements Disposable { break } try { - const projectUri = await findLeanProjectRoot(uri) - if (projectUri === 'FileNotFound') { - continue - } - const [cached, client] = await this.ensureClient(uri) if (cached && client) { await client.restart() @@ -130,7 +124,7 @@ export class LeanClientProvider implements Disposable { } restartFile(uri: ExtUri) { - const fileName = uri.scheme === 'file' ? path.basename(uri.fsPath) : 'untitled file' + const fileName = uri.scheme === 'file' ? uri.baseName() : 'untitled file' const client: LeanClient | undefined = this.findClient(uri) if (!client || !client.isRunning()) { @@ -243,10 +237,18 @@ export class LeanClientProvider implements Disposable { } async ensureClient(uri: ExtUri): Promise<[boolean, LeanClient | undefined]> { - const folderUri = uri.scheme === 'file' ? await findLeanProjectRoot(uri) : new UntitledUri() - if (folderUri === 'FileNotFound') { + const projectInfo = await findLeanProjectRootInfo(uri) + if (projectInfo.kind === 'FileNotFound') { + return [false, undefined] + } + if (projectInfo.kind === 'LakefileWithoutToolchain') { + displayNotification( + 'Error', + `Project at ${projectInfo.projectRootUri} has a Lakefile, but lacks a 'lean-toolchain' file. Please create one with the Lean version that you would like the project to use.`, + ) return [false, undefined] } + const folderUri = projectInfo.projectRootUri let client = this.getClientForFolder(folderUri) if (client) { this.activeClient = client diff --git a/vscode-lean4/src/utils/configwatchservice.ts b/vscode-lean4/src/utils/configwatchservice.ts index 0d519ce3b..5233968f4 100644 --- a/vscode-lean4/src/utils/configwatchservice.ts +++ b/vscode-lean4/src/utils/configwatchservice.ts @@ -1,7 +1,7 @@ import * as path from 'path' import { Disposable, EventEmitter, Uri, window, workspace } from 'vscode' import { FileUri } from './exturi' -import { findLeanProjectInfo, findLeanProjectRoot } from './projectInfo' +import { findLeanProjectInfo, findLeanProjectRootInfo } from './projectInfo' // This service monitors the Lean package root folders for changes to any // lean-toolchail, lakefile.lean or lakefile.toml files found there. @@ -78,8 +78,12 @@ export class LeanConfigWatchService implements Disposable { // Note: just opening the file fires this event sometimes which is annoying, so // we compare the contents just to be sure and normalize whitespace so that // just adding a new line doesn't trigger the prompt. - const projectUri = await findLeanProjectRoot(fileUri) - if (projectUri === 'FileNotFound') { + const info = await findLeanProjectRootInfo(fileUri) + if ( + info.kind === 'FileNotFound' || + info.kind === 'LakefileWithoutToolchain' || + info.projectRootUri.scheme === 'untitled' + ) { return } @@ -96,7 +100,7 @@ export class LeanConfigWatchService implements Disposable { this.normalizedLakeFileContents.set(key, contents) if (raiseEvent) { // raise an event so the extension triggers handleLakeFileChanged. - this.lakeFileChangedEmitter.fire(projectUri) + this.lakeFileChangedEmitter.fire(info.projectRootUri) } } @@ -111,6 +115,8 @@ export class LeanConfigWatchService implements Disposable { const projectInfo = await findLeanProjectInfo(fileUri) if ( projectInfo.kind === 'FileNotFound' || + projectInfo.kind === 'LakefileWithoutToolchain' || + projectInfo.projectRootUri.scheme === 'untitled' || projectInfo.toolchainInfo === undefined || projectInfo.toolchainInfo.toolchain === undefined ) { diff --git a/vscode-lean4/src/utils/exturi.ts b/vscode-lean4/src/utils/exturi.ts index 905513d89..1b4259a36 100644 --- a/vscode-lean4/src/utils/exturi.ts +++ b/vscode-lean4/src/utils/exturi.ts @@ -1,3 +1,4 @@ +import path from 'path' import { Uri, workspace } from 'vscode' import { isFileInFolder, relativeFilePathInFolder } from './fsHelper' @@ -49,6 +50,10 @@ export class FileUri { return this.asUri().toString() } + baseName(): string { + return path.basename(this.fsPath) + } + join(...pathSegments: string[]): FileUri { return FileUri.fromUriOrError(Uri.joinPath(this.asUri(), ...pathSegments)) } diff --git a/vscode-lean4/src/utils/lake.ts b/vscode-lean4/src/utils/lake.ts index a139a711d..732e2fb8a 100644 --- a/vscode-lean4/src/utils/lake.ts +++ b/vscode-lean4/src/utils/lake.ts @@ -1,4 +1,3 @@ -import path from 'path' import { OutputChannel } from 'vscode' import { ExecutionExitCode, ExecutionResult } from './batch' import { FileUri } from './exturi' @@ -50,7 +49,7 @@ export class LakeRunner { } async fetchMathlibCacheForFile(projectRelativeFileUri: FileUri): Promise { - const prompt = `Fetching Mathlib build artifact cache for ${path.basename(projectRelativeFileUri.fsPath)}` + const prompt = `Fetching Mathlib build artifact cache for ${projectRelativeFileUri.baseName()}` return this.runLakeCommandWithProgress('exe', ['cache', 'get', projectRelativeFileUri.fsPath], prompt) } diff --git a/vscode-lean4/src/utils/leanCmdRunner.ts b/vscode-lean4/src/utils/leanCmdRunner.ts index a567a486a..17adaeb91 100644 --- a/vscode-lean4/src/utils/leanCmdRunner.ts +++ b/vscode-lean4/src/utils/leanCmdRunner.ts @@ -43,7 +43,7 @@ function overrideReason(activeOverride: ElanOverrideReason | undefined): string case 'Environment': return undefined case 'Manual': - return `set by \`elan override\` in folder '${path.basename(activeOverride.directoryPath.fsPath)}'` + return `set by \`elan override\` in folder '${activeOverride.directoryPath.baseName()}'` case 'ToolchainFile': return `of Lean project '${path.dirname(activeOverride.toolchainPath.fsPath)}'` case 'LeanpkgFile': diff --git a/vscode-lean4/src/utils/projectInfo.ts b/vscode-lean4/src/utils/projectInfo.ts index 6bedafff7..cf5b76a2b 100644 --- a/vscode-lean4/src/utils/projectInfo.ts +++ b/vscode-lean4/src/utils/projectInfo.ts @@ -1,6 +1,6 @@ import * as fs from 'fs' import path from 'path' -import { ExtUri, FileUri, isWorkspaceFolder } from './exturi' +import { ExtUri, FileUri, isWorkspaceFolder, UntitledUri } from './exturi' import { dirExists, fileExists } from './fsHelper' // Detect lean4 root directory (works for both lean4 repo and nightly distribution) @@ -30,17 +30,20 @@ export async function isCoreLean4Directory(path: FileUri): Promise { } type ProjectRootInfo = - | { kind: 'Success'; projectRootUri: FileUri; toolchainUri: FileUri | undefined } + | { kind: 'Success'; projectRootUri: ExtUri; toolchainUri: FileUri | undefined } | { kind: 'FileNotFound' } + | { kind: 'LakefileWithoutToolchain'; projectRootUri: FileUri; lakefileUri: FileUri } type ToolchainInfo = { uri: FileUri; toolchain: string | undefined } type ProjectInfo = - | { kind: 'Success'; projectRootUri: FileUri; toolchainInfo: ToolchainInfo | undefined } + | { kind: 'Success'; projectRootUri: ExtUri; toolchainInfo: ToolchainInfo | undefined } | { kind: 'FileNotFound' } + | { kind: 'LakefileWithoutToolchain'; projectRootUri: FileUri; lakefileUri: FileUri } // Find the root of a Lean project and the Uri for the 'lean-toolchain' file found there. -export async function findLeanProjectRootInfo(uri: FileUri): Promise { - const toolchainFileName = 'lean-toolchain' - +export async function findLeanProjectRootInfo(uri: ExtUri): Promise { + if (uri.scheme === 'untitled') { + return { kind: 'Success', projectRootUri: new UntitledUri(), toolchainUri: undefined } + } let path = uri try { if ((await fs.promises.stat(path.fsPath)).isFile()) { @@ -53,7 +56,9 @@ export async function findLeanProjectRootInfo(uri: FileUri): Promise { - const info = await findLeanProjectRootInfo(uri) - switch (info.kind) { - case 'Success': - return info.projectRootUri - case 'FileNotFound': - return 'FileNotFound' - } -} - export async function findLeanProjectInfo(uri: FileUri): Promise { const info = await findLeanProjectRootInfo(uri) switch (info.kind) { @@ -105,7 +104,9 @@ export async function findLeanProjectInfo(uri: FileUri): Promise { } return { kind: 'Success', projectRootUri: info.projectRootUri, toolchainInfo } case 'FileNotFound': - return { kind: 'FileNotFound' } + return info + case 'LakefileWithoutToolchain': + return info } } From ba0d7e491524cb816362c06c971f06ac9b1838d5 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Thu, 17 Apr 2025 14:35:15 +0200 Subject: [PATCH 22/36] Release 0.0.203 --- vscode-lean4/package.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json index e4c5f5650..0e53f77a4 100644 --- a/vscode-lean4/package.json +++ b/vscode-lean4/package.json @@ -2,7 +2,7 @@ "name": "lean4", "displayName": "Lean 4", "description": "Lean 4 language support for VS Code", - "version": "0.0.202", + "version": "0.0.203", "publisher": "leanprover", "engines": { "vscode": "^1.75.0" From 0d094aa12aaaebe89b9309433d30966d26502270 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Fri, 18 Apr 2025 14:02:07 +0200 Subject: [PATCH 23/36] feat: sorted installed toolchains (#611) This PR ensures that the installed toolchains in all commands that display them are sorted in a sensible manner. --- vscode-lean4/src/utils/elan.ts | 6 +- vscode-lean4/src/utils/elanCommands.ts | 89 +++++++++++++++++++++++++- vscode-lean4/src/utils/manifest.ts | 5 +- vscode-lean4/src/utils/semverRegex.ts | 3 + 4 files changed, 92 insertions(+), 11 deletions(-) create mode 100644 vscode-lean4/src/utils/semverRegex.ts diff --git a/vscode-lean4/src/utils/elan.ts b/vscode-lean4/src/utils/elan.ts index c26f5727f..acb9574fb 100644 --- a/vscode-lean4/src/utils/elan.ts +++ b/vscode-lean4/src/utils/elan.ts @@ -4,6 +4,7 @@ import { z, ZodTypeAny } from 'zod' import { batchExecute, batchExecuteWithProgress, ExecutionExitCode, ExecutionResult } from './batch' import { FileUri } from './exturi' import { groupByUniqueKey } from './groupBy' +import { semVerRegex } from './semverRegex' export const elanStableChannel = 'leanprover/lean4:stable' export const elanNightlyChannel = 'leanprover/lean4:nightly' @@ -14,11 +15,6 @@ export function isElanEagerResolutionVersion(version: SemVer) { return version.major >= elanEagerResolutionMajorVersion } -// Suggested at https://semver.org/#is-there-a-suggested-regular-expression-regex-to-check-a-semver-string - -const semVerRegex = - /^(0|[1-9]\d*)\.(0|[1-9]\d*)\.(0|[1-9]\d*)(?:-((?:0|[1-9]\d*|\d*[a-zA-Z-][0-9a-zA-Z-]*)(?:\.(?:0|[1-9]\d*|\d*[a-zA-Z-][0-9a-zA-Z-]*))*))?(?:\+([0-9a-zA-Z-]+(?:\.[0-9a-zA-Z-]+)*))?$/ - const elanVersionRegex = /^elan ((0|[1-9]\d*)\.(0|[1-9]\d*)\.(0|[1-9]\d*)(?:-((?:0|[1-9]\d*|\d*[a-zA-Z-][0-9a-zA-Z-]*)(?:\.(?:0|[1-9]\d*|\d*[a-zA-Z-][0-9a-zA-Z-]*))*))?(?:\+([0-9a-zA-Z-]+(?:\.[0-9a-zA-Z-]+)*))?)/ diff --git a/vscode-lean4/src/utils/elanCommands.ts b/vscode-lean4/src/utils/elanCommands.ts index 1936d5de0..3fe68eeba 100644 --- a/vscode-lean4/src/utils/elanCommands.ts +++ b/vscode-lean4/src/utils/elanCommands.ts @@ -1,4 +1,6 @@ +import assert from 'assert' import { promises } from 'fs' +import { SemVer, valid } from 'semver' import { commands, Disposable, OutputChannel, QuickPickItem, QuickPickItemKind, window } from 'vscode' import { ExecutionExitCode } from './batch' import { LeanClientProvider } from './clientProvider' @@ -27,6 +29,89 @@ function displayElanNotInstalledError() { displayNotification('Error', 'Elan is not installed.') } +type LeanToolchain = + | { kind: 'Unknown'; fullName: string } + | { kind: 'Release'; fullName: string; version: SemVer } + | { kind: 'Nightly'; fullName: string; date: Date } + | { kind: 'PRRelease'; fullName: string; pr: number } + +function parseToolchain(toolchain: string): LeanToolchain { + const releaseMatch = toolchain.match(/leanprover\/lean4:(.+)/) + if (releaseMatch) { + let version = releaseMatch[1] + if (version[0] === 'v') { + version = version.substring(1) + } + if (valid(version)) { + return { kind: 'Release', fullName: toolchain, version: new SemVer(version) } + } + } + + const nightlyMatch = toolchain.match(/leanprover\/lean4-nightly:nightly-(.+)/) + if (nightlyMatch) { + const date = new Date(nightlyMatch[1]) + if (!isNaN(date.valueOf())) { + return { kind: 'Nightly', fullName: toolchain, date } + } + } + + const prReleaseMatch = toolchain.match(/leanprover\/lean4-pr-releases:pr-release-(\d+)/) + if (prReleaseMatch) { + const pr = Number.parseInt(prReleaseMatch[1]) + return { kind: 'PRRelease', fullName: toolchain, pr } + } + + return { kind: 'Unknown', fullName: toolchain } +} + +function toolchainKindPrio(k: 'Unknown' | 'Release' | 'Nightly' | 'PRRelease'): number { + switch (k) { + case 'Unknown': + return 3 + case 'Release': + return 2 + case 'Nightly': + return 1 + case 'PRRelease': + return 0 + } +} + +function compareToolchainKinds( + k1: 'Unknown' | 'Release' | 'Nightly' | 'PRRelease', + k2: 'Unknown' | 'Release' | 'Nightly' | 'PRRelease', +): number { + return toolchainKindPrio(k1) - toolchainKindPrio(k2) +} + +function compareToolchains(t1: LeanToolchain, t2: LeanToolchain): number { + const kindComparison = compareToolchainKinds(t1.kind, t2.kind) + if (kindComparison !== 0) { + return kindComparison + } + switch (t1.kind) { + case 'Unknown': + assert(t2.kind === 'Unknown') + return -1 * t1.fullName.localeCompare(t2.fullName) + case 'Release': + assert(t2.kind === 'Release') + return t1.version.compare(t2.version) + case 'Nightly': + assert(t2.kind === 'Nightly') + return t1.date.valueOf() - t2.date.valueOf() + case 'PRRelease': + assert(t2.kind === 'PRRelease') + return t1.pr - t2.pr + } +} + +function sortToolchains(ts: string[]): string[] { + return ts + .map(t => parseToolchain(t)) + .sort((t1, t2) => -1 * compareToolchains(t1, t2)) + .map(t => t.fullName) +} + export class ElanCommandProvider implements Disposable { private subscriptions: Disposable[] = [] @@ -212,7 +297,7 @@ export class ElanCommandProvider implements Disposable { if (toolchainInfo === undefined) { return } - const installedToolchains = toolchainInfo.toolchains + const installedToolchains = sortToolchains(toolchainInfo.toolchains) if (installedToolchains.length === 0) { displayNotification('Information', 'No Lean versions installed.') return @@ -375,7 +460,7 @@ export class ElanCommandProvider implements Disposable { if (toolchainInfo === undefined) { return undefined } - const installedToolchains = toolchainInfo.toolchains + const installedToolchains = sortToolchains(toolchainInfo.toolchains) const installedToolchainIndex = new Set(installedToolchains) let stableToolchains: string[] = [] diff --git a/vscode-lean4/src/utils/manifest.ts b/vscode-lean4/src/utils/manifest.ts index dedd7d880..c2c58867f 100644 --- a/vscode-lean4/src/utils/manifest.ts +++ b/vscode-lean4/src/utils/manifest.ts @@ -3,10 +3,7 @@ import { SemVer } from 'semver' import { Uri } from 'vscode' import { z } from 'zod' import { FileUri } from './exturi' - -// Suggested at https://semver.org/#is-there-a-suggested-regular-expression-regex-to-check-a-semver-string -const semVerRegex = - /^(0|[1-9]\d*)\.(0|[1-9]\d*)\.(0|[1-9]\d*)(?:-((?:0|[1-9]\d*|\d*[a-zA-Z-][0-9a-zA-Z-]*)(?:\.(?:0|[1-9]\d*|\d*[a-zA-Z-][0-9a-zA-Z-]*))*))?(?:\+([0-9a-zA-Z-]+(?:\.[0-9a-zA-Z-]+)*))?$/ +import { semVerRegex } from './semverRegex' export interface DirectGitDependency { name: string diff --git a/vscode-lean4/src/utils/semverRegex.ts b/vscode-lean4/src/utils/semverRegex.ts new file mode 100644 index 000000000..9779ca8ac --- /dev/null +++ b/vscode-lean4/src/utils/semverRegex.ts @@ -0,0 +1,3 @@ +// Suggested at https://semver.org/#is-there-a-suggested-regular-expression-regex-to-check-a-semver-string +export const semVerRegex = + /^(0|[1-9]\d*)\.(0|[1-9]\d*)\.(0|[1-9]\d*)(?:-((?:0|[1-9]\d*|\d*[a-zA-Z-][0-9a-zA-Z-]*)(?:\.(?:0|[1-9]\d*|\d*[a-zA-Z-][0-9a-zA-Z-]*))*))?(?:\+([0-9a-zA-Z-]+(?:\.[0-9a-zA-Z-]+)*))?$/ From d310b9cc1bb8d5e34dec9843013a9c7354bf68f9 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Wed, 23 Apr 2025 12:22:11 +0200 Subject: [PATCH 24/36] feat: improve activation error when forked extension is installed (#613) Every so often, users decide that they want to get (what they believe to be) the "full" Lean experience in VS Code and install every single Lean-related extension from the VS Code marketplace. While well-intentioned, since the marketplace also contains forks of our extension, this then leads to an internal activation error when VS Code's `commands.registerCommand` API throws an exception for trying to register duplicate commands. This PR improves the error message that is displayed in this case to hint at the cause so that users are more likely to be able to fix it themselves without requiring assistance. --- vscode-lean4/src/utils/internalErrors.ts | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/vscode-lean4/src/utils/internalErrors.ts b/vscode-lean4/src/utils/internalErrors.ts index a71ea1e49..360a52cfe 100644 --- a/vscode-lean4/src/utils/internalErrors.ts +++ b/vscode-lean4/src/utils/internalErrors.ts @@ -1,5 +1,5 @@ import { env } from 'vscode' -import { displayNotificationWithInput } from './notifs' +import { displayModalNotification, displayNotificationWithInput } from './notifs' export async function displayInternalError(scope: string, e: any) { let msg: string = `Internal error (while ${scope}): ${e}` @@ -17,10 +17,21 @@ export async function displayInternalError(scope: string, e: any) { } } +const duplicateCommandError = (scope: string) => + `Error (while ${scope}): Two separate Lean 4 VS Code extensions that register the same VS Code functionality are installed. +Please uninstall or disable one of them and restart VS Code. + +The 'Lean 4' extension by the 'leanprover' organization is the only official Lean 4 VS Code extension.` + export async function displayInternalErrorsIn(scope: string, f: () => Promise): Promise { try { return await f() } catch (e) { + const msg = e.message + if (msg !== undefined && typeof msg === 'string' && msg.match(/command '.*' already exists/)) { + await displayModalNotification('Error', duplicateCommandError(scope)) + throw e + } await displayInternalError(scope, e) throw e } From 8e34c2e8172aa731518662f2957efdeabd8e3e38 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Wed, 23 Apr 2025 16:12:38 +0200 Subject: [PATCH 25/36] feat: revamp infoview options and actions (#606) This PR revamps the option and action UX of the InfoView. This work is motivated by several reports from users that they never knew that certain InfoView functionality existed, and intends to make these features more discoverable. Closes #592. Specifically, the following adjustments are made: - The filter menu was difficult to discover and users had trouble finding the 'reverse tactic state' functionality. To improve this, all goal state settings have been moved into a single 'Settings' menu that uses a standard cog icon, which should hopefully be much more recognizable. - All goal state settings are now also available in the 'Settings' submenu of the InfoView context menu. - The 'Unselect All' context menu entry is now only visible when there is something to be unselected, as is the case for other context menu entries. - All goal state settings can be persisted to the VS Code user settings with a context menu action or a button in the settings menu. Clients that do not support this functionality can hide the button in the settings menu by hiding the elements with `saveConfigButton` and `saveConfigLineBreak` classes. - The `reverseTacticState`, `showGoalNames` and `emphasizeFirstGoal` settings have been made available in the InfoView goal state settings menu. - All InfoView actions have been made available in the context menu. - The 'Copy to comment' and 'Copy to clipboard' actions have been removed. As of [vscode#206529](https://github.com/microsoft/vscode/pull/206529), copying from VS Code webviews should work correctly out-of-the-box, so there is no need for these additional buttons that may unnecessarily complicate the UI anymore. - The 'Refresh' action has been adjusted so that it is only displayed when the InfoView is paused to explicitly hint at the fact that it can be used to refresh the goal state while the InfoView is paused. Many users used to think that this was just the "Retry if InfoView is broken" button, which is practically never necessary. - The tooltips of all InfoView icons have been adjusted to be a bit more descriptive. - The `lean4.infoview.showExpectedType` setting has been deprecated in favor of the new `lean4.infoview.expectedTypeVisibility` setting, which allows hiding the expected type section entirely, as this section was reported to be confusing for students in a teaching environment.
Adjusted InfoView UI (Click to open) ![Adjusted InfoView UI](https://github.com/user-attachments/assets/3988695f-ff5b-4355-92fa-fdd62aae6cae)
New settings menu (Click to open) ![New settings menu](https://github.com/user-attachments/assets/14721d72-f9c3-423e-a642-40a1e12348a6)
New InfoView context menu (Click to open) ![New InfoView context menu](https://github.com/user-attachments/assets/e7b7b129-b74a-40f9-9fd6-63db2d4bba5e)
--- lean4-infoview-api/package.json | 2 +- lean4-infoview-api/src/infoviewApi.ts | 66 ++- lean4-infoview/package.json | 4 +- lean4-infoview/src/infoview/collapsing.tsx | 11 +- lean4-infoview/src/infoview/goals.tsx | 235 ++++++---- lean4-infoview/src/infoview/info.tsx | 112 ++++- lean4-infoview/src/infoview/messages.tsx | 42 +- lean4-infoview/src/infoview/traceExplorer.tsx | 4 +- package-lock.json | 10 +- vscode-lean4/package.json | 421 +++++++++++++++++- vscode-lean4/src/config.ts | 27 +- vscode-lean4/src/infoview.ts | 174 +++++++- vscode-lean4/test/suite/info/info.test.ts | 25 -- vscode-lean4/test/suite/simple/simple.test.ts | 2 +- 14 files changed, 950 insertions(+), 185 deletions(-) diff --git a/lean4-infoview-api/package.json b/lean4-infoview-api/package.json index 30e4a714d..e1b93efbc 100644 --- a/lean4-infoview-api/package.json +++ b/lean4-infoview-api/package.json @@ -1,6 +1,6 @@ { "name": "@leanprover/infoview-api", - "version": "0.6.0", + "version": "0.7.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 1a9ad9397..8167b7f43 100644 --- a/lean4-infoview-api/src/infoviewApi.ts +++ b/lean4-infoview-api/src/infoviewApi.ts @@ -7,6 +7,23 @@ import type { WorkspaceEdit, } from 'vscode-languageserver-protocol' +export type ExpectedTypeVisibility = 'Expanded by default' | 'Collapsed by default' | 'Hidden' + +export interface InfoviewConfig { + allErrorsOnLine: boolean + autoOpenShowsGoal: boolean + debounceTime: number + expectedTypeVisibility: ExpectedTypeVisibility + showGoalNames: boolean + emphasizeFirstGoal: boolean + reverseTacticState: boolean + hideTypeAssumptions: boolean + hideInstanceAssumptions: boolean + hideInaccessibleAssumptions: boolean + hideLetValues: boolean + showTooltipOnHover: boolean +} + /** * An insert `here` should be written exactly at the specified position, * while one `above` should go on the preceding line. @@ -15,6 +32,8 @@ export type TextInsertKind = 'here' | 'above' /** Interface that the InfoView WebView uses to talk to the hosting editor. */ export interface EditorApi { + saveConfig(config: InfoviewConfig): Promise + /** Make a request to the LSP server. */ sendClientRequest(uri: string, method: string, params: any): Promise /** Send a notification to the LSP server. */ @@ -77,25 +96,18 @@ export interface InfoviewTacticStateFilter { flags: string } -export interface InfoviewConfig { - allErrorsOnLine: boolean - autoOpenShowsGoal: boolean - debounceTime: number - showExpectedType: boolean - showGoalNames: boolean - emphasizeFirstGoal: boolean - reverseTacticState: boolean - showTooltipOnHover: boolean -} - export const defaultInfoviewConfig: InfoviewConfig = { allErrorsOnLine: true, autoOpenShowsGoal: true, debounceTime: 50, - showExpectedType: true, + expectedTypeVisibility: 'Expanded by default', showGoalNames: true, emphasizeFirstGoal: false, reverseTacticState: false, + hideTypeAssumptions: false, + hideInstanceAssumptions: false, + hideInaccessibleAssumptions: false, + hideLetValues: false, showTooltipOnHover: true, } @@ -108,7 +120,35 @@ export type InfoviewActionKind = export type InfoviewAction = { kind: InfoviewActionKind } -export type ContextMenuEntry = 'goToDefinition' | 'select' | 'unselect' | 'unselectAll' +export type ContextMenuEntry = + | 'goToDefinition' + | 'select' + | 'unselect' + | 'unselectAll' + | 'pause' + | 'unpause' + | 'pin' + | 'unpin' + | 'refresh' + | 'pauseAllMessages' + | 'unpauseAllMessages' + | 'goToPinnedLocation' + | 'goToMessageLocation' + | 'displayTargetBeforeAssumptions' + | 'displayAssumptionsBeforeTarget' + | 'hideTypeAssumptions' + | 'showTypeAssumptions' + | 'hideInstanceAssumptions' + | 'showInstanceAssumptions' + | 'hideInaccessibleAssumptions' + | 'showInaccessibleAssumptions' + | 'hideLetValues' + | 'showLetValues' + | 'hideGoalNames' + | 'showGoalNames' + | 'emphasizeFirstGoal' + | 'deemphasizeFirstGoal' + | 'saveSettings' export interface ContextMenuAction { entry: ContextMenuEntry diff --git a/lean4-infoview/package.json b/lean4-infoview/package.json index bd5b5b5aa..48dd370cc 100644 --- a/lean4-infoview/package.json +++ b/lean4-infoview/package.json @@ -1,6 +1,6 @@ { "name": "@leanprover/infoview", - "version": "0.8.3", + "version": "0.8.4", "description": "An interactive display for the Lean 4 theorem prover.", "scripts": { "watch": "rollup --config --environment NODE_ENV:development --watch", @@ -49,7 +49,7 @@ "typescript": "^5.4.5" }, "dependencies": { - "@leanprover/infoview-api": "~0.6.0", + "@leanprover/infoview-api": "~0.7.0", "@vscode/codicons": "^0.0.32", "@vscode-elements/react-elements": "^0.5.0", "es-module-lexer": "^1.5.4", diff --git a/lean4-infoview/src/infoview/collapsing.tsx b/lean4-infoview/src/infoview/collapsing.tsx index 14880cdea..90bb4a9e8 100644 --- a/lean4-infoview/src/infoview/collapsing.tsx +++ b/lean4-infoview/src/infoview/collapsing.tsx @@ -26,7 +26,7 @@ export function useIsVisible(): [(element: HTMLElement) => void, boolean] { return [node, isVisible] } -interface DetailsProps { +interface DetailsProps extends React.PropsWithoutRef> { initiallyOpen?: boolean children: [React.ReactNode, ...React.ReactNode[]] setOpenRef?: (_: React.Dispatch>) => void @@ -34,11 +34,16 @@ interface DetailsProps { /** Like `
` but can be programatically revealed using `setOpenRef`. * The first child is placed inside the `` node. */ -export function Details({ initiallyOpen, children: [summary, ...children], setOpenRef }: DetailsProps): JSX.Element { +export function Details({ + initiallyOpen, + children: [summary, ...children], + setOpenRef, + ...props +}: DetailsProps): JSX.Element { const [isOpen, setOpen] = React.useState(initiallyOpen === undefined ? false : initiallyOpen) if (setOpenRef) setOpenRef(setOpen) return ( -
+
{ diff --git a/lean4-infoview/src/infoview/goals.tsx b/lean4-infoview/src/infoview/goals.tsx index d1c91c1d8..5d5adf3a4 100644 --- a/lean4-infoview/src/infoview/goals.tsx +++ b/lean4-infoview/src/infoview/goals.tsx @@ -1,5 +1,6 @@ import { InfoviewActionKind, + InfoviewConfig, InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle, @@ -46,9 +47,13 @@ export function goalsToString(goals: InteractiveGoals): string { return goals.goals.map(goalToString).join('\n\n') } -interface GoalFilterState { +interface GoalSettingsState { /** If true reverse the list of hypotheses, if false present the order received from LSP. */ reverse: boolean + /** If true hide the names of goals, otherwise show them. */ + hideGoalNames: boolean + /** If true emphasize the first goal, otherwise don't emphasize it. */ + emphasizeFirstGoal: boolean /** If true show hypotheses that have isType=True, otherwise hide them. */ showType: boolean /** If true show hypotheses that have isInstance=True, otherwise hide them. */ @@ -59,15 +64,27 @@ interface GoalFilterState { showLetValue: boolean } +function goalSettingsStateOfConfig(config: InfoviewConfig): GoalSettingsState { + return { + reverse: config.reverseTacticState, + hideGoalNames: !config.showGoalNames, + emphasizeFirstGoal: config.emphasizeFirstGoal, + showType: !config.hideTypeAssumptions, + showInstance: !config.hideInstanceAssumptions, + showHiddenAssumption: !config.hideInaccessibleAssumptions, + showLetValue: !config.hideLetValues, + } +} + function getFilteredHypotheses( hyps: InteractiveHypothesisBundle[], - filter: GoalFilterState, + settings: GoalSettingsState, ): InteractiveHypothesisBundle[] { return hyps.reduce((acc: InteractiveHypothesisBundle[], h) => { - if (h.isInstance && !filter.showInstance) return acc - if (h.isType && !filter.showType) return acc - const names = filter.showHiddenAssumption ? h.names : h.names.filter(n => !isInaccessibleName(n)) - const hNew: InteractiveHypothesisBundle = filter.showLetValue + if (h.isInstance && !settings.showInstance) return acc + if (h.isType && !settings.showType) return acc + const names = settings.showHiddenAssumption ? h.names : h.names.filter(n => !isInaccessibleName(n)) + const hNew: InteractiveHypothesisBundle = settings.showLetValue ? { ...h, names } : { ...h, names, val: undefined } if (names.length !== 0) acc.push(hNew) @@ -181,7 +198,7 @@ function Hyp({ hyp: h, mvarId }: HypProps) { interface GoalProps { goal: InteractiveGoal - filter: GoalFilterState + settings: GoalSettingsState additionalClassNames: string } @@ -189,12 +206,12 @@ interface GoalProps { * Displays the hypotheses, target type and optional case label of a goal according to the * provided `filter`. */ export const Goal = React.memo((props: GoalProps) => { - const { goal, filter, additionalClassNames } = props + const { goal, settings, additionalClassNames } = props const config = React.useContext(ConfigContext) const prefix = goal.goalPrefix ?? '⊢ ' - const filteredList = getFilteredHypotheses(goal.hyps, filter) - const hyps = filter.reverse ? filteredList.slice().reverse() : filteredList + const filteredList = getFilteredHypotheses(goal.hyps, settings) + const hyps = settings.reverse ? filteredList.slice().reverse() : filteredList const locs = React.useContext(LocationsContext) const goalLocs = React.useMemo( () => @@ -217,12 +234,12 @@ export const Goal = React.memo((props: GoalProps) => { if (props.goal.isRemoved) cn += ' b--removed ' const children: React.ReactNode[] = [ - filter.reverse && goalLi, + settings.reverse && goalLi, hyps.map((h, i) => ), - !filter.reverse && goalLi, + !settings.reverse && goalLi, ] - if (goal.userName && config.showGoalNames) { + if (goal.userName && !settings.hideGoalNames) { return (
@@ -237,12 +254,12 @@ export const Goal = React.memo((props: GoalProps) => { interface GoalsProps { goals: InteractiveGoals - filter: GoalFilterState + settings: GoalSettingsState /** Whether or not to display the number of goals. */ displayCount: boolean } -function Goals({ goals, filter, displayCount }: GoalsProps) { +function Goals({ goals, settings, displayCount }: GoalsProps) { const nGoals = goals.goals.length const config = React.useContext(ConfigContext) if (nGoals === 0) { @@ -260,8 +277,8 @@ function Goals({ goals, filter, displayCount }: GoalsProps) { ))} @@ -295,50 +312,41 @@ export const FilteredGoals = React.memo( const ec = React.useContext(EditorContext) const config = React.useContext(ConfigContext) - const copyToCommentButton = ( - { - if (goals) void ec.copyToComment(goalsToString(goals)) - }} - title="copy state to comment" - /> - ) - - const [goalFilters, setGoalFilters] = React.useState({ - reverse: config.reverseTacticState, - showType: true, - showInstance: true, - showHiddenAssumption: true, - showLetValue: true, - }) - const sortClasses = - 'link pointer mh2 dim codicon ' + (goalFilters.reverse ? 'codicon-arrow-up ' : 'codicon-arrow-down ') - const sortButton = ( - { - setGoalFilters(s => ({ ...s, reverse: !s.reverse })) - }} - /> - ) - - const mkFilterButton = ( - filterFn: React.SetStateAction, - filledFn: (_: GoalFilterState) => boolean, + const [goalSettings, setGoalSettings] = React.useState(goalSettingsStateOfConfig(config)) + + const goalSettingsDifferFromDefaultConfig = + JSON.stringify(goalSettings) !== JSON.stringify(goalSettingsStateOfConfig(config)) + const disabledSaveStyle: React.CSSProperties = goalSettingsDifferFromDefaultConfig + ? {} + : { color: 'var(--vscode-disabledForeground)', pointerEvents: 'none' } + + const saveConfig = React.useCallback(async () => { + await ec.api.saveConfig({ + ...config, + reverseTacticState: goalSettings.reverse, + showGoalNames: !goalSettings.hideGoalNames, + emphasizeFirstGoal: goalSettings.emphasizeFirstGoal, + hideTypeAssumptions: !goalSettings.showType, + hideInstanceAssumptions: !goalSettings.showInstance, + hideInaccessibleAssumptions: !goalSettings.showHiddenAssumption, + hideLetValues: !goalSettings.showLetValue, + }) + }, [config, ec.api, goalSettings]) + + const mkSettingButton = ( + settingFn: React.SetStateAction, + filledFn: (_: GoalSettingsState) => boolean, name: string, ) => ( { - setGoalFilters(filterFn) + setGoalSettings(settingFn) }} >   @@ -348,47 +356,113 @@ export const FilteredGoals = React.memo( ) const filterMenu = ( - {mkFilterButton( + {mkSettingButton( + s => ({ ...s, reverse: !s.reverse }), + gs => gs.reverse, + 'Display target before assumptions', + )} +
+ {mkSettingButton( s => ({ ...s, showType: !s.showType }), - gf => gf.showType, - 'types', + gs => !gs.showType, + 'Hide type assumptions', )}
- {mkFilterButton( + {mkSettingButton( s => ({ ...s, showInstance: !s.showInstance }), - gf => gf.showInstance, - 'instances', + gs => !gs.showInstance, + 'Hide instance assumptions', )}
- {mkFilterButton( + {mkSettingButton( s => ({ ...s, showHiddenAssumption: !s.showHiddenAssumption }), - gf => gf.showHiddenAssumption, - 'hidden assumptions', + gs => !gs.showHiddenAssumption, + 'Hide inaccessible assumptions', )}
- {mkFilterButton( + {mkSettingButton( s => ({ ...s, showLetValue: !s.showLetValue }), - gf => gf.showLetValue, - 'let-values', + gs => !gs.showLetValue, + 'Hide let-values', + )} +
+ {mkSettingButton( + s => ({ ...s, hideGoalNames: !s.hideGoalNames }), + gs => gs.hideGoalNames, + 'Hide goal names', + )} +
+ {mkSettingButton( + s => ({ ...s, emphasizeFirstGoal: !s.emphasizeFirstGoal }), + gs => gs.emphasizeFirstGoal, + 'Emphasize first goal', )} +
+ saveConfig()} + > +   + Save current settings to default settings + ) - const isFiltered = - !goalFilters.showInstance || - !goalFilters.showType || - !goalFilters.showHiddenAssumption || - !goalFilters.showLetValue - const filterButton = ( + const settingsButton = ( - + ) + const context: { [k: string]: any } = {} + const id = React.useId() + const useContextMenuEvent = ( + name: string, + action: () => void, + isEnabled: boolean, + dependencies?: React.DependencyList, + ) => { + if (isEnabled) { + context[name + 'Id'] = id + } + useEvent(ec.events.clickedContextMenu, _ => action(), dependencies, `${name}:${id}`) + } + const useSettingsContextMenuEvent = (name: string, setting: any, isEnabled: boolean) => + useContextMenuEvent(name, () => setGoalSettings(s => ({ ...s, ...setting })), isEnabled) + + useSettingsContextMenuEvent('displayTargetBeforeAssumptions', { reverse: true }, !goalSettings.reverse) + useSettingsContextMenuEvent('displayAssumptionsBeforeTarget', { reverse: false }, goalSettings.reverse) + useSettingsContextMenuEvent('hideTypeAssumptions', { showType: false }, goalSettings.showType) + useSettingsContextMenuEvent('showTypeAssumptions', { showType: true }, !goalSettings.showType) + useSettingsContextMenuEvent('hideInstanceAssumptions', { showInstance: false }, goalSettings.showInstance) + useSettingsContextMenuEvent('showInstanceAssumptions', { showInstance: true }, !goalSettings.showInstance) + useSettingsContextMenuEvent( + 'hideInaccessibleAssumptions', + { showHiddenAssumption: false }, + goalSettings.showHiddenAssumption, + ) + useSettingsContextMenuEvent( + 'showInaccessibleAssumptions', + { showHiddenAssumption: true }, + !goalSettings.showHiddenAssumption, + ) + useSettingsContextMenuEvent('hideLetValues', { showLetValues: false }, goalSettings.showLetValue) + useSettingsContextMenuEvent('showLetValues', { showLetValues: true }, !goalSettings.showLetValue) + useSettingsContextMenuEvent('hideGoalNames', { hideGoalNames: true }, !goalSettings.hideGoalNames) + useSettingsContextMenuEvent('showGoalNames', { hideGoalNames: false }, goalSettings.hideGoalNames) + useSettingsContextMenuEvent( + 'emphasizeFirstGoal', + { emphasizeFirstGoal: true }, + !goalSettings.emphasizeFirstGoal, + ) + useSettingsContextMenuEvent( + 'deemphasizeFirstGoal', + { emphasizeFirstGoal: false }, + goalSettings.emphasizeFirstGoal, + ) + useContextMenuEvent('saveSettings', () => saveConfig(), goalSettingsDifferFromDefaultConfig, [saveConfig]) + const setOpenRef = React.useRef>>() useEvent( ec.events.requestedAction, @@ -402,7 +476,10 @@ export const FilteredGoals = React.memo( ) return ( -
+
(setOpenRef.current = r)} initiallyOpen={initiallyOpen}> <> {headerChildren} @@ -412,13 +489,11 @@ export const FilteredGoals = React.memo( e.preventDefault() }} > - {copyToCommentButton} - {sortButton} - {filterButton} + {settingsButton}
- {goals && } + {goals && }
diff --git a/lean4-infoview/src/infoview/info.tsx b/lean4-infoview/src/infoview/info.tsx index f89eda23e..b350552f6 100644 --- a/lean4-infoview/src/infoview/info.tsx +++ b/lean4-infoview/src/infoview/info.tsx @@ -80,7 +80,7 @@ const InfoStatusBar = React.memo((props: InfoStatusBarProps) => { {isPinned && !isPaused && ' (pinned)'} {!isPinned && isPaused && ' (paused)'} {isPinned && isPaused && ' (pinned and paused)'} - +