diff --git a/lean4-infoview/src/infoview/info.tsx b/lean4-infoview/src/infoview/info.tsx index 7bcd0f326..3df1298e1 100644 --- a/lean4-infoview/src/infoview/info.tsx +++ b/lean4-infoview/src/infoview/info.tsx @@ -498,6 +498,8 @@ function InfoAux(props: InfoProps) { errorString = mapRpcError(ex).message } else if (ex instanceof Error) { errorString = ex.toString() + } else if ('message' in ex && typeof ex.message === 'string') { + errorString = ex.message } else { errorString = `Unrecognized error: ${JSON.stringify(ex)}` } diff --git a/package-lock.json b/package-lock.json index 3e8ff2ee1..e6f3efb7b 100644 --- a/package-lock.json +++ b/package-lock.json @@ -17015,7 +17015,7 @@ }, "vscode-lean4": { "name": "lean4", - "version": "0.0.184", + "version": "0.0.186", "license": "Apache-2.0", "dependencies": { "@leanprover/infoview": "~0.7.0", diff --git a/vscode-lean4/manual/images/select-default-lean-version.png b/vscode-lean4/manual/images/select-default-lean-version.png new file mode 100644 index 000000000..8d076a423 Binary files /dev/null and b/vscode-lean4/manual/images/select-default-lean-version.png differ diff --git a/vscode-lean4/manual/images/select-project-lean-version.png b/vscode-lean4/manual/images/select-project-lean-version.png new file mode 100644 index 000000000..15730d978 Binary files /dev/null and b/vscode-lean4/manual/images/select-project-lean-version.png differ diff --git a/vscode-lean4/manual/images/uninstall-lean-versions.png b/vscode-lean4/manual/images/uninstall-lean-versions.png new file mode 100644 index 000000000..bd0271b05 Binary files /dev/null and b/vscode-lean4/manual/images/uninstall-lean-versions.png differ diff --git a/vscode-lean4/manual/images/update-release-channel.png b/vscode-lean4/manual/images/update-release-channel.png new file mode 100644 index 000000000..d78c344d9 Binary files /dev/null and b/vscode-lean4/manual/images/update-release-channel.png differ diff --git a/vscode-lean4/manual/manual.md b/vscode-lean4/manual/manual.md index 791a66068..56cba8983 100644 --- a/vscode-lean4/manual/manual.md +++ b/vscode-lean4/manual/manual.md @@ -39,7 +39,10 @@ This manual covers how to interact with the most recent version of Lean 4 using - [Project actions](#project-actions) - [Terminal](#terminal) 1. [Managing Lean versions](#managing-lean-versions) - - [Installing and updating Elan](#installing-and-updating-elan) + - [Elan](#elan) + - [Selecting default Lean versions](#selecting-default-lean-versions) + - [Updating Lean release channels](#updating-lean-release-channels) + - [Uninstalling Lean versions](#uninstalling-lean-versions) 1. [Finding definitions and theorems](#finding-definitions-and-theorems) - [LoogleView](#loogleview) 1. [Troubleshooting issues](#troubleshooting-issues) @@ -599,8 +602,8 @@ This section describes how to manage Lean projects using the Lean 4 VS Code exte ### Creating projects There are two project creation commands that can be accessed using the [command palette](#command-palette) or by navigating to the 'New Project…' submenu in the [command menu](#command-menu): -1. **['Project: Create Standalone Project…'](command:lean4.project.createStandaloneProject)**. This command will create a new Lean 4 project with the name specified in the folder creation dialog and without any additional dependencies. It will use the `leanprover/lean4:stable` toolchain for the Lean version of the project, initialize a [Git](https://git-scm.com/) repository and create an initial commit with all the files in the fresh project. -1. **['Project: Create Project Using Mathlib…'](command:lean4.project.createMathlibProject)**. This command will create a new Lean 4 project with the name specified in the folder creation dialog that depends on Lean's math library, [Mathlib](https://github.com/leanprover-community/mathlib4). It will use Mathlib's Lean toolchain for the Lean version of the project, download and install the current Mathlib build artifact cache, initialize a [Git](https://git-scm.com/) repository and create an initial commit with all the files in the fresh project. +1. **['Project: Create Standalone Project…'](command:lean4.project.createStandaloneProject)**. This command will create a new Lean 4 project with the name specified in the folder creation dialog and without any additional dependencies. It will use the `leanprover/lean4:stable` Lean release channel for the Lean version of the project, initialize a [Git](https://git-scm.com/) repository and create an initial commit with all the files in the fresh project. +1. **['Project: Create Project Using Mathlib…'](command:lean4.project.createMathlibProject)**. This command will create a new Lean 4 project with the name specified in the folder creation dialog that depends on Lean's math library, [Mathlib](https://github.com/leanprover-community/mathlib4). It will use Mathlib's Lean version for the project, download and install the current Mathlib build artifact cache, initialize a [Git](https://git-scm.com/) repository and create an initial commit with all the files in the fresh project. ### Opening projects @@ -613,9 +616,10 @@ There are two commands to open existing Lean projects that can be accessed using The Lean 4 VS Code extension supports the following commands that can be run in existing Lean projects and that can be accessed using the [command palette](#command-palette) or by navigating to the 'Project Actions…' submenu in the [command menu](#command-menu): 1. **['Project: Build Project'](command:lean4.project.build)**. Builds the full Lean project. If the project is Lean's math library [Mathlib](https://github.com/leanprover-community/mathlib4) or depends on it, it will also download and install the current Mathlib build artifact cache before trying to build the project. 1. **['Project: Clean Project'](command:lean4.project.clean)**. Removes all build artifacts for the Lean project. If the project is [Mathlib](https://github.com/leanprover-community/mathlib4) or depends on it, it will also offer to download and install the current Mathlib build artifact cache after cleaning the project. -1. **['Project: Update Dependency…'](command:lean4.project.updateDependency)**. Displays a list of all dependencies that can be updated. After selecting a dependency and updating it, if the project is [Mathlib](https://github.com/leanprover-community/mathlib4) or depends on it, it will also download and install the current Mathlib build artifact cache. At the end, if the Lean toolchain of the updated project differs from the Lean toolchain of the project, the command will offer to update the Lean toolchain of the project to that of the updated dependency. +1. **['Project: Update Dependency…'](command:lean4.project.updateDependency)**. Displays a list of all dependencies that can be updated. After selecting a dependency and updating it, if the project is [Mathlib](https://github.com/leanprover-community/mathlib4) or depends on it, it will also download and install the current Mathlib build artifact cache. At the end, if the Lean version of the updated project differs from the Lean version of the project, the command will offer to update the Lean version of the project to that of the updated dependency. 1. **['Project: Fetch Mathlib Build Cache'](command:lean4.project.fetchCache)**. Downloads and installs the current Mathlib build artifact cache if the project is [Mathlib](https://github.com/leanprover-community/mathlib4) or depends on it. 1. **['Project: Fetch Mathlib Build Cache For Current Imports'](command:lean4.project.fetchFileCache)**. Downloads and installs the current Mathlib build artifact for the focused file and all of its imports if the project is [Mathlib](https://github.com/leanprover-community/mathlib4). +1. **['Project: Select Project Lean Version…'](command:lean4.project.selectProjectToolchain)**. Displays a list of all available Lean versions. After selecting a Lean version, the command writes the selected Lean version to the `lean-toolchain` file of the given project.
@@ -623,6 +627,12 @@ The Lean 4 VS Code extension supports the following commands that can be run in | :--: | | *'Project: Update Dependency…' selection dialog* | +
+ +| ![](images/select-project-lean-version.png) | +| :--: | +| *'Project: Select Project Lean Version…' selection dialog* | + ### Terminal If the commands provided by the Lean 4 VS Code extension are not sufficient to manage the Lean project, then a built-in VS Code terminal can be launched by calling the ['Terminal: Create New Terminal'](command:workbench.action.terminal.new) command or by pressing ``` Ctrl+Shift+` ``` (``` Cmd+Shift+` ```). In this terminal, all [Lake](https://github.com/leanprover/lean4/blob/master/src/lake/README.md) commands can be executed. @@ -637,11 +647,56 @@ If the commands provided by the Lean 4 VS Code extension are not sufficient to m ## Managing Lean versions -This section covers how to manage different Lean versions. All of these commands provide a frontend for Lean's version manager [Elan](https://github.com/leanprover/elan/blob/master/README.md). At the moment, the VS Code extension does not support many Elan commands yet. +This section covers how to manage different Lean versions. All of these commands provide a frontend for Lean's version manager [Elan](https://github.com/leanprover/elan/blob/master/README.md) and can be found using the [command palette](#command-palette) or by navigating to the 'Version Management…' submenu in the [command menu](#command-menu). + +### Elan + +[Elan](https://github.com/leanprover/elan/blob/master/README.md) is Lean's version manager. It automatically installs Lean versions when a Lean command like `lean` or `lake` is used depending on the current working directory of the command. + +When used inside of a Lean project with a `lean-toolchain` file, Elan will use the Lean version denoted in the `lean-toolchain` file. Outside of a Lean project, Elan will use the default Lean version that can be configured using the `elan default ` command. + +Lean versions can either be specific Lean versions, like `leanprover/lean4:v4.14.0`, or release channels, like `leanprover/lean4:stable`, which is Elan's default Lean version when Elan is first installed. Elan's release channels resolve to the most recent specific Lean version in a given release channel. +Before Elan 4.0.0, release channels were explicitly installed in Elan, would resolve to the most recent version at the point of installation and could be manually updated to the most recent version in the release channel using the `elan toolchain update ` command. +Since Elan 4.0.0, release channels cannot be installed anymore, but whenever they are used anywhere, e.g. when running `lean` with a default Lean version of `leanprover/lean4:stable`, they will automatically resolve to the most recent Lean version for that release channel. This means that since Elan 4.0.0, release channels are updated on-the-go and do not need to be kept up-to-date manually. When Elan cannot resolve a release channel, e.g. because the machine it runs on has no network connection, it will attempt to fall back to the last installed Lean version of that release channel. + +Before Elan 4.0.0, the Lean 4 VS Code extension would always automatically install missing Lean versions as it encountered them by using Elan in exactly the same way as it works on the command line. +Since Elan 4.0.0, the Lean 4 VS Code extension now has a 'Lean 4: Always Ask Before Installing Lean Versions' setting that can be enabled to issue a confirmation prompt every time before a Lean version is installed by Elan. Additionally, regardless of this setting, the Lean 4 VS Code extension will always issue a confirmation prompt when opening a Lean file that is using a release channel for its version if there is a new Lean version for the release channel available. + +### Selecting default Lean versions + +Elan's default Lean version can be selected using the ['Setup: Select Default Lean Version…'](command:lean4.setup.selectDefaultToolchain) command. The command queries all installed Lean version and fetches all available Lean versions from [https://release.lean-lang.org/](https://release.lean-lang.org/) to present them in a selection dialog. + +
+ +| ![](images/select-default-lean-version.png) | +| :--: | +| *'Setup: Select Default Lean Version…' selection dialog* | + +### Updating Lean release channels + +The newest versions of the `leanprover/lean4:stable` and `leanprover/lean4:nightly` release channels can be installed manually using the 'Setup: Update Release Channel Lean Version…' command. The command uses Elan to resolve `leanprover/lean4:stable` and `leanprover/lean4:nightly` to determine their most recent versions and displays them in a selection dialog if an update for the respective Lean release channel is available. + +
+ +| ![](images/update-release-channel.png) | +| :--: | +| *'Setup: Update Release Channel Lean Version…' selection dialog* | + +### Uninstalling Lean versions + +Installed Lean versions can be uninstalled using the 'Setup: Uninstall Lean Versions…' command. The command determines all unused Lean versions using Elan's Lean version garbage collector and displays a selection dialog for uninstalling all unused Lean versions, as well as additional individual Lean versions and the projects they are used in. + +
+ +| ![](images/uninstall-lean-versions.png) | +| :--: | +| *'Setup: Uninstall Lean Versions……' selection dialog* | + +### Installing, updating and uninstalling Elan -### Installing and updating Elan +Elan can be installed using the ['Setup: Install Elan'](command:lean4.setup.installElan) command. Similarly, the ['Setup: Update Elan'](command:lean4.setup.updateElan) command can be used to update Elan to the newest version and the ['Setup: Uninstall Elan'](command:lean4.setup.uninstallElan) command can be used to remove Elan and all installed Lean versions from the machine. -Lean's version manager [Elan](https://github.com/leanprover/elan/blob/master/README.md) can be installed or updated using the ['Setup: Install Elan'](command:lean4.setup.installElan) command that can be found using the [command palette](#command-palette) or by navigating to the 'Version Management…' submenu in the [command menu](#command-menu). +After installing Elan or updating it from a pre-4.0.0 version, the Lean 4 VS Code extension will also prompt users about whether they want to set the ['Lean 4: Always Ask Before Installing Lean Versions' setting](#elan). --- @@ -702,7 +757,7 @@ Executing the ['Troubleshooting: Show Setup Information'](command:lean4.troubles 1. Whether Lean's version manager [Elan](https://github.com/leanprover/elan/blob/master/README.md) is installed and reasonably up-to-date, as well as the Elan version 1. Whether Lean is installed and reasonably up-to-date, as well as the Lean version 1. Whether a Lean project with a lean-toolchain has been opened, as well as the path to the project -1. Available Elan toolchains +1. Available Elan Lean versions The output is formatted using Markdown and will produce a nicely rendered output when copied to a Markdown-supporting tool, e.g. [the Lean Zulip](https://leanprover.zulipchat.com). diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json index a95eae3f9..8658421a9 100644 --- a/vscode-lean4/package.json +++ b/vscode-lean4/package.json @@ -81,6 +81,11 @@ "description": "Entry to add to the PATH variable" } }, + "lean4.alwaysAskBeforeInstallingLeanVersions": { + "type": "boolean", + "default": false, + "markdownDescription": "Enable to display a confirmation prompt whenever Elan is about to download and install a new Lean version. Needs Elan >= 4.0.0." + }, "lean4.serverArgs": { "type": "array", "default": [], @@ -320,6 +325,36 @@ "title": "Setup: Install Elan", "description": "Install Lean's version manager 'Elan'" }, + { + "command": "lean4.setup.updateElan", + "category": "Lean 4", + "title": "Setup: Update Elan", + "description": "Update Lean's version manager 'Elan' to the most recent version" + }, + { + "command": "lean4.setup.uninstallElan", + "category": "Lean 4", + "title": "Setup: Uninstall Elan", + "description": "Uninstall Lean's version manager 'Elan' and all installed Lean versions" + }, + { + "command": "lean4.setup.selectDefaultToolchain", + "category": "Lean 4", + "title": "Setup: Select Default Lean Version…", + "description": "Sets a given Lean version to be the default for non-project files and command-line operations outside of projects" + }, + { + "command": "lean4.setup.updateReleaseChannel", + "category": "Lean 4", + "title": "Setup: Update Release Channel Lean Version…", + "description": "Updates the Lean version for a given release channel" + }, + { + "command": "lean4.setup.uninstallToolchains", + "category": "Lean 4", + "title": "Setup: Uninstall Lean Versions…", + "description": "Uninstalls given Lean versions" + }, { "command": "lean4.project.createStandaloneProject", "category": "Lean 4", @@ -373,6 +408,12 @@ "category": "Lean 4", "title": "Project: Fetch Mathlib Build Cache For Current Imports", "description": "Downloads cached Mathlib build artifacts of the focused file and all of its imports to avoid full elaboration" + }, + { + "command": "lean4.project.selectProjectToolchain", + "category": "Lean 4", + "title": "Project: Select Project Lean Version…", + "description": "Updates the 'lean-toolchain' file of the currently focused project with a given Lean version" } ], "languages": [ @@ -583,6 +624,21 @@ { "command": "lean4.setup.installElan" }, + { + "command": "lean4.setup.updateElan" + }, + { + "command": "lean4.setup.uninstallElan" + }, + { + "command": "lean4.setup.selectDefaultToolchain" + }, + { + "command": "lean4.setup.updateReleaseChannel" + }, + { + "command": "lean4.setup.uninstallToolchains" + }, { "command": "lean4.project.createStandaloneProject" }, @@ -614,6 +670,10 @@ { "command": "lean4.project.fetchFileCache", "when": "lean4.isLeanFeatureSetActive" + }, + { + "command": "lean4.project.selectProjectToolchain", + "when": "lean4.isLeanFeatureSetActive" } ], "editor/title": [ @@ -715,10 +775,35 @@ } ], "lean4.titlebar.versions": [ + { + "command": "lean4.setup.selectDefaultToolchain", + "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive", + "group": "1_toolchains@1" + }, + { + "command": "lean4.setup.updateReleaseChannel", + "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive", + "group": "1_toolchains@2" + }, + { + "command": "lean4.setup.uninstallToolchains", + "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive", + "group": "1_toolchains@3" + }, { "command": "lean4.setup.installElan", "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive", - "group": "1_setup@1" + "group": "2_elan@1" + }, + { + "command": "lean4.setup.updateElan", + "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive", + "group": "2_elan@2" + }, + { + "command": "lean4.setup.uninstallElan", + "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive", + "group": "2_elan@3" } ], "lean4.titlebar.projectActions": [ @@ -746,6 +831,11 @@ "command": "lean4.project.fetchFileCache", "when": "lean4.isLeanFeatureSetActive", "group": "2_mathlibActions@2" + }, + { + "command": "lean4.project.selectProjectToolchain", + "when": "lean4.isLeanFeatureSetActive", + "group": "3_projectToolchains@1" } ], "lean4.titlebar.documentation": [ diff --git a/vscode-lean4/src/config.ts b/vscode-lean4/src/config.ts index 94a71a2a4..305ab4bdf 100644 --- a/vscode-lean4/src/config.ts +++ b/vscode-lean4/src/config.ts @@ -1,4 +1,5 @@ -import { workspace } from 'vscode' +import { ConfigurationTarget, workspace } from 'vscode' +import { elanStableChannel } from './utils/elan' import { PATH } from './utils/envPath' // TODO: does currently not contain config options for `./abbreviation` @@ -17,6 +18,20 @@ export function envPathExtensions(): PATH { return new PATH(workspace.getConfiguration('lean4').get('envPathExtensions', [])) } +export function alwaysAskBeforeInstallingLeanVersions(): boolean { + return workspace.getConfiguration('lean4').get('alwaysAskBeforeInstallingLeanVersions', false) +} + +export async function setAlwaysAskBeforeInstallingLeanVersions(alwaysAskBeforeInstallingLeanVersions: boolean) { + await workspace + .getConfiguration('lean4') + .update( + 'alwaysAskBeforeInstallingLeanVersions', + alwaysAskBeforeInstallingLeanVersions, + ConfigurationTarget.Global, + ) +} + export function serverArgs(): string[] { return workspace.getConfiguration('lean4').get('serverArgs', []) } @@ -105,7 +120,7 @@ export function getTestFolder(): string { export function getDefaultLeanVersion(): string { return typeof process.env.DEFAULT_LEAN_TOOLCHAIN === 'string' ? process.env.DEFAULT_LEAN_TOOLCHAIN - : 'leanprover/lean4:stable' + : elanStableChannel } /** The editor line height, in pixels. */ diff --git a/vscode-lean4/src/diagnostics/fullDiagnostics.ts b/vscode-lean4/src/diagnostics/fullDiagnostics.ts index 0f268c940..0ab72590b 100644 --- a/vscode-lean4/src/diagnostics/fullDiagnostics.ts +++ b/vscode-lean4/src/diagnostics/fullDiagnostics.ts @@ -1,11 +1,13 @@ import { SemVer } from 'semver' import { Disposable, OutputChannel, commands, env } from 'vscode' import { ExecutionExitCode, ExecutionResult } from '../utils/batch' +import { ElanInstalledToolchain, ElanToolchains, ElanUnresolvedToolchain } from '../utils/elan' import { FileUri } from '../utils/exturi' import { lean } from '../utils/leanEditorProvider' import { displayNotification, displayNotificationWithInput } from '../utils/notifs' import { findLeanProjectRoot } from '../utils/projectInfo' import { + ElanDumpStateWithoutNetQueryResult, ElanVersionDiagnosis, LeanVersionDiagnosis, ProjectSetupDiagnosis, @@ -24,6 +26,7 @@ export type FullDiagnostics = { leanVersionDiagnosis: LeanVersionDiagnosis projectSetupDiagnosis: ProjectSetupDiagnosis elanShowOutput: ExecutionResult + elanDumpStateOutput: ElanDumpStateWithoutNetQueryResult } function formatCommandOutput(cmdOutput: string): string { @@ -62,6 +65,8 @@ function formatLeanVersionDiagnosis(d: LeanVersionDiagnosis): string { return `Pre-stable-release Lean 4 version (version: ${d.version})` case 'ExecutionError': return 'Execution error: ' + formatCommandOutput(d.message) + case 'Cancelled': + return 'Operation cancelled' case 'NotInstalled': return 'Not installed' } @@ -92,6 +97,74 @@ function formatElanShowOutput(r: ExecutionResult): string { return formatCommandOutput(r.stdout) } +function formatElanActiveToolchain(r: ElanToolchains): string { + if (r.activeOverride !== undefined) { + const toolchain = r.activeOverride.unresolved + const overrideReason = r.activeOverride.reason + let formattedOverrideReason: string + switch (overrideReason.kind) { + case 'Environment': + formattedOverrideReason = 'set by `ELAN_TOOLCHAIN`' + break + case 'Manual': + formattedOverrideReason = `set by \`elan override\` in \`${overrideReason.directoryPath}\`` + break + case 'ToolchainFile': + formattedOverrideReason = `set by \`${overrideReason.toolchainPath}\`` + break + case 'LeanpkgFile': + formattedOverrideReason = `set by Leanpkg file in \`${overrideReason.leanpkgPath}\`` + break + case 'ToolchainDirectory': + formattedOverrideReason = `of core toolchain directory at \`${overrideReason.directoryPath}\`` + break + } + return `${ElanUnresolvedToolchain.toolchainName(toolchain)} (${formattedOverrideReason})` + } + if (r.default !== undefined) { + return `${ElanUnresolvedToolchain.toolchainName(r.default.unresolved)} (default Lean version)` + } + return 'No active Lean version' +} + +function formatElanInstalledToolchains(toolchains: Map) { + const installed = [...toolchains.values()].map(t => t.resolvedName) + if (installed.length > 20) { + return `${installed.slice(0, 20).join(', ')} ...` + } + return installed.join(', ') +} + +function formatElanDumpState(r: ElanDumpStateWithoutNetQueryResult): string { + if (r.kind === 'ElanNotFound') { + return '**Elan**: Elan not installed' + } + if (r.kind === 'ExecutionError') { + return `**Elan**: Execution error: ${r.message}` + } + if (r.kind === 'PreEagerResolutionVersion') { + return '**Elan**: Pre-4.0.0 version' + } + r.kind satisfies 'Success' + const stateDump = r.state + return [ + `**Active Lean version**: ${formatElanActiveToolchain(stateDump.toolchains)}`, + `**Installed Lean versions**: ${formatElanInstalledToolchains(stateDump.toolchains.installed)}`, + ].join('\n') +} + +function formatElanInfo(d: FullDiagnostics): string { + if (d.elanDumpStateOutput.kind === 'PreEagerResolutionVersion') { + return [ + '', + '-------------------------------------', + '', + `**Elan toolchains**: ${formatElanShowOutput(d.elanShowOutput)}`, + ].join('\n') + } + return formatElanDumpState(d.elanDumpStateOutput) +} + export function formatFullDiagnostics(d: FullDiagnostics): string { return [ `**Operating system**: ${d.systemInfo.operatingSystem}`, @@ -106,10 +179,7 @@ export function formatFullDiagnostics(d: FullDiagnostics): string { `**Elan**: ${formatElanVersionDiagnosis(d.elanVersionDiagnosis)}`, `**Lean**: ${formatLeanVersionDiagnosis(d.leanVersionDiagnosis)}`, `**Project**: ${formatProjectSetupDiagnosis(d.projectSetupDiagnosis)}`, - '', - '-------------------------------------', - '', - `**Elan toolchains**: ${formatElanShowOutput(d.elanShowOutput)}`, + formatElanInfo(d), ].join('\n') } @@ -117,8 +187,12 @@ export async function performFullDiagnosis( channel: OutputChannel, cwdUri: FileUri | undefined, ): Promise { - const showSetupInformationContext = 'Show Setup Information' - const diagnose = new SetupDiagnoser(channel, cwdUri) + const diagnose = new SetupDiagnoser({ + channel, + cwdUri, + context: 'Show Setup Information', + toolchainUpdateMode: 'DoNotUpdate', + }) return { systemInfo: diagnose.querySystemInformation(), vscodeVersionDiagnosis: diagnose.queryVSCodeVersion(), @@ -126,9 +200,10 @@ export async function performFullDiagnosis( isCurlAvailable: await diagnose.checkCurlAvailable(), isGitAvailable: await diagnose.checkGitAvailable(), elanVersionDiagnosis: await diagnose.elanVersion(), - leanVersionDiagnosis: await diagnose.leanVersion(showSetupInformationContext), + leanVersionDiagnosis: await diagnose.leanVersion(), projectSetupDiagnosis: await diagnose.projectSetup(), elanShowOutput: await diagnose.queryElanShow(), + elanDumpStateOutput: await diagnose.queryElanStateDumpWithoutNet(), } } @@ -167,7 +242,12 @@ export class FullDiagnosticsProvider implements Disposable { const fullDiagnostics = await performFullDiagnosis(this.outputChannel, projectUri) const formattedFullDiagnostics = formatFullDiagnostics(fullDiagnostics) const copyToClipboardInput = 'Copy to Clipboard' - const choice = await displayNotificationWithInput('Information', formattedFullDiagnostics, copyToClipboardInput) + const choice = await displayNotificationWithInput( + 'Information', + formattedFullDiagnostics, + [copyToClipboardInput], + 'Close', + ) if (choice === copyToClipboardInput) { await env.clipboard.writeText(formattedFullDiagnostics) } diff --git a/vscode-lean4/src/diagnostics/setupDiagnoser.ts b/vscode-lean4/src/diagnostics/setupDiagnoser.ts index a2dd9a012..74d39212c 100644 --- a/vscode-lean4/src/diagnostics/setupDiagnoser.ts +++ b/vscode-lean4/src/diagnostics/setupDiagnoser.ts @@ -1,8 +1,16 @@ import * as os from 'os' import { SemVer } from 'semver' import { OutputChannel, extensions, version } from 'vscode' -import { ExecutionExitCode, ExecutionResult, batchExecute, batchExecuteWithProgress } from '../utils/batch' +import { ExecutionExitCode, ExecutionResult, batchExecute } from '../utils/batch' +import { + ElanDumpStateWithNetResult, + ElanDumpStateWithoutNetResult, + elanDumpStateWithNet, + elanDumpStateWithoutNet, + isElanEagerResolutionVersion, +} from '../utils/elan' import { FileUri } from '../utils/exturi' +import { ToolchainUpdateMode, leanRunner } from '../utils/leanCmdRunner' import { checkParentFoldersForLeanProject, isValidLeanProject } from '../utils/projectInfo' export type SystemQueryResult = { @@ -16,8 +24,12 @@ export type VersionQueryResult = | { kind: 'Success'; version: SemVer } | { kind: 'CommandNotFound' } | { kind: 'CommandError'; message: string } + | { kind: 'Cancelled' } | { kind: 'InvalidVersion'; versionResult: string } +export type ElanDumpStateWithoutNetQueryResult = ElanDumpStateWithoutNetResult | { kind: 'PreEagerResolutionVersion' } +export type ElanDumpStateWithNetQueryResult = ElanDumpStateWithNetResult | { kind: 'PreEagerResolutionVersion' } + const recommendedElanVersion = new SemVer('3.1.1') // Should be bumped in a release *before* we bump the version requirement of the VS Code extension so that // users know that they need to update and do not get stuck on an old VS Code version. @@ -39,6 +51,7 @@ export type LeanVersionDiagnosis = | { kind: 'IsLean3Version'; version: SemVer } | { kind: 'IsAncientLean4Version'; version: SemVer } | { kind: 'NotInstalled' } + | { kind: 'Cancelled' } | { kind: 'ExecutionError'; message: string } export type VSCodeVersionDiagnosis = @@ -54,6 +67,10 @@ export function versionQueryResult(executionResult: ExecutionResult, versionRege return { kind: 'CommandError', message: executionResult.combined } } + if (executionResult.exitCode === ExecutionExitCode.Cancelled) { + return { kind: 'Cancelled' } + } + const match = versionRegex.exec(executionResult.stdout) if (!match) { return { kind: 'InvalidVersion', versionResult: executionResult.stdout } @@ -76,6 +93,9 @@ export function checkElanVersion(elanVersionResult: VersionQueryResult): ElanVer message: `Invalid Elan version format: '${elanVersionResult.versionResult}'`, } + case 'Cancelled': + throw new Error('Unexpected cancellation of `elan --version` query.') + case 'Success': if (elanVersionResult.version.compare(recommendedElanVersion) < 0) { return { @@ -107,6 +127,10 @@ export function checkLeanVersion(leanVersionResult: VersionQueryResult): LeanVer } } + if (leanVersionResult.kind === 'Cancelled') { + return { kind: 'Cancelled' } + } + const leanVersion = leanVersionResult.version if (leanVersion.major === 3) { return { kind: 'IsLean3Version', version: leanVersion } @@ -119,15 +143,27 @@ export function checkLeanVersion(leanVersionResult: VersionQueryResult): LeanVer return { kind: 'UpToDate', version: leanVersion } } +export type SetupDiagnoserOptions = { + channel: OutputChannel | undefined + cwdUri: FileUri | undefined + context?: string | undefined + toolchain?: string | undefined + toolchainUpdateMode?: ToolchainUpdateMode | undefined +} + export class SetupDiagnoser { readonly channel: OutputChannel | undefined readonly cwdUri: FileUri | undefined + readonly context: string | undefined readonly toolchain: string | undefined - - constructor(channel: OutputChannel | undefined, cwdUri: FileUri | undefined, toolchain?: string | undefined) { - this.channel = channel - this.cwdUri = cwdUri - this.toolchain = toolchain + readonly toolchainUpdateMode: ToolchainUpdateMode | undefined + + constructor(options: SetupDiagnoserOptions) { + this.channel = options.channel + this.cwdUri = options.cwdUri + this.context = options.context + this.toolchain = options.toolchain + this.toolchainUpdateMode = options.toolchainUpdateMode } async checkCurlAvailable(): Promise { @@ -140,13 +176,13 @@ export class SetupDiagnoser { return gitVersionResult.exitCode === ExecutionExitCode.Success } - async queryLakeVersion(context: string): Promise { - const lakeVersionResult = await this.runLeanCommand('lake', ['--version'], context, 'Checking Lake version') + async queryLakeVersion(): Promise { + const lakeVersionResult = await this.runLeanCommand('lake', ['--version'], 'Checking Lake version') return versionQueryResult(lakeVersionResult, /version (\d+\.\d+\.\d+(\w|-)*)/) } - async checkLakeAvailable(context: string): Promise { - const lakeVersionResult = await this.queryLakeVersion(context) + async checkLakeAvailable(): Promise { + const lakeVersionResult = await this.queryLakeVersion() return lakeVersionResult.kind === 'Success' } @@ -191,8 +227,8 @@ export class SetupDiagnoser { return { kind: 'UpToDate', version: currentVSCodeVersion } } - async queryLeanVersion(context: string): Promise { - const leanVersionResult = await this.runLeanCommand('lean', ['--version'], context, 'Checking Lean version') + async queryLeanVersion(): Promise { + const leanVersionResult = await this.runLeanCommand('lean', ['--version'], 'Checking Lean version') return versionQueryResult(leanVersionResult, /version (\d+\.\d+\.\d+(\w|-)*)/) } @@ -205,6 +241,28 @@ export class SetupDiagnoser { return await this.runSilently('elan', ['show']) } + async queryElanStateDumpWithoutNet(): Promise { + const dumpStateResult = await elanDumpStateWithoutNet(this.cwdUri, this.toolchain) + if (dumpStateResult.kind === 'ExecutionError') { + const versionResult = await this.queryElanVersion() + if (versionResult.kind === 'Success' && !isElanEagerResolutionVersion(versionResult.version)) { + return { kind: 'PreEagerResolutionVersion' } + } + } + return dumpStateResult + } + + async queryElanStateDumpWithNet(): Promise { + const dumpStateResult = await elanDumpStateWithNet(this.cwdUri, this.toolchain) + if (dumpStateResult.kind === 'ExecutionError') { + const versionResult = await this.queryElanVersion() + if (versionResult.kind === 'Success' && !isElanEagerResolutionVersion(versionResult.version)) { + return { kind: 'PreEagerResolutionVersion' } + } + } + return dumpStateResult + } + async elanVersion(): Promise { const elanVersionResult = await this.queryElanVersion() return checkElanVersion(elanVersionResult) @@ -223,8 +281,8 @@ export class SetupDiagnoser { return { kind: 'ValidProjectSetup', projectFolder: this.cwdUri } } - async leanVersion(context: string): Promise { - const leanVersionResult = await this.queryLeanVersion(context) + async leanVersion(): Promise { + const leanVersionResult = await this.queryLeanVersion() return checkLeanVersion(leanVersionResult) } @@ -232,31 +290,18 @@ export class SetupDiagnoser { return batchExecute(executablePath, args, this.cwdUri?.fsPath, { combined: this.channel }) } - private async runWithProgress( - executablePath: string, - args: string[], - context: string, - title: string, - ): Promise { - return batchExecuteWithProgress(executablePath, args, context, title, { - cwd: this.cwdUri?.fsPath, + private async runLeanCommand(executablePath: string, args: string[], title: string): Promise { + return await leanRunner.runLeanCommand(executablePath, args, { channel: this.channel, + context: this.context, + cwdUri: this.cwdUri, + waitingPrompt: title, + toolchain: this.toolchain, + toolchainUpdateMode: this.toolchainUpdateMode ?? 'UpdateAutomatically', }) } - - private async runLeanCommand(executablePath: string, args: string[], context: string, title: string) { - const leanArgs = [...args] - if (this.toolchain !== undefined) { - leanArgs.unshift(`+${this.toolchain}`) - } - return await this.runWithProgress(executablePath, leanArgs, context, title) - } } -export function diagnose( - channel: OutputChannel | undefined, - cwdUri: FileUri | undefined, - toolchain?: string | undefined, -): SetupDiagnoser { - return new SetupDiagnoser(channel, cwdUri, toolchain) +export function diagnose(options: SetupDiagnoserOptions): SetupDiagnoser { + return new SetupDiagnoser(options) } diff --git a/vscode-lean4/src/diagnostics/setupDiagnostics.ts b/vscode-lean4/src/diagnostics/setupDiagnostics.ts index c8fa0b903..be09f94c4 100644 --- a/vscode-lean4/src/diagnostics/setupDiagnostics.ts +++ b/vscode-lean4/src/diagnostics/setupDiagnostics.ts @@ -1,6 +1,7 @@ import { SemVer } from 'semver' import { OutputChannel, commands } from 'vscode' import { ExtUri, FileUri, extUriToCwdUri } from '../utils/exturi' +import { ToolchainUpdateMode } from '../utils/leanCmdRunner' import { LeanInstaller } from '../utils/leanInstaller' import { diagnose } from './setupDiagnoser' import { @@ -43,10 +44,10 @@ export class SetupDiagnostics { cwdUri: FileUri | undefined, ): Promise { const missingDeps = [] - if (!(await diagnose(channel, cwdUri).checkCurlAvailable())) { + if (!(await diagnose({ channel, cwdUri }).checkCurlAvailable())) { missingDeps.push('curl') } - if (!(await diagnose(channel, cwdUri).checkGitAvailable())) { + if (!(await diagnose({ channel, cwdUri }).checkGitAvailable())) { missingDeps.push('git') } if (missingDeps.length === 0) { @@ -67,8 +68,14 @@ export class SetupDiagnostics { installer: LeanInstaller, context: string, cwdUri: FileUri | undefined, + toolchainUpdateMode: ToolchainUpdateMode, ): Promise { - const leanVersionResult = await diagnose(installer.getOutputChannel(), cwdUri).queryLeanVersion(context) + const leanVersionResult = await diagnose({ + channel: installer.getOutputChannel(), + cwdUri, + context, + toolchainUpdateMode, + }).queryLeanVersion() switch (leanVersionResult.kind) { case 'Success': return 'Fulfilled' @@ -78,6 +85,9 @@ export class SetupDiagnostics { `Error while checking Lean version: ${leanVersionResult.message}`, ) + case 'Cancelled': + return this.n.displaySetupErrorWithOutput('Error while checking Lean version: Operation cancelled.') + case 'InvalidVersion': return this.n.displaySetupErrorWithOutput( `Error while checking Lean version: 'lean --version' returned a version that could not be parsed: '${leanVersionResult.versionResult}'`, @@ -93,7 +103,7 @@ export class SetupDiagnostics { cwdUri: FileUri | undefined, options: { elanMustBeInstalled: boolean }, ): Promise { - const elanDiagnosis = await diagnose(installer.getOutputChannel(), cwdUri).elanVersion() + const elanDiagnosis = await diagnose({ channel: installer.getOutputChannel(), cwdUri }).elanVersion() switch (elanDiagnosis.kind) { case 'NotInstalled': @@ -126,7 +136,7 @@ export class SetupDiagnostics { } async checkIsValidProjectFolder(channel: OutputChannel, folderUri: ExtUri): Promise { - const projectSetupDiagnosis = await diagnose(channel, extUriToCwdUri(folderUri)).projectSetup() + const projectSetupDiagnosis = await diagnose({ channel, cwdUri: extUriToCwdUri(folderUri) }).projectSetup() switch (projectSetupDiagnosis.kind) { case 'SingleFile': return await this.n.displaySetupWarning(singleFileWarningMessage) @@ -138,11 +148,13 @@ export class SetupDiagnostics { } else { return this.n.displaySetupWarningWithInput( missingLeanToolchainWithParentProjectWarningMessage(parentProjectFolder), - { - input: 'Open Parent Directory Project', - // this kills the extension host - action: () => commands.executeCommand('vscode.openFolder', parentProjectFolder), - }, + [ + { + input: 'Open Parent Directory Project', + // this kills the extension host + action: () => commands.executeCommand('vscode.openFolder', parentProjectFolder), + }, + ], ) } @@ -155,7 +167,7 @@ export class SetupDiagnostics { channel: OutputChannel, context: string, folderUri: ExtUri, - options: { toolchainOverride?: string | undefined }, + options: { toolchainOverride?: string | undefined; toolchainUpdateMode: ToolchainUpdateMode }, ): Promise { let origin: string if (options.toolchainOverride !== undefined) { @@ -165,11 +177,13 @@ export class SetupDiagnostics { } else { origin = 'Opened project' } - const projectLeanVersionDiagnosis = await diagnose( + const projectLeanVersionDiagnosis = await diagnose({ channel, - extUriToCwdUri(folderUri), - options.toolchainOverride, - ).leanVersion(context) + cwdUri: extUriToCwdUri(folderUri), + toolchain: options.toolchainOverride, + context, + toolchainUpdateMode: options.toolchainUpdateMode, + }).leanVersion() switch (projectLeanVersionDiagnosis.kind) { case 'NotInstalled': return this.n.displaySetupErrorWithOutput( @@ -181,6 +195,9 @@ export class SetupDiagnostics { `Error while checking Lean version: ${projectLeanVersionDiagnosis.message}`, ) + case 'Cancelled': + return this.n.displaySetupErrorWithOutput('Error while checking Lean version: Operation cancelled.') + case 'IsLean3Version': return this.n.displaySetupError(lean3ProjectErrorMessage(origin, projectLeanVersionDiagnosis.version)) @@ -198,13 +215,15 @@ export class SetupDiagnostics { channel: OutputChannel, context: string, folderUri: ExtUri, - options: { toolchainOverride?: string | undefined }, + options: { toolchainOverride?: string | undefined; toolchainUpdateMode: ToolchainUpdateMode }, ): Promise { - const lakeVersionResult = await diagnose( + const lakeVersionResult = await diagnose({ channel, - extUriToCwdUri(folderUri), - options.toolchainOverride, - ).queryLakeVersion(context) + cwdUri: extUriToCwdUri(folderUri), + toolchain: options.toolchainOverride, + context, + toolchainUpdateMode: options.toolchainUpdateMode, + }).queryLakeVersion() switch (lakeVersionResult.kind) { case 'CommandNotFound': return this.n.displaySetupErrorWithOutput( @@ -216,6 +235,9 @@ export class SetupDiagnostics { `Error while checking Lake version: ${lakeVersionResult.message}`, ) + case 'Cancelled': + return this.n.displaySetupErrorWithOutput('Error while checking Lake version: Operation cancelled.') + case 'InvalidVersion': return this.n.displaySetupErrorWithOutput( `Error while checking Lake version: Invalid Lake version format: '${lakeVersionResult.versionResult}'`, @@ -227,7 +249,7 @@ export class SetupDiagnostics { } async checkIsVSCodeUpToDate(): Promise { - const vscodeVersionResult = diagnose(undefined, undefined).queryVSCodeVersion() + const vscodeVersionResult = diagnose({ channel: undefined, cwdUri: undefined }).queryVSCodeVersion() switch (vscodeVersionResult.kind) { case 'Outdated': return await this.n.displaySetupWarning( diff --git a/vscode-lean4/src/diagnostics/setupNotifs.ts b/vscode-lean4/src/diagnostics/setupNotifs.ts index 117ec9c17..177a16091 100644 --- a/vscode-lean4/src/diagnostics/setupNotifs.ts +++ b/vscode-lean4/src/diagnostics/setupNotifs.ts @@ -1,8 +1,9 @@ import { SemVer } from 'semver' import { Disposable } from 'vscode' import { shouldShowSetupWarnings } from '../config' -import { LeanInstaller } from '../utils/leanInstaller' +import { LeanInstaller, UpdateElanMode } from '../utils/leanInstaller' import { + displayModalNotification, displayModalNotificationWithOutput, displayModalNotificationWithSetupGuide, displayNotification, @@ -57,7 +58,9 @@ export type SetupNotificationOptions = { warningMode: { modal: boolean; proceedByDefault: boolean } } -const proceedItem: string = 'Proceed Regardless' +const closeItem: string = 'Close' +const proceedItem: string = 'Proceed' +const proceedRegardlessItem: string = 'Proceed Regardless' const retryItem: StickyInput = { input: 'Retry', continueDisplaying: false, @@ -125,26 +128,26 @@ export class SetupNotifier { async displaySetupError(message: string): Promise { return await this.error({ modal: async () => { - await displayNotificationWithInput('Error', message) + await displayModalNotification('Error', message) return 'Fatal' }, nonModal: () => { displayNotification('Error', message) return 'Fatal' }, - sticky: async options => displayStickyNotificationWithOptionalInput('Error', message, options, retryItem), + sticky: async options => displayStickyNotificationWithOptionalInput('Error', message, options, [retryItem]), }) } async displaySetupWarning(message: string): Promise { return await this.warning({ modalProceedByDefault: async () => { - await displayNotificationWithInput('Warning', message) + await displayModalNotification('Warning', message) return 'Warning' }, modalAskBeforeProceeding: async () => { - const choice = await displayNotificationWithInput('Warning', message, proceedItem) - return choice === proceedItem ? 'Warning' : 'Fatal' + const choice = await displayNotificationWithInput('Warning', message, [proceedRegardlessItem]) + return choice === proceedRegardlessItem ? 'Warning' : 'Fatal' }, nonModal: () => { displayNotification('Warning', message) @@ -153,13 +156,14 @@ export class SetupNotifier { }) } - async displaySetupErrorWithInput( - message: string, - ...inputs: StickyInput[] - ): Promise { + async displaySetupErrorWithInput(message: string, inputs: StickyInput[]): Promise { return await this.error({ modal: async () => { - const choice = await displayNotificationWithInput('Error', message, ...inputs.map(i => i.input)) + const choice = await displayNotificationWithInput( + 'Error', + message, + inputs.map(i => i.input), + ) const chosenInput = inputs.find(i => i.input === choice) await chosenInput?.action() return 'Fatal' @@ -169,28 +173,31 @@ export class SetupNotifier { return 'Fatal' }, sticky: async options => - displayStickyNotificationWithOptionalInput('Error', message, options, retryItem, ...inputs), + displayStickyNotificationWithOptionalInput('Error', message, options, [retryItem, ...inputs]), }) } - async displaySetupWarningWithInput(message: string, ...inputs: Input[]): Promise { + async displaySetupWarningWithInput(message: string, inputs: Input[]): Promise { return await this.warning({ modalProceedByDefault: async () => { - const choice = await displayNotificationWithInput('Warning', message, ...inputs.map(i => i.input)) + const choice = await displayNotificationWithInput( + 'Warning', + message, + inputs.map(i => i.input), + proceedItem, + ) const chosenInput = inputs.find(i => i.input === choice) chosenInput?.action() return 'Warning' }, modalAskBeforeProceeding: async () => { - const choice = await displayNotificationWithInput( - 'Warning', - message, - proceedItem, + const choice = await displayNotificationWithInput('Warning', message, [ ...inputs.map(i => i.input), - ) + proceedRegardlessItem, + ]) const chosenInput = inputs.find(i => i.input === choice) chosenInput?.action() - return choice === proceedItem ? 'Warning' : 'Fatal' + return choice === proceedRegardlessItem ? 'Warning' : 'Fatal' }, nonModal: () => { displayNotificationWithOptionalInput('Warning', message, inputs) @@ -202,26 +209,26 @@ export class SetupNotifier { async displaySetupErrorWithOutput(message: string): Promise { return await this.error({ modal: async () => { - await displayModalNotificationWithOutput('Error', message) + await displayModalNotificationWithOutput('Error', message, [], closeItem) return 'Fatal' }, nonModal: () => { displayNotificationWithOutput('Error', message) return 'Fatal' }, - sticky: async options => displayStickyNotificationWithOutput('Error', message, options, retryItem), + sticky: async options => displayStickyNotificationWithOutput('Error', message, options, [retryItem]), }) } async displaySetupWarningWithOutput(message: string): Promise { return await this.warning({ modalProceedByDefault: async () => { - await displayModalNotificationWithOutput('Warning', message) + await displayModalNotificationWithOutput('Warning', message, [], proceedItem) return 'Warning' }, modalAskBeforeProceeding: async () => { - const choice = await displayModalNotificationWithOutput('Warning', message, proceedItem) - return choice === proceedItem ? 'Warning' : 'Fatal' + const choice = await displayModalNotificationWithOutput('Warning', message, [proceedRegardlessItem]) + return choice === proceedRegardlessItem ? 'Warning' : 'Fatal' }, nonModal: () => { displayNotificationWithOutput('Warning', message) @@ -233,26 +240,26 @@ export class SetupNotifier { async displaySetupErrorWithSetupGuide(message: string): Promise { return await this.error({ modal: async () => { - await displayModalNotificationWithSetupGuide('Error', message) + await displayModalNotificationWithSetupGuide('Error', message, [], closeItem) return 'Fatal' }, nonModal: () => { displayNotificationWithSetupGuide('Error', message) return 'Fatal' }, - sticky: async options => displayStickyNotificationWithSetupGuide('Error', message, options, retryItem), + sticky: async options => displayStickyNotificationWithSetupGuide('Error', message, options, [retryItem]), }) } async displaySetupWarningWithSetupGuide(message: string): Promise { return await this.warning({ modalProceedByDefault: async () => { - await displayModalNotificationWithSetupGuide('Warning', message) + await displayModalNotificationWithSetupGuide('Warning', message, [], proceedItem) return 'Warning' }, modalAskBeforeProceeding: async () => { - const choice = await displayModalNotificationWithSetupGuide('Warning', message, proceedItem) - return choice === proceedItem ? 'Warning' : 'Fatal' + const choice = await displayModalNotificationWithSetupGuide('Warning', message, [proceedRegardlessItem]) + return choice === proceedRegardlessItem ? 'Warning' : 'Fatal' }, nonModal: () => { displayNotificationWithSetupGuide('Warning', message) @@ -267,18 +274,19 @@ export class SetupNotifier { const isElanInstalled = await installer.displayInstallElanPrompt('Error', reason) return isElanInstalled ? 'Fulfilled' : 'Fatal' }, - sticky: async options => installer.displayStickyInstallElanPrompt('Error', reason, options, retryItem), + sticky: async options => installer.displayStickyInstallElanPrompt('Error', reason, options, [retryItem]), }) } async displayElanSetupWarning(installer: LeanInstaller, reason: string): Promise { return await this.warning({ modalProceedByDefault: async () => { - const success = await installer.displayInstallElanPrompt('Warning', reason) + const r = await installer.displayInstallElanPromptWithItems('Warning', reason, [], proceedItem) + const success = r !== undefined && r.kind === 'InstallElan' && r.success return success ? 'Fulfilled' : 'Warning' }, modalAskBeforeProceeding: async () => { - const r = await installer.displayInstallElanPromptWithItems('Warning', reason, proceedItem) + const r = await installer.displayInstallElanPromptWithItems('Warning', reason, [proceedRegardlessItem]) if (r === undefined) { return 'Fatal' } @@ -295,23 +303,16 @@ export class SetupNotifier { currentVersion: SemVer, recommendedVersion: SemVer, ): Promise { + const mode: UpdateElanMode = { + kind: 'Outdated', + versions: { currentVersion, recommendedVersion }, + } return await this.error({ modal: async () => { - const isElanUpToDate = await installer.displayUpdateElanPrompt( - 'Error', - currentVersion, - recommendedVersion, - ) + const isElanUpToDate = await installer.displayUpdateElanPrompt('Error', mode) return isElanUpToDate ? 'Fulfilled' : 'Fatal' }, - sticky: async options => - installer.displayStickyUpdateElanPrompt( - 'Error', - currentVersion, - recommendedVersion, - options, - retryItem, - ), + sticky: async options => installer.displayStickyUpdateElanPrompt('Error', mode, options, [retryItem]), }) } @@ -320,18 +321,18 @@ export class SetupNotifier { currentVersion: SemVer, recommendedVersion: SemVer, ): Promise { + const mode: UpdateElanMode = { + kind: 'Outdated', + versions: { currentVersion, recommendedVersion }, + } return await this.warning({ modalProceedByDefault: async () => { - const success = await installer.displayUpdateElanPrompt('Warning', currentVersion, recommendedVersion) + const r = await installer.displayUpdateElanPromptWithItems('Warning', mode, [], proceedItem) + const success = r !== undefined && r.kind === 'UpdateElan' && r.success return success ? 'Fulfilled' : 'Warning' }, modalAskBeforeProceeding: async () => { - const r = await installer.displayUpdateElanPromptWithItems( - 'Warning', - currentVersion, - recommendedVersion, - proceedItem, - ) + const r = await installer.displayUpdateElanPromptWithItems('Warning', mode, [proceedRegardlessItem]) if (r === undefined) { return 'Fatal' } diff --git a/vscode-lean4/src/exports.ts b/vscode-lean4/src/exports.ts index 0bf0dc4aa..e4a9b8451 100644 --- a/vscode-lean4/src/exports.ts +++ b/vscode-lean4/src/exports.ts @@ -4,6 +4,7 @@ import { InfoProvider } from './infoview' import { ProjectInitializationProvider } from './projectinit' import { ProjectOperationProvider } from './projectoperations' import { LeanClientProvider } from './utils/clientProvider' +import { ElanCommandProvider } from './utils/elanCommands' import { LeanInstaller } from './utils/leanInstaller' export interface AlwaysEnabledFeatures { @@ -11,6 +12,7 @@ export interface AlwaysEnabledFeatures { outputChannel: OutputChannel installer: LeanInstaller fullDiagnosticsProvider: FullDiagnosticsProvider + elanCommandProvider: ElanCommandProvider } export interface Lean4EnabledFeatures { diff --git a/vscode-lean4/src/extension.ts b/vscode-lean4/src/extension.ts index 2231d7856..6f1b0a3b6 100644 --- a/vscode-lean4/src/extension.ts +++ b/vscode-lean4/src/extension.ts @@ -18,16 +18,18 @@ import { ProjectOperationProvider } from './projectoperations' import { LeanTaskGutter } from './taskgutter' import { LeanClientProvider } from './utils/clientProvider' 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 { displayInternalErrorsIn } from './utils/internalErrors' +import { registerLeanCommandRunner } from './utils/leanCmdRunner' import { lean, LeanEditor, registerLeanEditorProvider } from './utils/leanEditorProvider' import { LeanInstaller } from './utils/leanInstaller' import { displayActiveStickyNotification, + displayModalNotification, displayNotification, - displayNotificationWithInput, setStickyNotificationActiveButHidden, } from './utils/notifs' import { PathExtensionProvider } from './utils/pathExtensionProvider' @@ -113,9 +115,12 @@ function activateAlwaysEnabledFeatures(context: ExtensionContext): AlwaysEnabled const defaultToolchain = getDefaultLeanVersion() const installer = new LeanInstaller(outputChannel, defaultToolchain) context.subscriptions.push( - commands.registerCommand('lean4.setup.installElan', () => - installer.displayInstallElanPrompt('Information', undefined), + commands.registerCommand( + 'lean4.setup.installElan', + async () => await installer.displayInstallElanPrompt('Information', undefined), ), + commands.registerCommand('lean4.setup.updateElan', async () => await installer.displayManualUpdateElanPrompt()), + commands.registerCommand('lean4.setup.uninstallElan', async () => await installer.uninstallElan()), ) const projectInitializationProvider = new ProjectInitializationProvider(outputChannel, installer) @@ -144,7 +149,10 @@ function activateAlwaysEnabledFeatures(context: ExtensionContext): AlwaysEnabled const abbreviationView = new AbbreviationView(extensionPath, abbreviationFeature.abbreviations) context.subscriptions.push(abbreviationView) - return { projectInitializationProvider, outputChannel, installer, fullDiagnosticsProvider } + const elanCommandProvider = new ElanCommandProvider(outputChannel) + context.subscriptions.push(elanCommandProvider) + + return { projectInitializationProvider, outputChannel, installer, fullDiagnosticsProvider, elanCommandProvider } } async function checkLean4FeaturePreconditions( @@ -155,7 +163,7 @@ async function checkLean4FeaturePreconditions( ): Promise { return await checkAll( () => d.checkAreDependenciesInstalled(installer.getOutputChannel(), cwdUri), - () => d.checkIsLean4Installed(installer, context, cwdUri), + () => d.checkIsLean4Installed(installer, context, cwdUri, 'PromptAboutUpdate'), () => d.checkIsElanUpToDate(installer, cwdUri, { elanMustBeInstalled: false, @@ -167,8 +175,10 @@ async function checkLean4FeaturePreconditions( async function activateLean4Features( context: ExtensionContext, installer: LeanInstaller, + elanCommandProvider: ElanCommandProvider, ): Promise { const clientProvider = new LeanClientProvider(installer, installer.getOutputChannel()) + elanCommandProvider.setClientProvider(clientProvider) context.subscriptions.push(clientProvider) const watchService = new LeanConfigWatchService() @@ -203,6 +213,7 @@ async function activateLean4Features( async function tryActivatingLean4FeaturesInProject( context: ExtensionContext, installer: LeanInstaller, + elanCommandProvider: ElanCommandProvider, resolve: (value: Lean4EnabledFeatures) => void, d: SetupDiagnostics, projectUri: FileUri | undefined, @@ -217,7 +228,7 @@ async function tryActivatingLean4FeaturesInProject( return } const lean4EnabledFeatures: Lean4EnabledFeatures = await displayInternalErrorsIn('activating Lean 4 features', () => - activateLean4Features(context, installer), + activateLean4Features(context, installer, elanCommandProvider), ) resolve(lean4EnabledFeatures) } @@ -225,17 +236,18 @@ async function tryActivatingLean4FeaturesInProject( async function tryActivatingLean4Features( context: ExtensionContext, installer: LeanInstaller, + elanCommandProvider: ElanCommandProvider, resolve: (value: Lean4EnabledFeatures) => void, d: SetupDiagnostics, warnAboutNoValidDocument: boolean, ) { const projectUri = await findOpenLeanProjectUri() if (projectUri !== 'NoValidDocument') { - await tryActivatingLean4FeaturesInProject(context, installer, resolve, d, projectUri) + await tryActivatingLean4FeaturesInProject(context, installer, elanCommandProvider, resolve, d, projectUri) return } if (warnAboutNoValidDocument) { - await displayNotificationWithInput( + await displayModalNotification( 'Error', 'No visible Lean document - cannot retry activating the extension. Please select a Lean document.', ) @@ -248,7 +260,14 @@ async function tryActivatingLean4Features( if (projectUri === 'InvalidProject') { return 'Continue' } - await tryActivatingLean4FeaturesInProject(context, installer, resolve, d, projectUri) + await tryActivatingLean4FeaturesInProject( + context, + installer, + elanCommandProvider, + resolve, + d, + projectUri, + ) return 'Stop' }), ), @@ -262,6 +281,7 @@ export async function activate(context: ExtensionContext): Promise { context.subscriptions.push( commands.registerCommand('lean4.redisplaySetupError', async () => displayActiveStickyNotification()), ) + registerLeanCommandRunner(context) const alwaysEnabledFeatures: AlwaysEnabledFeatures = await displayInternalErrorsIn( 'activating Lean 4 extension', @@ -275,12 +295,26 @@ export async function activate(context: ExtensionContext): Promise { errorMode: { mode: 'Sticky', retry: async () => - tryActivatingLean4Features(context, alwaysEnabledFeatures.installer, resolve, d, true), + tryActivatingLean4Features( + context, + alwaysEnabledFeatures.installer, + alwaysEnabledFeatures.elanCommandProvider, + resolve, + d, + true, + ), }, warningMode: { modal: true, proceedByDefault: true }, } d = new SetupDiagnostics(options) - await tryActivatingLean4Features(context, alwaysEnabledFeatures.installer, resolve, d, false) + await tryActivatingLean4Features( + context, + alwaysEnabledFeatures.installer, + alwaysEnabledFeatures.elanCommandProvider, + resolve, + d, + false, + ) }) return new Exports(alwaysEnabledFeatures, lean4EnabledFeatures) diff --git a/vscode-lean4/src/infoview.ts b/vscode-lean4/src/infoview.ts index 38e4dea1c..1b995dd85 100644 --- a/vscode-lean4/src/infoview.ts +++ b/vscode-lean4/src/infoview.ts @@ -142,7 +142,7 @@ export class InfoProvider implements Disposable { sendClientRequest: async (uri: string, method: string, params: any): Promise => { const extUri = parseExtUri(uri) if (extUri === undefined) { - return undefined + throw Error(`Unexpected URI scheme: ${Uri.parse(uri).scheme}`) } const client = this.clientProvider.findClient(extUri) @@ -162,7 +162,7 @@ export class InfoProvider implements Disposable { throw ex } } - return undefined + throw Error('No active Lean client.') }, sendClientNotification: async (uri: string, method: string, params: any): Promise => { const extUri = parseExtUri(uri) @@ -292,15 +292,17 @@ export class InfoProvider implements Disposable { createRpcSession: async uri => { const extUri = parseExtUri(uri) if (extUri === undefined) { - return '' + throw Error(`Unexpected URI scheme: ${Uri.parse(uri).scheme}`) } const client = this.clientProvider.findClient(extUri) - if (!client) return '' + if (client === undefined) { + throw Error('No active Lean client.') + } const sessionId = await rpcConnect(client, uri) const session = new RpcSessionAtPos(client, sessionId, uri) if (!this.webviewPanel) { session.dispose() - throw Error('infoview disconnect while connecting to RPC session') + throw Error('InfoView disconnected while connecting to RPC session.') } else { this.rpcSessions.set(sessionId, session) return sessionId diff --git a/vscode-lean4/src/leanclient.ts b/vscode-lean4/src/leanclient.ts index 48dbb2515..b7581a30b 100644 --- a/vscode-lean4/src/leanclient.ts +++ b/vscode-lean4/src/leanclient.ts @@ -40,7 +40,9 @@ import { logger } from './utils/logger' // @ts-ignore import { SemVer } from 'semver' import { c2pConverter, p2cConverter, patchConverters, setDependencyBuildMode } from './utils/converters' +import { elanInstalledToolchains } from './utils/elan' import { ExtUri, parseExtUri, toExtUri } from './utils/exturi' +import { leanRunner } from './utils/leanCmdRunner' import { lean, LeanDocument } from './utils/leanEditorProvider' import { displayNotification, @@ -62,7 +64,6 @@ export class LeanClient implements Disposable { private subscriptions: Disposable[] = [] private noPrompt: boolean = false private showingRestartMessage: boolean = false - private elanDefaultToolchain: string private isRestarting: boolean = false private staleDepNotifier: Disposable | undefined @@ -105,17 +106,10 @@ export class LeanClient implements Disposable { private serverFailedEmitter = new EventEmitter() serverFailed = this.serverFailedEmitter.event - constructor(folderUri: ExtUri, outputChannel: OutputChannel, elanDefaultToolchain: string) { - this.outputChannel = outputChannel // can be null when opening adhoc files. + constructor(folderUri: ExtUri, outputChannel: OutputChannel) { + this.outputChannel = outputChannel this.folderUri = folderUri - this.elanDefaultToolchain = elanDefaultToolchain - this.subscriptions.push( - new Disposable(() => { - if (this.staleDepNotifier) { - this.staleDepNotifier.dispose() - } - }), - ) + this.subscriptions.push(new Disposable(() => this.staleDepNotifier?.dispose())) } dispose(): void { @@ -169,6 +163,30 @@ export class LeanClient implements Disposable { } this.isRestarting = true try { + let defaultToolchain: string | undefined + if (this.folderUri.scheme === 'untitled') { + const installedToolchainsResult = await elanInstalledToolchains() + switch (installedToolchainsResult.kind) { + case 'Success': + if (installedToolchainsResult.defaultToolchain === undefined) { + this.serverFailedEmitter.fire( + 'No default Lean version set - cannot launch client for untitled file.', + ) + return + } + defaultToolchain = installedToolchainsResult.defaultToolchain + break + case 'ElanNotFound': + defaultToolchain = undefined + break + case 'ExecutionError': + this.serverFailedEmitter.fire( + `Cannot determine Lean version information for launching a client for an untitled file: ${installedToolchainsResult.message}`, + ) + return + } + } + logger.log('[LeanClient] Restarting Lean Server') if (this.isStarted()) { await this.stop() @@ -178,21 +196,64 @@ export class LeanClient implements Disposable { const progressOptions: ProgressOptions = { location: ProgressLocation.Notification, - title: 'Starting Lean language client', + title: '[Server Startup] Starting Lean language client', cancellable: false, } - await window.withProgress(progressOptions, async progress => await this.startClient(progress)) + await window.withProgress( + progressOptions, + async progress => await this.startClient(progress, defaultToolchain), + ) } finally { this.isRestarting = false } } - private async startClient(progress: Progress<{ message?: string; increment?: number }>) { + private async determineToolchainOverride( + defaultToolchain: string | undefined, + ): Promise<{ kind: 'Override'; toolchain: string } | { kind: 'NoOverride' } | { kind: 'Error'; message: string }> { + const cwdUri = this.folderUri.scheme === 'file' ? this.folderUri : undefined + const toolchainDecision = await leanRunner.decideToolchain({ + channel: this.outputChannel, + context: 'Server Startup', + cwdUri, + toolchainUpdateMode: 'PromptAboutUpdate', + }) + + if (toolchainDecision.kind === 'Error') { + return toolchainDecision + } + + if (toolchainDecision.kind === 'RunWithSpecificToolchain') { + return { kind: 'Override', toolchain: toolchainDecision.toolchain } + } + + toolchainDecision.kind satisfies 'RunWithActiveToolchain' + + if (this.folderUri.scheme === 'untitled' && defaultToolchain !== undefined) { + // Fixes issue #227, for adhoc files it would pick up the cwd from the open folder + // which is not what we want. For adhoc files we want the (default) toolchain instead. + return { kind: 'Override', toolchain: defaultToolchain } + } + return { kind: 'NoOverride' } + } + + private async startClient( + progress: Progress<{ message?: string; increment?: number }>, + defaultToolchain: string | undefined, + ): Promise { // Should only be called from `restart` const startTime = Date.now() progress.report({}) - this.client = await this.setupClient() + const toolchainOverrideResult = await this.determineToolchainOverride(defaultToolchain) + if (toolchainOverrideResult.kind === 'Error') { + this.serverFailedEmitter.fire(`Error while starting client: ${toolchainOverrideResult.message}`) + return + } + const toolchainOverride: string | undefined = + toolchainOverrideResult.kind === 'Override' ? toolchainOverrideResult.toolchain : undefined + + this.client = await this.setupClient(toolchainOverride) let insideRestart = true try { @@ -235,7 +296,6 @@ export class LeanClient implements Disposable { this.outputChannel.appendLine(msg) this.serverFailedEmitter.fire(msg) insideRestart = false - return } // HACK(WN): Register a default notification handler to fire on custom notifications. @@ -270,7 +330,12 @@ export class LeanClient implements Disposable { const finalizer = () => { stderrMsgBoxVisible = false } - displayNotificationWithOutput('Error', `Lean server printed an error:\n${chunk.toString()}`, finalizer) + displayNotificationWithOutput( + 'Error', + `Lean server printed an error:\n${chunk.toString()}`, + [], + finalizer, + ) } }) @@ -335,7 +400,6 @@ export class LeanClient implements Disposable { } await this.restart() - return 'Success' } @@ -438,22 +502,22 @@ export class LeanClient implements Disposable { return this.running ? this.client?.initializeResult : undefined } - private async determineServerOptions(): Promise { + private async determineServerOptions(toolchainOverride: string | undefined): Promise { const env = Object.assign({}, process.env) if (serverLoggingEnabled()) { env.LEAN_SERVER_LOG_DIR = serverLoggingPath() } const [serverExecutable, options] = await this.determineExecutable() + if (toolchainOverride) { + options.unshift('+' + toolchainOverride) + } const cwd = this.folderUri.scheme === 'file' ? this.folderUri.fsPath : undefined if (cwd) { // Add folder name to command-line so that it shows up in `ps aux`. options.push(cwd) } else { - // Fixes issue #227, for adhoc files it would pick up the cwd from the open folder - // which is not what we want. For adhoc files we want the (default) toolchain instead. - options.unshift('+' + this.elanDefaultToolchain) options.push('untitled') } @@ -604,8 +668,8 @@ export class LeanClient implements Disposable { } } - private async setupClient(): Promise { - const serverOptions: ServerOptions = await this.determineServerOptions() + private async setupClient(toolchainOverride: string | undefined): Promise { + const serverOptions: ServerOptions = await this.determineServerOptions(toolchainOverride) const clientOptions: LanguageClientOptions = this.obtainClientOptions() const client = new LanguageClient('lean4', 'Lean 4', serverOptions, clientOptions) diff --git a/vscode-lean4/src/projectinit.ts b/vscode-lean4/src/projectinit.ts index 9fbd84a0b..aa50263c8 100644 --- a/vscode-lean4/src/projectinit.ts +++ b/vscode-lean4/src/projectinit.ts @@ -8,6 +8,7 @@ import { ExecutionExitCode, ExecutionResult, } from './utils/batch' +import { elanStableChannel } from './utils/elan' import { ExtUri, extUriToCwdUri, FileUri } from './utils/exturi' import { lake } from './utils/lake' import { LeanInstaller } from './utils/leanInstaller' @@ -34,9 +35,14 @@ async function checkCreateLean4ProjectPreconditions( () => d.checkIsElanUpToDate(installer, cwdUri, { elanMustBeInstalled: true }), () => d.checkIsLeanVersionUpToDate(channel, context, folderUri, { + toolchainUpdateMode: 'UpdateAutomatically', toolchainOverride: projectToolchain, }), - () => d.checkIsLakeInstalledCorrectly(channel, context, folderUri, { toolchainOverride: projectToolchain }), + () => + d.checkIsLakeInstalledCorrectly(channel, context, folderUri, { + toolchainOverride: projectToolchain, + toolchainUpdateMode: 'UpdateAutomatically', + }), ) } @@ -51,8 +57,11 @@ async function checkPostCloneLean4ProjectPreconditions(installer: LeanInstaller, const d = new SetupDiagnostics(projectInitNotificationOptions) return await checkAll( () => d.checkIsElanUpToDate(installer, cwdUri, { elanMustBeInstalled: false }), - () => d.checkIsLeanVersionUpToDate(channel, context, folderUri, {}), - () => d.checkIsLakeInstalledCorrectly(channel, context, folderUri, {}), + () => d.checkIsLeanVersionUpToDate(channel, context, folderUri, { toolchainUpdateMode: 'UpdateAutomatically' }), + () => + d.checkIsLakeInstalledCorrectly(channel, context, folderUri, { + toolchainUpdateMode: 'UpdateAutomatically', + }), ) } @@ -73,7 +82,7 @@ export class ProjectInitializationProvider implements Disposable { private async createStandaloneProject() { const createStandaloneProjectContext = 'Create Standalone Project' - const toolchain = 'leanprover/lean4:stable' + const toolchain = elanStableChannel const projectFolder: FileUri | 'DidNotComplete' = await this.createProject( createStandaloneProjectContext, undefined, @@ -83,12 +92,13 @@ export class ProjectInitializationProvider implements Disposable { return } - const buildResult: ExecutionResult = await lake( - this.channel, - projectFolder, - createStandaloneProjectContext, + const buildResult: ExecutionResult = await lake({ + channel: this.channel, + cwdUri: projectFolder, + context: createStandaloneProjectContext, toolchain, - ).build() + toolchainUpdateMode: 'UpdateAutomatically', + }).build() if (buildResult.exitCode === ExecutionExitCode.Cancelled) { return } @@ -118,12 +128,13 @@ export class ProjectInitializationProvider implements Disposable { return } - const cacheGetResult: ExecutionResult = await lake( - this.channel, - projectFolder, - createMathlibProjectContext, - mathlibToolchain, - ).fetchMathlibCache() + const cacheGetResult: ExecutionResult = await lake({ + channel: this.channel, + cwdUri: projectFolder, + context: createMathlibProjectContext, + toolchain: mathlibToolchain, + toolchainUpdateMode: 'UpdateAutomatically', + }).fetchMathlibCache() if (cacheGetResult.exitCode === ExecutionExitCode.Cancelled) { return } @@ -132,12 +143,13 @@ export class ProjectInitializationProvider implements Disposable { return } - const buildResult: ExecutionResult = await lake( - this.channel, - projectFolder, - createMathlibProjectContext, - mathlibToolchain, - ).build() + const buildResult: ExecutionResult = await lake({ + channel: this.channel, + cwdUri: projectFolder, + context: createMathlibProjectContext, + toolchain: mathlibToolchain, + toolchainUpdateMode: 'UpdateAutomatically', + }).build() if (buildResult.exitCode === ExecutionExitCode.Cancelled) { return } @@ -158,7 +170,7 @@ export class ProjectInitializationProvider implements Disposable { private async createProject( context: string, kind?: string | undefined, - toolchain: string = 'leanprover/lean4:stable', + toolchain: string = elanStableChannel, ): Promise { const projectFolder: FileUri | undefined = await ProjectInitializationProvider.askForNewProjectFolderLocation({ saveLabel: 'Create project folder', @@ -181,21 +193,25 @@ export class ProjectInitializationProvider implements Disposable { } const projectName: string = path.basename(projectFolder.fsPath) - const result: ExecutionResult = await lake(this.channel, projectFolder, context, toolchain).initProject( - projectName, - kind, - ) + const result: ExecutionResult = await lake({ + channel: this.channel, + cwdUri: projectFolder, + context, + toolchain, + toolchainUpdateMode: 'UpdateAutomatically', + }).initProject(projectName, kind) if (result.exitCode !== ExecutionExitCode.Success) { displayResultError(result, 'Cannot initialize project.') return 'DidNotComplete' } - const updateResult: ExecutionResult = await lake( - this.channel, - projectFolder, + const updateResult: ExecutionResult = await lake({ + channel: this.channel, + cwdUri: projectFolder, context, toolchain, - ).updateDependencies() + toolchainUpdateMode: 'UpdateAutomatically', + }).updateDependencies() if (updateResult.exitCode === ExecutionExitCode.Cancelled) { return 'DidNotComplete' } @@ -278,7 +294,7 @@ Click the following link to learn how to set up Lean projects: [(Show Setup Guid However, a valid Lean 4 project folder was found in one of the parent directories at '${parentProjectFolder.fsPath}'. Open this project instead?` const input = 'Open parent directory project' - const choice: string | undefined = await displayNotificationWithInput('Information', message, input) + const choice: string | undefined = await displayNotificationWithInput('Information', message, [input]) if (choice !== input) { return undefined } @@ -381,11 +397,12 @@ Open this project instead?` } // Try it. If this is not a mathlib project, it will fail silently. Otherwise, it will grab the cache. - const fetchResult: ExecutionResult = await lake( - this.channel, - projectFolder, - downloadProjectContext, - ).fetchMathlibCache(true) + const fetchResult: ExecutionResult = await lake({ + channel: this.channel, + cwdUri: projectFolder, + context: downloadProjectContext, + toolchainUpdateMode: 'UpdateAutomatically', + }).fetchMathlibCache(true) if (fetchResult.exitCode === ExecutionExitCode.Cancelled) { return } @@ -416,7 +433,7 @@ Open this project instead?` private static async openNewFolder(projectFolder: FileUri) { const message = `Project initialized. Open new project folder '${path.basename(projectFolder.fsPath)}'?` const input = 'Open project folder' - const choice: string | undefined = await displayNotificationWithInput('Information', message, input) + const choice: string | undefined = await displayNotificationWithInput('Information', message, [input]) if (choice === input) { // This kills the extension host, so it has to be the last command await commands.executeCommand('vscode.openFolder', projectFolder.asUri()) diff --git a/vscode-lean4/src/projectoperations.ts b/vscode-lean4/src/projectoperations.ts index f990f8e85..bb441476e 100644 --- a/vscode-lean4/src/projectoperations.ts +++ b/vscode-lean4/src/projectoperations.ts @@ -57,7 +57,7 @@ export class ProjectOperationProvider implements Disposable { const deleteChoice: string | undefined = await displayNotificationWithInput( 'Information', 'Delete all build artifacts?', - deleteInput, + [deleteInput], ) if (deleteChoice !== deleteInput) { return @@ -82,12 +82,13 @@ export class ProjectOperationProvider implements Disposable { return } - const fetchMessage = "Project cleaned successfully. Do you want to fetch Mathlib's build artifact cache?" + const fetchMessage = "Project cleaned successfully. Do you wish to fetch Mathlib's build artifact cache?" const fetchInput = 'Fetch Cache' const fetchChoice: string | undefined = await displayNotificationWithInput( 'Information', fetchMessage, - fetchInput, + [fetchInput], + 'Do Not Fetch Cache', ) if (fetchChoice !== fetchInput) { return @@ -126,7 +127,7 @@ export class ProjectOperationProvider implements Disposable { private async fetchMathlibCacheForCurrentImports() { await this.runOperation('Fetch Mathlib Build Cache For Current Imports', async lakeRunner => { - const projectUri = lakeRunner.cwdUri! + const projectUri = lakeRunner.options.cwdUri! const doc = lean.lastActiveLeanDocument if (doc === undefined) { @@ -244,7 +245,7 @@ export class ProjectOperationProvider implements Disposable { const warningMessage = `This command will update ${dependencyChoice.name} to its most recent version. It is only intended to be used by maintainers of this project. If the updated version of ${dependencyChoice.name} is incompatible with any other dependency or the code in this project, this project may not successfully build anymore. Are you sure you want to proceed?` const warningInput = 'Proceed' - const warningChoice = await displayNotificationWithInput('Warning', warningMessage, warningInput) + const warningChoice = await displayNotificationWithInput('Warning', warningMessage, [warningInput]) if (warningChoice !== warningInput) { return } @@ -331,9 +332,9 @@ export class ProjectOperationProvider implements Disposable { toolchainResult === 'CannotReadLocalToolchain' ? `Could not read Lean version of open project at '${localToolchainPath}'` : `Could not read Lean version of ${dependencyName} at ${dependencyToolchainPath}` - const message = `${errorFlavor}. Do you want to update ${dependencyName} without updating the Lean version of the open project to that of ${dependencyName} regardless?` + const message = `${errorFlavor}. Do you wish to update ${dependencyName} without updating the Lean version of the open project to that of ${dependencyName} regardless?` const input = 'Proceed' - const choice: string | undefined = await displayNotificationWithInput('Information', message, input) + const choice: string | undefined = await displayNotificationWithInput('Information', message, [input]) return choice === 'input' ? { kind: 'DoNotUpdate' } : { kind: 'Cancelled' } } const [localToolchain, dependencyToolchain]: [string, string] = toolchainResult @@ -342,14 +343,14 @@ export class ProjectOperationProvider implements Disposable { return { kind: 'DoNotUpdate' } } - const message = `The Lean version '${localToolchain}' of the open project differs from the Lean version '${dependencyToolchain}' of ${dependencyName}. Do you want to update the Lean version of the open project to the Lean version of ${dependencyName}?` - const input1 = 'Update Lean Version' - const input2 = 'Keep Lean Version' - const choice = await displayNotificationWithInput('Information', message, input1, input2) + const message = `The Lean version '${localToolchain}' of the open project differs from the Lean version '${dependencyToolchain}' of ${dependencyName}. Do you wish to update the Lean version of the open project to the Lean version of ${dependencyName}?` + const updateInput = 'Update Lean Version' + const keepInput = 'Keep Lean Version' + const choice = await displayNotificationWithInput('Information', message, [keepInput, updateInput]) if (choice === undefined) { return { kind: 'Cancelled' } } - if (choice !== input1) { + if (choice !== updateInput) { return { kind: 'DoNotUpdate' } } @@ -415,7 +416,12 @@ export class ProjectOperationProvider implements Disposable { return } - const lakeRunner: LakeRunner = lake(this.channel, activeClient.folderUri, context) + const lakeRunner: LakeRunner = lake({ + channel: this.channel, + cwdUri: activeClient.folderUri, + context, + toolchainUpdateMode: 'DoNotUpdate', + }) const result: 'Success' | 'IsRestarting' = await activeClient.withStoppedClient(() => command(lakeRunner)) if (result === 'IsRestarting') { diff --git a/vscode-lean4/src/utils/batch.ts b/vscode-lean4/src/utils/batch.ts index 073b03427..23bc00b73 100644 --- a/vscode-lean4/src/utils/batch.ts +++ b/vscode-lean4/src/utils/batch.ts @@ -37,6 +37,7 @@ export function batchExecuteWithProc( args: string[], workingDirectory?: string | undefined, channel?: ExecutionChannel | undefined, + envExtensions?: { [key: string]: string } | undefined, ): [ChildProcessWithoutNullStreams | 'CannotLaunch', Promise] { let stdout: string = '' let stderr: string = '' @@ -45,6 +46,13 @@ export function batchExecuteWithProc( if (workingDirectory !== undefined) { options = { cwd: workingDirectory } } + if (envExtensions !== undefined) { + const env = Object.assign({}, process.env) + for (const [key, value] of Object.entries(envExtensions)) { + env[key] = value + } + options = { ...options, env } + } if (channel?.combined) { const formattedCwd = workingDirectory ? `${workingDirectory}` : '' const formattedArgs = args.map(arg => (arg.includes(' ') ? `"${arg}"` : arg)).join(' ') @@ -132,15 +140,17 @@ export async function batchExecute( args: string[], workingDirectory?: string | undefined, channel?: ExecutionChannel | undefined, + envExtensions?: { [key: string]: string } | undefined, ): Promise { - const [_, execPromise] = batchExecuteWithProc(executablePath, args, workingDirectory, channel) + const [_, execPromise] = batchExecuteWithProc(executablePath, args, workingDirectory, channel, envExtensions) return execPromise } -interface ProgressExecutionOptions { +export interface ProgressExecutionOptions { cwd?: string | undefined channel?: OutputChannel | undefined translator?: ((line: string) => string | undefined) | undefined + envExtensions?: { [key: string]: string } | undefined allowCancellation?: boolean } @@ -160,7 +170,6 @@ export async function batchExecuteWithProgress( cancellable: options.allowCancellation === true, } - let lastReportedMessage: string | undefined let progress: | Progress<{ message?: string | undefined @@ -180,11 +189,8 @@ export async function batchExecuteWithProgress( } if (options.channel) { options.channel.appendLine(value.trimEnd()) + progress?.report({ message: value }) } - if (progress !== undefined) { - progress.report({ message: value }) - } - lastReportedMessage = value }, appendLine(value: string) { this.append(value + '\n') @@ -209,9 +215,15 @@ export async function batchExecuteWithProgress( const expensiveExecutionTimeoutPromise: Promise = new Promise((resolve, _) => setTimeout(() => resolve(undefined), 250), ) - const [proc, executionPromise] = batchExecuteWithProc(executablePath, args, options.cwd, { - combined: progressChannel, - }) + const [proc, executionPromise] = batchExecuteWithProc( + executablePath, + args, + options.cwd, + { + combined: progressChannel, + }, + options.envExtensions, + ) if (proc === 'CannotLaunch') { return executionPromise // resolves to a 'CannotLaunch' ExecutionResult } @@ -225,7 +237,6 @@ export async function batchExecuteWithProgress( const result: ExecutionResult = await window.withProgress(progressOptions, (p, token) => { progress = p token.onCancellationRequested(() => proc.kill()) - progress.report({ message: lastReportedMessage }) return executionPromise }) return result diff --git a/vscode-lean4/src/utils/clientProvider.ts b/vscode-lean4/src/utils/clientProvider.ts index 7b8056939..f0ac3f1fd 100644 --- a/vscode-lean4/src/utils/clientProvider.ts +++ b/vscode-lean4/src/utils/clientProvider.ts @@ -23,12 +23,14 @@ async function checkLean4ProjectPreconditions( const d = new SetupDiagnostics(options) return await checkAll( () => d.checkIsValidProjectFolder(channel, folderUri), - () => d.checkIsLeanVersionUpToDate(channel, context, folderUri, {}), + () => d.checkIsLeanVersionUpToDate(channel, context, folderUri, { toolchainUpdateMode: 'PromptAboutUpdate' }), async () => { if (!(await willUseLakeServer(folderUri))) { return 'Fulfilled' } - return await d.checkIsLakeInstalledCorrectly(channel, context, folderUri, {}) + return await d.checkIsLakeInstalledCorrectly(channel, context, folderUri, { + toolchainUpdateMode: 'PromptAboutUpdate', + }) }, ) } @@ -104,6 +106,7 @@ export class LeanClientProvider implements Disposable { } getActiveClient(): LeanClient | undefined { + // TODO: Most callers of this function probably don't need an active client, just the folder URI. return this.activeClient } @@ -130,7 +133,7 @@ export class LeanClientProvider implements Disposable { const preconditionCheckResult = await checkLean4ProjectPreconditions( this.outputChannel, - 'Restart Client', + 'Client Restart', projectUri, ) if (preconditionCheckResult !== 'Fatal') { @@ -178,18 +181,31 @@ export class LeanClientProvider implements Disposable { this.restartFile(doc.extUri) } - private stopActiveClient() { + private async stopActiveClient() { if (this.activeClient && this.activeClient.isStarted()) { - void this.activeClient?.stop() + await this.activeClient?.stop() } } private async restartActiveClient() { - void this.activeClient?.restart() - } + if (this.activeClient === undefined) { + const activeUri = lean.lastActiveLeanDocument?.extUri + if (activeUri === undefined) { + displayNotification( + 'Error', + 'Cannot restart server: No focused Lean tab. Please focus the Lean tab for which you want to restart the server.', + ) + return + } - clientIsStarted() { - void this.activeClient?.isStarted() + const [cached, client] = await this.ensureClient(activeUri) + if (cached) { + await client?.restart() + } + return + } + + await this.activeClient?.restart() } // Find the client for a given document. @@ -224,9 +240,6 @@ export class LeanClientProvider implements Disposable { return this.clients.get(folder.toString()) } - // Starts a LeanClient if the given file is in a new workspace we haven't seen before. - // Returns a boolean "true" if the LeanClient was already created. - // Returns a null client if it turns out the new workspace is a lean3 workspace. async ensureClient(uri: ExtUri): Promise<[boolean, LeanClient | undefined]> { const folderUri = uri.scheme === 'file' ? await findLeanProjectRoot(uri) : new UntitledUri() if (folderUri === 'FileNotFound') { @@ -246,22 +259,24 @@ export class LeanClientProvider implements Disposable { const preconditionCheckResult = await checkLean4ProjectPreconditions( this.outputChannel, - 'Start Client', + 'Client Startup', folderUri, ) if (preconditionCheckResult === 'Fatal') { this.pending.delete(key) + this.activeClient = undefined return [false, undefined] } logger.log('[ClientProvider] Creating LeanClient for ' + folderUri.toString()) - const elanDefaultToolchain = await this.installer.getElanDefaultToolchain(folderUri) - - client = new LeanClient(folderUri, this.outputChannel, elanDefaultToolchain) + client = new LeanClient(folderUri, this.outputChannel) this.subscriptions.push(client) this.clients.set(key, client) client.serverFailed(err => { + if (this.activeClient === client) { + this.activeClient = undefined + } this.clients.delete(key) client.dispose() displayNotification('Error', err) @@ -276,12 +291,13 @@ export class LeanClientProvider implements Disposable { this.progressChangedEmitter.fire(arg) }) - this.pending.delete(key) + // Fired before starting the client because the InfoView uses this to register + // events on `client` that fire during `start`. this.clientAddedEmitter.fire(client) await client.start() - // tell the InfoView about this activated client. + this.pending.delete(key) this.activeClient = client return [false, client] diff --git a/vscode-lean4/src/utils/elan.ts b/vscode-lean4/src/utils/elan.ts index 4cedcb0dc..c26f5727f 100644 --- a/vscode-lean4/src/utils/elan.ts +++ b/vscode-lean4/src/utils/elan.ts @@ -1,6 +1,706 @@ +import { SemVer } from 'semver' import { OutputChannel } from 'vscode' -import { batchExecuteWithProgress, ExecutionResult } from './batch' +import { z, ZodTypeAny } from 'zod' +import { batchExecute, batchExecuteWithProgress, ExecutionExitCode, ExecutionResult } from './batch' +import { FileUri } from './exturi' +import { groupByUniqueKey } from './groupBy' -export async function elanSelfUpdate(channel: OutputChannel): Promise { - return await batchExecuteWithProgress('elan', ['self', 'update'], undefined, 'Updating Elan', { channel }) +export const elanStableChannel = 'leanprover/lean4:stable' +export const elanNightlyChannel = 'leanprover/lean4:nightly' + +export const elanEagerResolutionMajorVersion = 4 + +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-]+)*))?)/ + +export type ElanVersionResult = + | { kind: 'Success'; version: SemVer } + | { kind: 'ElanNotInstalled' } + | { kind: 'ExecutionError'; message: string } + +export async function elanVersion(): Promise { + const r = await batchExecute('elan', ['--version']) + switch (r.exitCode) { + case ExecutionExitCode.Success: + const match = elanVersionRegex.exec(r.stdout) + if (match === null) { + return { kind: 'ExecutionError', message: 'Cannot parse output of `elan --version`: ' + r.stdout } + } + return { kind: 'Success', version: new SemVer(match[1]) } + case ExecutionExitCode.CannotLaunch: + return { kind: 'ElanNotInstalled' } + case ExecutionExitCode.ExecutionError: + return { kind: 'ExecutionError', message: r.combined } + case ExecutionExitCode.Cancelled: + throw new Error('Unexpected cancellation of `elan --version`') + } +} + +export async function elanSelfUpdate( + channel: OutputChannel | undefined, + context: string | undefined, +): Promise { + return await batchExecuteWithProgress('elan', ['self', 'update'], context, 'Updating Elan', { channel }) +} + +export type ElanOption = T | undefined +export type ElanResult = { kind: 'Ok'; value: T } | { kind: 'Error'; message: string } + +export type ElanVersion = { + current: SemVer + newest: ElanResult +} + +export type ElanInstalledToolchain = { + resolvedName: string + path: FileUri +} + +export type ElanLocalUnresolvedToolchain = { kind: 'Local'; toolchain: string } +export type ElanRemoteUnresolvedToolchain = { + kind: 'Remote' + githubRepoOrigin: string + release: string + fromChannel: ElanOption +} + +export type ElanUnresolvedToolchain = ElanLocalUnresolvedToolchain | ElanRemoteUnresolvedToolchain + +export namespace ElanUnresolvedToolchain { + export function toolchainName(unresolved: ElanUnresolvedToolchain): string { + switch (unresolved.kind) { + case 'Local': + return unresolved.toolchain + case 'Remote': + return unresolved.githubRepoOrigin + ':' + unresolved.release + } + } +} + +export type ElanToolchainResolution = { + resolvedToolchain: ElanResult + cachedToolchain: ElanOption +} + +export type ElanDefaultToolchain = { + unresolved: ElanUnresolvedToolchain + resolved: ElanToolchainResolution +} + +export type ElanOverrideReason = + | { kind: 'Environment' } + | { kind: 'Manual'; directoryPath: FileUri } + | { kind: 'ToolchainFile'; toolchainPath: FileUri } + | { kind: 'LeanpkgFile'; leanpkgPath: FileUri } + | { kind: 'ToolchainDirectory'; directoryPath: FileUri } + +export type ElanOverride = { + unresolved: ElanUnresolvedToolchain + reason: ElanOverrideReason +} + +export type ElanToolchains = { + installed: Map + default: ElanOption + activeOverride: ElanOption + resolvedActive: ElanOption +} + +export namespace ElanToolchains { + export function unresolvedToolchain(toolchains: ElanToolchains): ElanOption { + return toolchains.activeOverride?.unresolved ?? toolchains.default?.unresolved + } + + export function unresolvedToolchainName(toolchains: ElanToolchains): ElanOption { + const unresolvedToolchain = ElanToolchains.unresolvedToolchain(toolchains) + if (unresolvedToolchain === undefined) { + return undefined + } + return ElanUnresolvedToolchain.toolchainName(unresolvedToolchain) + } +} + +export type ElanStateDump = { + elanVersion: ElanVersion + toolchains: ElanToolchains +} + +function zodElanResult(zodValue: T) { + return z.union([ + z.object({ + Ok: zodValue, + }), + z.object({ + Err: z.string(), + }), + ]) +} + +function zodElanUnresolvedToolchain() { + return z.union([ + z.object({ + Local: z.object({ + name: z.string(), + }), + }), + z.object({ + Remote: z.object({ + origin: z.string(), + release: z.string(), + from_channel: z.nullable(z.string()), + }), + }), + ]) +} + +function zodElanToolchainResolution() { + return z.object({ + live: zodElanResult(z.string()), + cached: z.nullable(z.string()), + }) +} + +function convertElanResult( + zodResult: + | { + Ok: T + } + | { + Err: string + }, + f: (v: T) => V, +): ElanResult { + if ('Ok' in zodResult) { + return { kind: 'Ok', value: f(zodResult.Ok) } + } + zodResult satisfies { + Err: string + } + return { kind: 'Error', message: zodResult.Err } +} + +function convertElanOption(zodNullable: T | null, f: (v: T) => V): ElanOption { + if (zodNullable === null) { + return undefined + } + return f(zodNullable) +} + +function convertElanUnresolvedToolchain( + zodElanUnresolvedToolchain: + | { + Local: { + name: string + } + } + | { + Remote: { + origin: string + release: string + from_channel: string | null + } + }, +): ElanUnresolvedToolchain { + if ('Local' in zodElanUnresolvedToolchain) { + return { kind: 'Local', toolchain: zodElanUnresolvedToolchain.Local.name } + } + zodElanUnresolvedToolchain satisfies { + Remote: { + origin: string + release: string + from_channel: string | null + } + } + return { + kind: 'Remote', + githubRepoOrigin: zodElanUnresolvedToolchain.Remote.origin, + release: zodElanUnresolvedToolchain.Remote.release, + fromChannel: convertElanOption(zodElanUnresolvedToolchain.Remote.from_channel, c => c), + } +} + +function covertElanToolchainResolution( + installed: Map, + zodElanToolchainResolution: { + live: + | { + Ok: string + } + | { + Err: string + } + cached: string | null + }, +): ElanToolchainResolution { + let cachedToolchain = convertElanOption(zodElanToolchainResolution.cached, t => t) + if (cachedToolchain !== undefined && !installed.has(cachedToolchain)) { + cachedToolchain = undefined + } + return { + resolvedToolchain: convertElanResult(zodElanToolchainResolution.live, t => t), + cachedToolchain, + } +} + +function convertElanOverrideReason( + zodElanOverrideReason: + | 'Environment' + | { + OverrideDB: string + } + | { + ToolchainFile: string + } + | { + LeanpkgFile: string + } + | { + InToolchainDirectory: string + }, +): ElanOverrideReason { + if (zodElanOverrideReason === 'Environment') { + return { kind: 'Environment' } + } + if ('OverrideDB' in zodElanOverrideReason) { + return { kind: 'Manual', directoryPath: new FileUri(zodElanOverrideReason.OverrideDB) } + } + if ('ToolchainFile' in zodElanOverrideReason) { + return { kind: 'ToolchainFile', toolchainPath: new FileUri(zodElanOverrideReason.ToolchainFile) } + } + if ('LeanpkgFile' in zodElanOverrideReason) { + return { kind: 'LeanpkgFile', leanpkgPath: new FileUri(zodElanOverrideReason.LeanpkgFile) } + } + zodElanOverrideReason satisfies { InToolchainDirectory: string } + return { kind: 'ToolchainDirectory', directoryPath: new FileUri(zodElanOverrideReason.InToolchainDirectory) } +} + +function parseElanStateDump(elanDumpStateOutput: string): ElanStateDump | undefined { + let parsedJson: any + try { + parsedJson = JSON.parse(elanDumpStateOutput) + } catch (e) { + return undefined + } + + const stateDumpSchema = z.object({ + elan_version: z.object({ + current: z.string().regex(semVerRegex), + newest: zodElanResult(z.string().regex(semVerRegex)), + }), + toolchains: z.object({ + installed: z.array( + z.object({ + resolved_name: z.string(), + path: z.string(), + }), + ), + default: z.nullable( + z.object({ + unresolved: zodElanUnresolvedToolchain(), + resolved: zodElanToolchainResolution(), + }), + ), + active_override: z.nullable( + z.object({ + unresolved: zodElanUnresolvedToolchain(), + reason: z.union([ + z.literal('Environment'), + z.object({ OverrideDB: z.string() }), + z.object({ ToolchainFile: z.string() }), + z.object({ LeanpkgFile: z.string() }), + z.object({ InToolchainDirectory: z.string() }), + ]), + }), + ), + resolved_active: z.nullable(zodElanToolchainResolution()), + }), + }) + const stateDumpResult = stateDumpSchema.safeParse(parsedJson) + if (!stateDumpResult.success) { + return undefined + } + const s = stateDumpResult.data + + const installed = groupByUniqueKey( + s.toolchains.installed.map(i => ({ resolvedName: i.resolved_name, path: new FileUri(i.path) })), + i => i.resolvedName, + ) + + const stateDump: ElanStateDump = { + elanVersion: { + current: new SemVer(s.elan_version.current), + newest: convertElanResult(s.elan_version.newest, version => new SemVer(version)), + }, + toolchains: { + installed, + default: convertElanOption(s.toolchains.default, d => ({ + unresolved: convertElanUnresolvedToolchain(d.unresolved), + resolved: covertElanToolchainResolution(installed, d.resolved), + })), + activeOverride: convertElanOption(s.toolchains.active_override, r => ({ + reason: convertElanOverrideReason(r.reason), + unresolved: convertElanUnresolvedToolchain(r.unresolved), + })), + resolvedActive: convertElanOption(s.toolchains.resolved_active, r => + covertElanToolchainResolution(installed, r), + ), + }, + } + return stateDump +} + +export type ElanDumpStateWithoutNetResult = + | { kind: 'Success'; state: ElanStateDump } + | { kind: 'ElanNotFound' } + | { kind: 'ExecutionError'; message: string } + +export type ElanDumpStateWithNetResult = ElanDumpStateWithoutNetResult | { kind: 'Cancelled' } + +function toolchainEnvExtensions(toolchain: string | undefined): { [key: string]: string } | undefined { + if (toolchain === undefined) { + return undefined + } + return { + ELAN_TOOLCHAIN: toolchain, + } +} + +export async function elanDumpStateWithoutNet( + cwdUri: FileUri | undefined, + toolchain?: string | undefined, +): Promise { + const r = await batchExecute( + 'elan', + ['dump-state', '--no-net'], + cwdUri?.fsPath, + undefined, + toolchainEnvExtensions(toolchain), + ) + switch (r.exitCode) { + case ExecutionExitCode.Success: + const state = parseElanStateDump(r.stdout) + if (state === undefined) { + return { kind: 'ExecutionError', message: 'Cannot parse output of `elan dump-state --no-net`.' } + } + return { kind: 'Success', state } + case ExecutionExitCode.CannotLaunch: + return { kind: 'ElanNotFound' } + case ExecutionExitCode.ExecutionError: + return { kind: 'ExecutionError', message: r.combined } + case ExecutionExitCode.Cancelled: + throw new Error('Unexpected cancellation of `elan dump-state --no-net`') + } +} + +export async function elanDumpStateWithNet( + cwdUri: FileUri | undefined, + context: string | undefined, + toolchain?: string | undefined, +): Promise { + const r = await batchExecuteWithProgress('elan', ['dump-state'], context, 'Fetching Lean version information', { + cwd: cwdUri?.fsPath, + allowCancellation: true, + envExtensions: toolchainEnvExtensions(toolchain), + }) + switch (r.exitCode) { + case ExecutionExitCode.Success: + const state = parseElanStateDump(r.stdout) + if (state === undefined) { + return { kind: 'ExecutionError', message: 'Cannot parse output of `elan dump-state`.' } + } + return { kind: 'Success', state } + case ExecutionExitCode.CannotLaunch: + return { kind: 'ElanNotFound' } + case ExecutionExitCode.ExecutionError: + return { kind: 'ExecutionError', message: r.combined } + case ExecutionExitCode.Cancelled: + return { kind: 'Cancelled' } + } +} + +export type ElanInstalledToolchainsResult = + | { kind: 'Success'; toolchains: string[]; defaultToolchain: string | undefined } + | { kind: 'ElanNotFound' } + | { kind: 'ExecutionError'; message: string } + +export async function elanInstalledToolchains(): Promise { + const stateDumpResult = await elanDumpStateWithoutNet(undefined) + + if (stateDumpResult.kind === 'ExecutionError') { + // User is probably on a pre-eager toolchain resolution elan version which did not yet support + // `elan dump-state`. Fall back to parsing the toolchain with `elan toolchain list`. + const r = await batchExecute('elan', ['toolchain', 'list']) + switch (r.exitCode) { + case ExecutionExitCode.Success: + const lines = r.stdout + .split(/\r?\n/) + .map(line => line.trim()) + .filter(line => line.length > 0) + const toolchainInfo: [string, boolean][] = lines.map(line => [ + line.replace(/\(default\)$/, '').trim(), + line.endsWith('(default)'), + ]) + const toolchains = toolchainInfo.map(([toolchain, _]) => toolchain) + const defaultToolchain = toolchainInfo.find(([_, isDefault]) => isDefault)?.[0] + return { kind: 'Success', toolchains, defaultToolchain } + case ExecutionExitCode.CannotLaunch: + return { kind: 'ElanNotFound' } + case ExecutionExitCode.ExecutionError: + return { kind: 'ExecutionError', message: r.combined } + case ExecutionExitCode.Cancelled: + throw new Error('Unexpected cancellation of `elan toolchain list`') + } + } + + if (stateDumpResult.kind === 'ElanNotFound') { + return stateDumpResult + } + + stateDumpResult.kind satisfies 'Success' + const installedToolchains = [...stateDumpResult.state.toolchains.installed.values()].map(t => t.resolvedName) + const defaultToolchain = stateDumpResult.state.toolchains.default + if (defaultToolchain === undefined) { + return { kind: 'Success', toolchains: installedToolchains, defaultToolchain: undefined } + } + return { + kind: 'Success', + toolchains: installedToolchains, + defaultToolchain: ElanUnresolvedToolchain.toolchainName(defaultToolchain.unresolved), + } +} + +export type ActiveToolchainInfo = { + unresolvedToolchain: string + cachedToolchain: string | undefined + resolvedToolchain: string + origin: ElanOverrideReason | { kind: 'Default' } +} + +export type ElanActiveToolchainResult = + | { kind: 'ElanNotFound' } + | { kind: 'ExecutionError'; message: string } + | { kind: 'Cancelled' } + | { kind: 'NoActiveToolchain' } + | { + kind: 'Success' + info: ActiveToolchainInfo + } + +export async function elanActiveToolchain( + cwdUri: FileUri | undefined, + context: string | undefined, + toolchain?: string | undefined, +): Promise { + const stateDumpResult = await elanDumpStateWithNet(cwdUri, context, toolchain) + if (stateDumpResult.kind !== 'Success') { + return stateDumpResult + } + + const unresolvedToolchain = ElanToolchains.unresolvedToolchainName(stateDumpResult.state.toolchains) + if (unresolvedToolchain === undefined) { + return { kind: 'NoActiveToolchain' } + } + + const toolchainResolution = stateDumpResult.state.toolchains.resolvedActive + if (toolchainResolution === undefined) { + return { kind: 'NoActiveToolchain' } + } + + const cachedToolchain = toolchainResolution.cachedToolchain + const resolvedToolchainResult = toolchainResolution.resolvedToolchain + + if (resolvedToolchainResult.kind === 'Error') { + return { kind: 'ExecutionError', message: resolvedToolchainResult.message } + } + const resolvedToolchain = resolvedToolchainResult.value + + const overrideReason = stateDumpResult.state.toolchains.activeOverride?.reason + const origin: ElanOverrideReason | { kind: 'Default' } = + overrideReason !== undefined ? overrideReason : { kind: 'Default' } + + return { kind: 'Success', info: { unresolvedToolchain, cachedToolchain, resolvedToolchain, origin } } +} + +export function toolchainVersion(toolchain: string): string { + const toolchainRegex = /(.+)\/(.+):(.+)/ + const match = toolchainRegex.exec(toolchain) + if (match === null) { + return toolchain + } + return match[3] +} + +export type ElanInstallToolchainResult = + | { kind: 'Success' } + | { kind: 'ElanNotFound' } + | { kind: 'ToolchainAlreadyInstalled' } + | { kind: 'Error'; message: string } + | { kind: 'Cancelled' } + +export async function elanInstallToolchain( + channel: OutputChannel | undefined, + context: string | undefined, + toolchain: string, +): Promise { + const r = await batchExecuteWithProgress( + 'elan', + ['toolchain', 'install', toolchain], + context, + `Installing ${toolchain}`, + { + channel, + allowCancellation: true, + }, + ) + switch (r.exitCode) { + case ExecutionExitCode.Success: + return { kind: 'Success' } + case ExecutionExitCode.CannotLaunch: + return { kind: 'ElanNotFound' } + case ExecutionExitCode.ExecutionError: + if (r.stderr.match(/error: '.*' is already installed/) !== null) { + return { kind: 'ToolchainAlreadyInstalled' } + } else { + return { kind: 'Error', message: r.combined } + } + case ExecutionExitCode.Cancelled: + return { kind: 'Cancelled' } + } +} + +export async function elanUninstallToolchains( + channel: OutputChannel | undefined, + context: string | undefined, + toolchains: string[], +): Promise { + if (toolchains.length === 0) { + throw new Error('Cannot uninstall zero toolchains.') + } + const waitingPrompt = + toolchains.length === 1 + ? `Uninstalling '${toolchains[0]}'` + : `Uninstalling Lean versions ${toolchains.map(t => `'${t}'`).join(', ')}` + return await batchExecuteWithProgress('elan', ['toolchain', 'uninstall', ...toolchains], context, waitingPrompt, { + channel, + allowCancellation: true, + }) +} + +export async function elanSelfUninstall( + channel: OutputChannel | undefined, + context: string | undefined, +): Promise { + return await batchExecuteWithProgress('elan', ['self', 'uninstall', '-y'], context, 'Uninstalling Elan', { + channel, + allowCancellation: true, + }) +} + +export type ElanSetDefaultToolchainResult = + | { kind: 'Success' } + | { kind: 'ElanNotFound' } + | { kind: 'Error'; message: string } + +export async function elanSetDefaultToolchain( + channel: OutputChannel | undefined, + toolchain: string, +): Promise { + const r = await batchExecute('elan', ['default', toolchain], undefined, { combined: channel }) + switch (r.exitCode) { + case ExecutionExitCode.Success: + return { kind: 'Success' } + case ExecutionExitCode.CannotLaunch: + return { kind: 'ElanNotFound' } + case ExecutionExitCode.ExecutionError: + return { kind: 'Error', message: r.combined } + case ExecutionExitCode.Cancelled: + throw new Error('Unexpected cancellation of `elan default `') + } +} + +export type ElanUsedToolchain = { + user: string + toolchain: string +} + +export type ElanGcInfo = { + unusedToolchains: string[] + usedToolchains: ElanUsedToolchain[] +} + +function parseElanGcJson(jsonOutput: string): ElanGcInfo | undefined { + let parsedJson: any + try { + parsedJson = JSON.parse(jsonOutput) + } catch (e) { + return undefined + } + + const elanGcJsonSchema = z.object({ + unused_toolchains: z.array(z.string()), + used_toolchains: z.array( + z.object({ + user: z.string(), + toolchain: z.string(), + }), + ), + }) + const elanGcJsonResult = elanGcJsonSchema.safeParse(parsedJson) + if (!elanGcJsonResult.success) { + return undefined + } + const elanGcJson = elanGcJsonResult.data + + return { + unusedToolchains: elanGcJson.unused_toolchains, + usedToolchains: elanGcJson.used_toolchains, + } +} + +export type ElanQueryGcResult = + | { kind: 'Success'; info: ElanGcInfo } + | { kind: 'ElanNotFound' } + | { kind: 'ExecutionError'; message: string } + +export async function elanQueryGc(): Promise { + const r = await batchExecute('elan', ['toolchain', 'gc', '--json']) + switch (r.exitCode) { + case ExecutionExitCode.Success: + const info = parseElanGcJson(r.stdout) + if (info === undefined) { + return { kind: 'ExecutionError', message: 'Cannot parse output of `elan toolchain gc --json`' } + } + return { kind: 'Success', info } + case ExecutionExitCode.CannotLaunch: + return { kind: 'ElanNotFound' } + case ExecutionExitCode.ExecutionError: + return { kind: 'ExecutionError', message: r.combined } + case ExecutionExitCode.Cancelled: + throw new Error('Unexpected cancellation of `elan toolchain gc --json`.') + } +} + +export async function elanGC( + channel: OutputChannel | undefined, + context: string | undefined, +): Promise { + return await batchExecuteWithProgress( + 'elan', + ['toolchain', 'gc', '--delete'], + context, + 'Removing unused Lean versions', + { + channel, + allowCancellation: true, + }, + ) } diff --git a/vscode-lean4/src/utils/elanCommands.ts b/vscode-lean4/src/utils/elanCommands.ts new file mode 100644 index 000000000..1936d5de0 --- /dev/null +++ b/vscode-lean4/src/utils/elanCommands.ts @@ -0,0 +1,526 @@ +import { promises } from 'fs' +import { commands, Disposable, OutputChannel, QuickPickItem, QuickPickItemKind, window } from 'vscode' +import { ExecutionExitCode } from './batch' +import { LeanClientProvider } from './clientProvider' +import { + ActiveToolchainInfo, + elanActiveToolchain, + elanEagerResolutionMajorVersion, + elanInstalledToolchains, + elanInstallToolchain, + elanNightlyChannel, + elanQueryGc, + elanSetDefaultToolchain, + elanStableChannel, + elanUninstallToolchains, + elanVersion, + isElanEagerResolutionVersion, + toolchainVersion, +} from './elan' +import { FileUri, UntitledUri } from './exturi' +import { fileExists } from './fsHelper' +import { groupByKey } from './groupBy' +import { displayNotification, displayNotificationWithInput } from './notifs' +import { LeanReleaseChannel, queryLeanReleases } from './releaseQuery' + +function displayElanNotInstalledError() { + displayNotification('Error', 'Elan is not installed.') +} + +export class ElanCommandProvider implements Disposable { + private subscriptions: Disposable[] = [] + + private clientProvider: LeanClientProvider | undefined + + constructor(private channel: OutputChannel) { + this.subscriptions.push( + commands.registerCommand('lean4.setup.selectDefaultToolchain', () => this.selectDefaultToolchain()), + commands.registerCommand('lean4.setup.updateReleaseChannel', () => this.updateReleaseChannel()), + commands.registerCommand('lean4.setup.uninstallToolchains', () => this.uninstallToolchains()), + commands.registerCommand('lean4.project.selectProjectToolchain', () => this.selectProjectToolchain()), + ) + } + + setClientProvider(clientProvider: LeanClientProvider) { + this.clientProvider = clientProvider + } + + async selectDefaultToolchain() { + if (!(await this.checkElanSupportsDumpState())) { + return + } + + const selectDefaultToolchainContext = 'Select Default Lean Version' + const selectedDefaultToolchain = await this.displayToolchainSelectionQuickPick( + selectDefaultToolchainContext, + 'Select default Lean version', + true, + ) + if (selectedDefaultToolchain === undefined) { + return + } + + let prompt: string + if (selectedDefaultToolchain === elanStableChannel) { + prompt = + `This operation will set the '${selectedDefaultToolchain}' Lean release channel to be the global default Lean release channel.\n` + + 'This means that the most recent stable Lean version at any given time will be used for files in VS Code that do not belong to a Lean project, as well as for Lean commands on the command line outside of Lean projects.\n' + + 'When a new stable Lean version becomes available, VS Code will issue a prompt about whether to update to the most recent Lean version. On the command line, the new stable Lean version will be downloaded automatically without a prompt.\n\n' + + 'Do you wish to proceed?' + } else { + prompt = + `This operation will set '${selectedDefaultToolchain}' to be the global default Lean version.\n` + + 'This means that it will be used for files in VS Code that do not belong to a Lean project, as well as for Lean commands on the command line outside of Lean projects.\n\n' + + 'Do you wish to proceed?' + } + const promptChoice = await displayNotificationWithInput('Information', prompt, ['Proceed']) + if (promptChoice !== 'Proceed') { + return + } + + const setDefaultToolchainResult = await elanSetDefaultToolchain(this.channel, selectedDefaultToolchain) + switch (setDefaultToolchainResult.kind) { + case 'Success': + displayNotification( + 'Information', + `Default Lean version '${selectedDefaultToolchain}' set successfully.`, + ) + const clientForUntitledFiles = this.clientProvider?.findClient(new UntitledUri()) + await clientForUntitledFiles?.restart() + break + case 'ElanNotFound': + displayNotification('Error', 'Cannot set Lean default version: Elan is not installed.') + break + case 'Error': + displayNotification('Error', `Cannot set Lean default version: ${setDefaultToolchainResult.message}`) + break + } + } + + async updateReleaseChannel() { + if (!(await this.checkElanSupportsDumpState())) { + return + } + + const context = 'Update Release Channel Lean Version' + const channels = [ + { + name: 'Stable', + identifier: elanStableChannel, + }, + { + name: 'Nightly', + identifier: elanNightlyChannel, + }, + ] + + const channelInfos: { name: string; info: ActiveToolchainInfo }[] = [] + for (const channel of channels) { + const activeToolchainInfo = await this.activeToolchain(context, channel.identifier) + if (activeToolchainInfo === undefined) { + return + } + if (activeToolchainInfo.cachedToolchain === activeToolchainInfo.resolvedToolchain) { + continue + } + channelInfos.push({ + name: channel.name, + info: activeToolchainInfo, + }) + } + + if (channelInfos.length === 0) { + displayNotification('Information', 'All Lean versions for all release channels are up-to-date.') + return + } + + const items: (QuickPickItem & { info: ActiveToolchainInfo })[] = channelInfos.map(channelInfo => { + const i = channelInfo.info + let detail: string + if (i.cachedToolchain === undefined) { + detail = `Current: Not installed ⟹ New: ${toolchainVersion(i.resolvedToolchain)}` + } else { + detail = `Current: ${toolchainVersion(i.cachedToolchain)} ⟹ New: ${toolchainVersion(i.resolvedToolchain)}` + } + return { + label: channelInfo.name, + description: i.unresolvedToolchain, + detail, + info: i, + } + }) + + const choice = await window.showQuickPick(items, { + title: 'Select the Lean release channel that should be updated to the most recent version', + matchOnDescription: true, + }) + if (choice === undefined) { + return + } + const channel = choice.info.unresolvedToolchain + + const installToolchainResult = await elanInstallToolchain( + this.channel, + 'Update Release Channel Lean Version', + channel, + ) + if (installToolchainResult.kind === 'ElanNotFound') { + displayNotification('Error', `Error while updating Lean version for '${channel}': Elan not found.`) + return + } + if (installToolchainResult.kind === 'Error') { + displayNotification( + 'Error', + `Error while updating Lean version for '${channel}': ${installToolchainResult.message}`, + ) + return + } + if (installToolchainResult.kind === 'Cancelled') { + displayNotification('Information', 'Lean version update cancelled.') + return + } + if (installToolchainResult.kind === 'ToolchainAlreadyInstalled') { + displayNotification('Information', `Lean version for release channel '${channel}' is already up-to-date.`) + return + } + installToolchainResult.kind satisfies 'Success' + displayNotification( + 'Information', + `Lean version for release channel '${channel}' has been updated to '${choice.info.resolvedToolchain}' successfully.`, + ) + } + + async uninstallToolchains() { + if (!(await this.checkElanSupportsDumpState())) { + return + } + + const queryGcResult = await elanQueryGc() + if (queryGcResult.kind === 'ElanNotFound') { + displayElanNotInstalledError() + return + } + if (queryGcResult.kind === 'ExecutionError') { + displayNotification('Error', `Error while querying unused toolchains: ${queryGcResult.message}`) + return + } + const unusedToolchains = queryGcResult.info.unusedToolchains + const unusedToolchainIndex = new Set(unusedToolchains) + const usedToolchainIndex = groupByKey(queryGcResult.info.usedToolchains, u => u.toolchain) + + const toolchainInfo = await this.installedToolchains() + if (toolchainInfo === undefined) { + return + } + const installedToolchains = toolchainInfo.toolchains + if (installedToolchains.length === 0) { + displayNotification('Information', 'No Lean versions installed.') + return + } + const installedToolchainItems = installedToolchains.map(t => { + const users = usedToolchainIndex + .get(t) + ?.map(t => { + if (t.user === 'default toolchain') { + // Translate Elan nomenclature to vscode-lean4 nomenclature + return 'default Lean version' + } + return `'${t.user}'` + }) + .join(', ') + return { + label: t, + description: users !== undefined ? `(used by ${users})` : '(unused)', + } + }) + + const allItems: QuickPickItem[] = [] + const uninstallUnusedLabel = 'Uninstall all unused Lean versions' + if (unusedToolchains.length > 0) { + allItems.push({ + label: uninstallUnusedLabel, + detail: unusedToolchains.map(t => toolchainVersion(t)).join(', '), + }) + allItems.push({ + label: '', + kind: QuickPickItemKind.Separator, + }) + } + allItems.push(...installedToolchainItems) + + const choices = await window.showQuickPick(allItems, { + canPickMany: true, + title: 'Choose Lean versions to uninstall', + }) + if (choices === undefined || choices.length === 0) { + return + } + + const toolchainsToUninstall: string[] = [] + if (choices.find(c => c.label === uninstallUnusedLabel) !== undefined) { + toolchainsToUninstall.push(...unusedToolchains) + toolchainsToUninstall.push( + ...choices + .filter(c => c.label !== uninstallUnusedLabel && !unusedToolchainIndex.has(c.label)) + .map(c => c.label), + ) + } else { + toolchainsToUninstall.push(...choices.map(c => c.label)) + } + + const formattedChoices = + toolchainsToUninstall.length === 1 + ? `'${toolchainsToUninstall[0]}'` + : toolchainsToUninstall.map(c => `'${c}'`).join(', ') + const confirmationPromptChoice = await displayNotificationWithInput( + 'Information', + `This command will uninstall ${formattedChoices}. Do you wish to proceed?`, + ['Proceed'], + ) + if (confirmationPromptChoice === undefined) { + return + } + confirmationPromptChoice satisfies 'Proceed' + + const r = await elanUninstallToolchains(this.channel, 'Uninstall Lean Versions', toolchainsToUninstall) + switch (r.exitCode) { + case ExecutionExitCode.Success: + const name = toolchainsToUninstall.length === 1 ? 'Lean version' : 'Lean versions' + displayNotification('Information', `${name} ${formattedChoices} uninstalled successfully.`) + return + case ExecutionExitCode.CannotLaunch: + displayElanNotInstalledError() + return + case ExecutionExitCode.ExecutionError: + displayNotification('Error', `Error while uninstalling Lean versions: ${r.combined}`) + return + case ExecutionExitCode.Cancelled: + return + } + } + + async selectProjectToolchain() { + if (!(await this.checkElanSupportsDumpState())) { + return + } + + const selectProjectToolchainContext = 'Select Project Lean Version' + + const activeClient = this.clientProvider?.getActiveClient() + if (activeClient === undefined) { + displayNotification( + 'Error', + 'No active client. Please focus a Lean file of the project for which you want to select a Lean version.', + ) + return + } + const activeClientUri = activeClient.getClientFolder() + const leanToolchainPath = (clientUri: FileUri) => clientUri.join('lean-toolchain').fsPath + + if (activeClientUri.scheme === 'untitled' || !(await fileExists(leanToolchainPath(activeClientUri)))) { + displayNotification( + 'Error', + 'Focused file is not contained in a Lean project. Please focus a Lean file of the project for which you want to select a Lean version.', + ) + return + } + + const selectedProjectToolchain = await this.displayToolchainSelectionQuickPick( + selectProjectToolchainContext, + 'Select project Lean version', + false, + ) + if (selectedProjectToolchain === undefined) { + return + } + + const prompt = + `This operation will set '${selectedProjectToolchain}' to be the Lean version of the Lean project at '${activeClientUri.fsPath}'. It is only intended to be used by maintainers of this project.\n\n` + + 'Changing the Lean version of this project may lead to breakages induced by incompatibilities with the new Lean version. For example, the following components of this project may end up being incompatible with the new Lean version:\n' + + '- The Lean code in this project\n' + + "- The 'lakefile.toml' or 'lakefile.lean' configuring this project\n" + + '- Lake dependencies of this project\n\n' + + "If you simply want to update a Lake dependency of this project and use its Lean version to ensure that the Lean version of the dependency is compatible with the Lean version of this project, it is preferable to use the 'Project: Update Dependency' command instead of this one.\n\n" + + 'Do you wish to proceed?' + const choice = await displayNotificationWithInput('Information', prompt, ['Proceed']) + if (choice !== 'Proceed') { + return + } + + try { + await promises.writeFile(leanToolchainPath(activeClientUri), selectedProjectToolchain, { + encoding: 'utf8', + flush: true, + }) + } catch (e) { + if (e instanceof Error) { + displayNotification('Error', `Update of '${leanToolchainPath(activeClientUri)}' failed: ${e.message}`) + } else { + displayNotification('Error', `Update of '${leanToolchainPath(activeClientUri)}' failed.`) + } + return + } + + await activeClient.restart() + + displayNotification('Information', 'Project Lean version update successful.') + } + + private async displayToolchainSelectionQuickPick( + context: string, + title: string, + includeStable: boolean, + ): Promise { + const toolchainInfo = await this.installedToolchains() + if (toolchainInfo === undefined) { + return undefined + } + const installedToolchains = toolchainInfo.toolchains + const installedToolchainIndex = new Set(installedToolchains) + + let stableToolchains: string[] = [] + let betaToolchains: string[] = [] + let nightlyToolchains: string[] = [] + const leanReleasesQueryResult = await queryLeanReleases(context) + if (leanReleasesQueryResult.kind === 'CannotParse') { + displayNotification( + 'Warning', + "Could not fetch Lean versions: Cannot parse response from 'https://release.lean-lang.org/'.", + ) + } + if (leanReleasesQueryResult.kind === 'CannotFetch') { + displayNotification('Warning', `Could not fetch Lean versions: ${leanReleasesQueryResult.error}`) + } + const toToolchainNames = (channel: LeanReleaseChannel) => + channel.map(t => `leanprover/lean4:${t.name}`).filter(t => !installedToolchainIndex.has(t)) + if (leanReleasesQueryResult.kind === 'Success') { + stableToolchains = toToolchainNames(leanReleasesQueryResult.releases.stable) + betaToolchains = toToolchainNames(leanReleasesQueryResult.releases.beta) + nightlyToolchains = toToolchainNames(leanReleasesQueryResult.releases.nightly) + } + const downloadableToolchains = [stableToolchains, betaToolchains, nightlyToolchains] + + const stableItem: QuickPickItem = { + label: 'Always use most recent stable version', + description: elanStableChannel, + picked: true, + } + const installedToolchainSeparator: QuickPickItem = { label: '', kind: QuickPickItemKind.Separator } + const installedToolchainItems: QuickPickItem[] = installedToolchains.map(t => ({ + label: t, + description: '(installed)', + })) + const downloadableToolchainItems: QuickPickItem[] = [] + for (const downloadableToolchainGroup of downloadableToolchains) { + if (downloadableToolchainGroup.length === 0) { + continue + } + const downloadableToolchainGroupSeparator: QuickPickItem = { label: '', kind: QuickPickItemKind.Separator } + downloadableToolchainItems.push(downloadableToolchainGroupSeparator) + for (const downloadableToolchain of downloadableToolchainGroup) { + downloadableToolchainItems.push({ + label: downloadableToolchain, + description: '(not installed)', + }) + } + } + + const allItems: QuickPickItem[] = [] + if (includeStable) { + allItems.push(stableItem) + allItems.push(installedToolchainSeparator) + } + allItems.push(...installedToolchainItems) + allItems.push(...downloadableToolchainItems) + + const choice = await window.showQuickPick(allItems, { + matchOnDescription: true, + title, + }) + if (choice === undefined) { + return undefined + } + if (choice.description === elanStableChannel) { + return elanStableChannel + } else { + return choice.label + } + } + + private async activeToolchain( + context: string, + toolchain?: string | undefined, + ): Promise { + const r = await elanActiveToolchain(undefined, context, toolchain) + if (r.kind === 'ExecutionError') { + displayNotification('Error', `Error while obtaining Lean versions: ${r.message}`) + return undefined + } + if (r.kind === 'ElanNotFound') { + displayElanNotInstalledError() + return undefined + } + if (r.kind === 'Cancelled') { + return undefined + } + if (r.kind === 'NoActiveToolchain') { + if (toolchain === undefined) { + displayNotification('Error', 'No active Lean version.') + } else { + displayNotification( + 'Error', + `Error while obtaining Lean versions: Expected active Lean version for toolchain override with '${toolchain}'`, + ) + } + return undefined + } + r.kind satisfies 'Success' + return r.info + } + + private async installedToolchains(): Promise< + { defaultToolchain: string | undefined; toolchains: string[] } | undefined + > { + const r = await elanInstalledToolchains() + if (r.kind === 'ExecutionError') { + displayNotification('Error', `Error while obtaining Lean versions: ${r.message}`) + return undefined + } + if (r.kind === 'ElanNotFound') { + displayElanNotInstalledError() + return undefined + } + r.kind satisfies 'Success' + return { + defaultToolchain: r.defaultToolchain, + toolchains: r.toolchains, + } + } + + private async checkElanSupportsDumpState(): Promise { + const r = await elanVersion() + switch (r.kind) { + case 'Success': + if (!isElanEagerResolutionVersion(r.version)) { + displayNotification( + 'Error', + `This command can only be used with Elan versions >= ${elanEagerResolutionMajorVersion}.0.0, but the installed Elan version is ${r.version.toString()}.`, + ) + return false + } + return true + case 'ElanNotInstalled': + displayElanNotInstalledError() + return false + case 'ExecutionError': + displayNotification('Error', `Error while checking Elan version: ${r.message}`) + return false + } + } + + dispose() { + for (const subscription of this.subscriptions) { + subscription.dispose() + } + } +} diff --git a/vscode-lean4/src/utils/groupBy.ts b/vscode-lean4/src/utils/groupBy.ts new file mode 100644 index 000000000..25f889ea4 --- /dev/null +++ b/vscode-lean4/src/utils/groupBy.ts @@ -0,0 +1,18 @@ +export function groupByKey(values: V[], key: (value: V) => K): Map { + const r = new Map() + for (const v of values) { + const k = key(v) + const group = r.get(k) ?? [] + group.push(v) + r.set(k, group) + } + return r +} + +export function groupByUniqueKey(values: V[], key: (value: V) => K): Map { + const r = new Map() + for (const v of values) { + r.set(key(v), v) + } + return r +} diff --git a/vscode-lean4/src/utils/internalErrors.ts b/vscode-lean4/src/utils/internalErrors.ts index fe92f055a..3cd111fd1 100644 --- a/vscode-lean4/src/utils/internalErrors.ts +++ b/vscode-lean4/src/utils/internalErrors.ts @@ -13,7 +13,8 @@ export async function displayInternalErrorsIn(scope: string, f: () => Promise 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 choice = await displayNotificationWithInput('Error', msg, copyToClipboardInput) + const closeInput = 'Close' + const choice = await displayNotificationWithInput('Error', msg, [copyToClipboardInput], closeInput) if (choice === copyToClipboardInput) { await env.clipboard.writeText(fullMsg) } diff --git a/vscode-lean4/src/utils/lake.ts b/vscode-lean4/src/utils/lake.ts index 3d103fe08..a139a711d 100644 --- a/vscode-lean4/src/utils/lake.ts +++ b/vscode-lean4/src/utils/lake.ts @@ -1,28 +1,22 @@ import path from 'path' import { OutputChannel } from 'vscode' -import { batchExecute, batchExecuteWithProgress, ExecutionExitCode, ExecutionResult } from './batch' +import { ExecutionExitCode, ExecutionResult } from './batch' import { FileUri } from './exturi' +import { leanRunner, ToolchainUpdateMode } from './leanCmdRunner' export const cacheNotFoundError = 'unknown executable `cache`' export const cacheNotFoundExitError = '=> Operation failed. Exit Code: 1.' -export class LakeRunner { +export type LakeRunnerOptions = { channel: OutputChannel cwdUri: FileUri | undefined context: string | undefined - toolchain: string | undefined + toolchain?: string | undefined + toolchainUpdateMode: ToolchainUpdateMode +} - constructor( - channel: OutputChannel, - cwdUri: FileUri | undefined, - context: string | undefined, - toolchain?: string | undefined, - ) { - this.channel = channel - this.cwdUri = cwdUri - this.context = context - this.toolchain = toolchain - } +export class LakeRunner { + constructor(readonly options: LakeRunnerOptions) {} async initProject(name: string, kind?: string | undefined): Promise { const args = kind ? [name, kind] : [name] @@ -75,40 +69,24 @@ export class LakeRunner { return 'No' } - private async runLakeCommandSilently(subCommand: string, args: string[]): Promise { - args = args.slice() - args.unshift(subCommand) - if (this.toolchain) { - args.unshift(`+${this.toolchain}`) - } - return await batchExecute('lake', args, this.cwdUri?.fsPath) - } - private async runLakeCommandWithProgress( subCommand: string, args: string[], waitingPrompt: string, translator?: ((line: string) => string | undefined) | undefined, ): Promise { - args = args.slice() - args.unshift(subCommand) - if (this.toolchain) { - args.unshift(`+${this.toolchain}`) - } - return await batchExecuteWithProgress('lake', args, this.context, waitingPrompt, { - cwd: this.cwdUri?.fsPath, - channel: this.channel, + return await leanRunner.runLeanCommand('lake', [subCommand, ...args], { + channel: this.options.channel, + context: this.options.context, + cwdUri: this.options.cwdUri, + waitingPrompt, + toolchain: this.options.toolchain, + toolchainUpdateMode: this.options.toolchainUpdateMode, translator, - allowCancellation: true, }) } } -export function lake( - channel: OutputChannel, - cwdUri: FileUri | undefined, - context: string | undefined, - toolchain?: string | undefined, -): LakeRunner { - return new LakeRunner(channel, cwdUri, context, toolchain) +export function lake(options: LakeRunnerOptions): LakeRunner { + return new LakeRunner(options) } diff --git a/vscode-lean4/src/utils/leanCmdRunner.ts b/vscode-lean4/src/utils/leanCmdRunner.ts new file mode 100644 index 000000000..a567a486a --- /dev/null +++ b/vscode-lean4/src/utils/leanCmdRunner.ts @@ -0,0 +1,412 @@ +import path from 'path' +import { ExtensionContext, OutputChannel } from 'vscode' +import { alwaysAskBeforeInstallingLeanVersions } from '../config' +import { batchExecuteWithProgress, ExecutionExitCode, ExecutionResult } from './batch' +import { + elanDumpStateWithNet, + ElanDumpStateWithNetResult, + elanDumpStateWithoutNet, + ElanDumpStateWithoutNetResult, + elanInstallToolchain, + ElanOverrideReason, + ElanRemoteUnresolvedToolchain, + ElanStateDump, + ElanToolchains, + ElanUnresolvedToolchain, +} from './elan' +import { FileUri } from './exturi' +import { displayNotification, displayNotificationWithInput } from './notifs' + +export type ToolchainUpdateMode = 'UpdateAutomatically' | 'PromptAboutUpdate' | 'DoNotUpdate' + +function shouldUpdateToolchainAutomatically(mode: ToolchainUpdateMode) { + return !alwaysAskBeforeInstallingLeanVersions() && mode === 'UpdateAutomatically' +} + +export type ToolchainDecisionOptions = { + channel: OutputChannel | undefined + cwdUri: FileUri | undefined + context: string | undefined + toolchainUpdateMode: ToolchainUpdateMode + toolchain?: string | undefined +} + +export type LeanCommandOptions = ToolchainDecisionOptions & { + waitingPrompt: string + translator?: ((line: string) => string | undefined) | undefined +} + +function overrideReason(activeOverride: ElanOverrideReason | undefined): string | undefined { + switch (activeOverride?.kind) { + case undefined: + return undefined + case 'Environment': + return undefined + case 'Manual': + return `set by \`elan override\` in folder '${path.basename(activeOverride.directoryPath.fsPath)}'` + case 'ToolchainFile': + return `of Lean project '${path.dirname(activeOverride.toolchainPath.fsPath)}'` + case 'LeanpkgFile': + return `of Lean project '${path.dirname(activeOverride.leanpkgPath.fsPath)}'` + case 'ToolchainDirectory': + return `of Lean project '${activeOverride.directoryPath.fsPath}'` + } +} + +function leanNotInstalledError( + activeOverride: ElanOverrideReason | undefined, + unresolvedActiveToolchain: ElanRemoteUnresolvedToolchain, +): string { + const or = overrideReason(activeOverride) + const formattedOverride = or !== undefined ? ' ' + or : '' + if (unresolvedActiveToolchain.fromChannel !== undefined) { + const prefix = activeOverride === undefined ? 'default ' : '' + return `No Lean version for ${prefix}release channel '${ElanUnresolvedToolchain.toolchainName(unresolvedActiveToolchain)}'${formattedOverride} is installed.` + } else { + const prefix = activeOverride === undefined ? 'Default ' : '' + return `${prefix}Lean version '${ElanUnresolvedToolchain.toolchainName(unresolvedActiveToolchain)}'${formattedOverride} is not installed.` + } +} + +function installationPrompt( + activeOverride: ElanOverrideReason | undefined, + unresolvedActiveToolchain: ElanRemoteUnresolvedToolchain, +): string { + const error = leanNotInstalledError(activeOverride, unresolvedActiveToolchain) + if (unresolvedActiveToolchain.fromChannel !== undefined) { + return `${error}\n\n` + 'Do you wish to install one?' + } else { + return `${error}\n\n` + 'Do you wish to install it?' + } +} + +function updatePrompt( + activeOverride: ElanOverrideReason | undefined, + releaseChannel: string, + cachedActiveToolchain: string, + resolvedActiveToolchain: string, +): string { + const prefix = activeOverride === undefined ? 'default ' : '' + const reason = overrideReason(activeOverride) + return ( + `Installed Lean version '${cachedActiveToolchain}' for ${prefix}release channel '${releaseChannel}'${reason !== undefined ? ' ' + reason : ''} is outdated.\n\n` + + `Do you wish to install the new Lean version '${resolvedActiveToolchain}' or continue using the outdated Lean version?` + ) +} + +function updateDecisionKey(cwdUri: FileUri | undefined, cachedToolchain: string): string { + return JSON.stringify({ + cwdUri, + cachedToolchain, + }) +} + +export class LeanCommandRunner { + private stickyUpdateDecisions: Map = new Map() + + private async runCmd( + executablePath: string, + args: string[], + options: LeanCommandOptions, + toolchain: string | undefined, + ): Promise { + const toolchainOverride = toolchain ?? options.toolchain + if (toolchainOverride !== undefined) { + args = [`+${toolchainOverride}`, ...args] + } + return await batchExecuteWithProgress(executablePath, args, options.context, options.waitingPrompt, { + cwd: options.cwdUri?.fsPath, + channel: options.channel, + translator: options.translator, + allowCancellation: true, + }) + } + + private async analyzeElanStateDumpWithoutNetResult( + channel: OutputChannel | undefined, + context: string | undefined, + r: ElanDumpStateWithoutNetResult, + ): Promise< + | { kind: 'CheckForToolchainUpdate'; cachedToolchain: string } + | { kind: 'RunWithActiveToolchain' } + | { kind: 'Error'; message: string } + > { + const runWithActiveToolchain: { kind: 'RunWithActiveToolchain' } = { kind: 'RunWithActiveToolchain' } + + let elanState: ElanStateDump + switch (r.kind) { + case 'Success': + elanState = r.state + break + case 'ElanNotFound': + return runWithActiveToolchain + case 'ExecutionError': + return runWithActiveToolchain + } + + const unresolvedToolchain = ElanToolchains.unresolvedToolchain(elanState.toolchains) + const toolchainResolutionResult = elanState.toolchains.resolvedActive + if (unresolvedToolchain === undefined || toolchainResolutionResult === undefined) { + return runWithActiveToolchain + } + + if (unresolvedToolchain.kind === 'Local') { + return runWithActiveToolchain + } + + const cachedToolchain = toolchainResolutionResult.cachedToolchain + if (cachedToolchain === undefined) { + const installNewToolchain: () => Promise< + { kind: 'RunWithActiveToolchain' } | { kind: 'Error'; message: string } + > = async () => { + const elanInstallToolchainResult = await elanInstallToolchain( + channel, + context, + ElanUnresolvedToolchain.toolchainName(unresolvedToolchain), + ) + switch (elanInstallToolchainResult.kind) { + case 'Success': + case 'ElanNotFound': + case 'ToolchainAlreadyInstalled': + return runWithActiveToolchain + case 'Error': + return { + kind: 'Error', + message: + leanNotInstalledError( + elanState.toolchains.activeOverride?.reason, + unresolvedToolchain, + ) + ` Reason: Installation failed. Error: ${elanInstallToolchainResult.message}`, + } + case 'Cancelled': + return { + kind: 'Error', + message: + leanNotInstalledError( + elanState.toolchains.activeOverride?.reason, + unresolvedToolchain, + ) + ' Reason: Installation was cancelled.', + } + } + } + if (!alwaysAskBeforeInstallingLeanVersions()) { + return await installNewToolchain() + } + const choice = await displayNotificationWithInput( + 'Information', + installationPrompt(elanState.toolchains.activeOverride?.reason, unresolvedToolchain), + ['Install Version'], + ) + if (choice === undefined) { + return { + kind: 'Error', + message: leanNotInstalledError(elanState.toolchains.activeOverride?.reason, unresolvedToolchain), + } + } + choice satisfies 'Install Version' + + return await installNewToolchain() + } + + if (unresolvedToolchain.fromChannel === undefined) { + return runWithActiveToolchain + } + + return { kind: 'CheckForToolchainUpdate', cachedToolchain } + } + + private async analyzeElanDumpStateWithNetResult( + channel: OutputChannel | undefined, + context: string | undefined, + toolchainUpdateMode: 'UpdateAutomatically' | 'PromptAboutUpdate', + cachedToolchain: string, + r: ElanDumpStateWithNetResult, + ): Promise< + | { kind: 'RunWithActiveToolchain' } + | { kind: 'RunWithCachedToolchain'; warning: string | undefined } + | { kind: 'Error'; message: string } + > { + const runWithActiveToolchain: { kind: 'RunWithActiveToolchain' } = { kind: 'RunWithActiveToolchain' } + const runWithCachedToolchain: (warning: string | undefined) => { + kind: 'RunWithCachedToolchain' + warning: string | undefined + } = warning => ({ + kind: 'RunWithCachedToolchain', + warning, + }) + + let elanState: ElanStateDump + switch (r.kind) { + case 'Success': + elanState = r.state + break + case 'ElanNotFound': + return runWithActiveToolchain + case 'ExecutionError': + return runWithActiveToolchain + case 'Cancelled': + return runWithCachedToolchain( + `Lean version information query was cancelled, falling back to installed Lean version '${cachedToolchain}'.`, + ) + } + + const unresolvedToolchain = ElanToolchains.unresolvedToolchain(elanState.toolchains) + const toolchainResolutionResult = elanState.toolchains.resolvedActive + if (unresolvedToolchain === undefined || toolchainResolutionResult === undefined) { + return runWithActiveToolchain + } + + if (unresolvedToolchain.kind === 'Local' || unresolvedToolchain.fromChannel === undefined) { + return runWithActiveToolchain + } + + const resolvedToolchainResult = toolchainResolutionResult.resolvedToolchain + let resolvedToolchain: string + switch (resolvedToolchainResult.kind) { + case 'Error': + return runWithCachedToolchain( + `Could not fetch Lean version information, falling back to installed Lean version '${cachedToolchain}'. Error: ${resolvedToolchainResult.message}`, + ) + case 'Ok': + resolvedToolchain = resolvedToolchainResult.value + break + } + + const willActiveToolchainBeUpdated = cachedToolchain !== resolvedToolchain + if (!willActiveToolchainBeUpdated) { + return runWithActiveToolchain + } + + const isResolvedToolchainAlreadyInstalled = elanState.toolchains.installed.has(resolvedToolchain) + if (isResolvedToolchainAlreadyInstalled) { + return runWithActiveToolchain + } + + const updateToolchain = async () => { + const elanInstallToolchainResult = await elanInstallToolchain( + channel, + context, + ElanUnresolvedToolchain.toolchainName(unresolvedToolchain), + ) + switch (elanInstallToolchainResult.kind) { + case 'Success': + case 'ElanNotFound': + case 'ToolchainAlreadyInstalled': + return runWithActiveToolchain + case 'Error': + return runWithCachedToolchain( + `Could not update Lean version, falling back to installed Lean version '${cachedToolchain}'. Error: ${elanInstallToolchainResult.message}`, + ) + case 'Cancelled': + return runWithCachedToolchain( + `Lean version update was cancelled, falling back to installed Lean version '${cachedToolchain}'.`, + ) + } + } + + if (shouldUpdateToolchainAutomatically(toolchainUpdateMode)) { + return await updateToolchain() + } + + const choice = await displayNotificationWithInput( + 'Information', + updatePrompt( + elanState.toolchains.activeOverride?.reason, + ElanUnresolvedToolchain.toolchainName(unresolvedToolchain), + cachedToolchain, + resolvedToolchain, + ), + ['Update Lean Version'], + 'Use Old Version', + ) + if (choice === undefined || choice === 'Use Old Version') { + return runWithCachedToolchain(undefined) + } + choice satisfies 'Update Lean Version' + return await updateToolchain() + } + + async decideToolchain( + options: ToolchainDecisionOptions, + ): Promise< + | { kind: 'RunWithActiveToolchain' } + | { kind: 'RunWithSpecificToolchain'; toolchain: string } + | { kind: 'Error'; message: string } + > { + const elanStateDumpWithoutNetResult = await elanDumpStateWithoutNet(options.cwdUri, options.toolchain) + const withoutNetAnalysisResult = await this.analyzeElanStateDumpWithoutNetResult( + options.channel, + options.context, + elanStateDumpWithoutNetResult, + ) + if (withoutNetAnalysisResult.kind !== 'CheckForToolchainUpdate') { + return withoutNetAnalysisResult + } + + const cachedToolchain = withoutNetAnalysisResult.cachedToolchain + const key = updateDecisionKey(options.cwdUri, cachedToolchain) + if ( + options.toolchainUpdateMode === 'DoNotUpdate' || + (!shouldUpdateToolchainAutomatically(options.toolchainUpdateMode) && + this.stickyUpdateDecisions.get(key) === 'DoNotUpdate') + ) { + return { kind: 'RunWithSpecificToolchain', toolchain: cachedToolchain } + } + + const elanStateDumpWithNetResult = await elanDumpStateWithNet( + options.cwdUri, + options.context, + options.toolchain, + ) + const withNetAnalysisResult = await this.analyzeElanDumpStateWithNetResult( + options.channel, + options.context, + options.toolchainUpdateMode, + cachedToolchain, + elanStateDumpWithNetResult, + ) + if (withNetAnalysisResult.kind === 'RunWithCachedToolchain') { + this.stickyUpdateDecisions.set(key, 'DoNotUpdate') + if (withNetAnalysisResult.warning !== undefined) { + displayNotification('Warning', withNetAnalysisResult.warning) + } + return { kind: 'RunWithSpecificToolchain', toolchain: cachedToolchain } + } + return withNetAnalysisResult + } + + async runLeanCommand( + executablePath: string, + args: string[], + options: LeanCommandOptions, + ): Promise { + const toolchainDecision = await this.decideToolchain(options) + if (toolchainDecision.kind === 'Error') { + return { + exitCode: ExecutionExitCode.ExecutionError, + stdout: toolchainDecision.message, + stderr: '', + combined: toolchainDecision.message, + } + } + if (toolchainDecision.kind === 'RunWithActiveToolchain') { + return await this.runCmd(executablePath, args, options, undefined) + } + toolchainDecision.kind satisfies 'RunWithSpecificToolchain' + return await this.runCmd(executablePath, args, options, toolchainDecision.toolchain) + } +} + +export let leanRunner: LeanCommandRunner + +/** Must be called at the very start when the extension is activated so that `leanRunner` is defined. */ +export function registerLeanCommandRunner(context: ExtensionContext) { + leanRunner = new LeanCommandRunner() + context.subscriptions.push({ + dispose: () => { + const u: any = undefined + // Implicit invariant: When the extension deactivates, `leanRunner` is not called after this assignment. + leanRunner = u + }, + }) +} diff --git a/vscode-lean4/src/utils/leanEditorProvider.ts b/vscode-lean4/src/utils/leanEditorProvider.ts index c46add8c4..a5470d561 100644 --- a/vscode-lean4/src/utils/leanEditorProvider.ts +++ b/vscode-lean4/src/utils/leanEditorProvider.ts @@ -11,25 +11,7 @@ import { workspace, } from 'vscode' import { ExtUri, isExtUri, toExtUriOrError } from './exturi' - -function groupByKey(values: V[], key: (value: V) => K): Map { - const r = new Map() - for (const v of values) { - const k = key(v) - const group = r.get(k) ?? [] - group.push(v) - r.set(k, group) - } - return r -} - -function groupByUniqueKey(values: V[], key: (value: V) => K): Map { - const r = new Map() - for (const v of values) { - r.set(key(v), v) - } - return r -} +import { groupByKey, groupByUniqueKey } from './groupBy' export class LeanDocument { constructor( @@ -426,4 +408,11 @@ export let lean: LeanEditorProvider export function registerLeanEditorProvider(context: ExtensionContext) { lean = new LeanEditorProvider() context.subscriptions.push(lean) + context.subscriptions.push({ + dispose: () => { + const u: any = undefined + // Implicit invariant: When the extension deactivates, `lean` is not called after this assignment. + lean = u + }, + }) } diff --git a/vscode-lean4/src/utils/leanInstaller.ts b/vscode-lean4/src/utils/leanInstaller.ts index 4d3fa0360..fc67978f5 100644 --- a/vscode-lean4/src/utils/leanInstaller.ts +++ b/vscode-lean4/src/utils/leanInstaller.ts @@ -1,9 +1,9 @@ import { SemVer } from 'semver' import { Disposable, EventEmitter, OutputChannel, TerminalOptions, window } from 'vscode' -import { getPowerShellPath, isRunningTest } from '../config' -import { ExecutionExitCode, batchExecute, displayResultError } from './batch' -import { elanSelfUpdate } from './elan' -import { ExtUri, FileUri } from './exturi' +import { getPowerShellPath, isRunningTest, setAlwaysAskBeforeInstallingLeanVersions } from '../config' +import { ExecutionExitCode, displayResultError } from './batch' +import { elanSelfUninstall, elanSelfUpdate, elanVersion, isElanEagerResolutionVersion } from './elan' +import { FileUri } from './exturi' import { logger } from './logger' import { NotificationSeverity, @@ -20,16 +20,23 @@ export class LeanVersion { error: string | undefined } +export type UpdateElanMode = + | { + kind: 'Outdated' + versions: { currentVersion: SemVer; recommendedVersion: SemVer } + } + | { + kind: 'Manual' + versions: { currentVersion: SemVer } + } + export class LeanInstaller { private leanInstallerLinux = 'https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh' private leanInstallerWindows = 'https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1' private outputChannel: OutputChannel private prompting: boolean = false - private installing: boolean = false + private pendingOperation: 'Install' | 'Update' | 'Uninstall' | undefined private freshInstallDefaultToolchain: string - private elanDefaultToolchain: string = '' // the default toolchain according to elan (toolchain marked with '(default)') - private workspaceSuffix: string = '(workspace override)' - private defaultSuffix: string = '(default)' private promptUser: boolean = true // This event is raised whenever a version change happens. @@ -90,72 +97,15 @@ export class LeanInstaller { void this.showRestartPromptAndRestart('Lake file configuration changed', packageUri) } - private removeSuffix(version: string): string { - let s = version - const suffixes = [this.defaultSuffix, this.workspaceSuffix] - suffixes.forEach(suffix => { - if (s.endsWith(suffix)) { - s = s.substr(0, s.length - suffix.length) - } - }) - return s.trim() - } - - async getElanDefaultToolchain(packageUri: ExtUri): Promise { - if (this.elanDefaultToolchain) { - return this.elanDefaultToolchain - } - - const toolChains = await this.elanListToolChains(packageUri) - let result: string = '' - toolChains.forEach(s => { - if (s.endsWith(this.defaultSuffix)) { - result = this.removeSuffix(s) - } - }) - - this.elanDefaultToolchain = result - return result - } - - async elanListToolChains(packageUri: ExtUri): Promise { - try { - const cmd = 'elan' - const options = ['toolchain', 'list'] - const cwd = packageUri.scheme === 'file' ? packageUri.fsPath : undefined - const stdout = (await batchExecute(cmd, options, cwd)).stdout - if (!stdout) { - throw new Error('elan toolchain list returned no output.') - } - const result: string[] = [] - stdout.split(/\r?\n/).forEach(s => { - s = s.trim() - if (s !== '') { - result.push(s) - } - }) - return result - } catch (err) { - return [`${err}`] - } - } - - async hasElan(): Promise { - try { - const options = ['--version'] - const result = await batchExecute('elan', options) - const filterVersion = /elan (\d+)\.\d+\..+/ - const match = filterVersion.exec(result.stdout) - return match !== null - } catch (err) { - return false - } - } - private installElanPrompt(reason: string | undefined): { message: string; item: 'Install Elan and Lean 4' } { - const reasonPrefix = reason ? reason + ' ' : '' - const message = - reasonPrefix + "Do you want to install Lean's version manager Elan and a recent stable version of Lean 4?" + let message: string + if (reason !== undefined) { + message = `${reason} Do you wish to install Lean's version manager Elan and a recent stable version of Lean 4?` + } else { + message = + "This command will install Lean's version manager Elan and a recent stable version of Lean 4.\n\n" + + 'Do you wish to proceed?' + } const item = 'Install Elan and Lean 4' return { message, item } } @@ -163,7 +113,8 @@ export class LeanInstaller { async displayInstallElanPromptWithItems( severity: NotificationSeverity, reason: string | undefined, - ...otherItems: string[] + otherItems: string[] = [], + defaultItem?: string | undefined, ): Promise<{ kind: 'InstallElan'; success: boolean } | { kind: 'OtherItem'; choice: string } | undefined> { if (!this.getPromptUser()) { // Used in tests @@ -172,12 +123,12 @@ export class LeanInstaller { } const p = this.installElanPrompt(reason) - const choice = await displayNotificationWithInput(severity, p.message, p.item, ...otherItems) + const choice = await displayNotificationWithInput(severity, p.message, [p.item, ...otherItems], defaultItem) if (choice === undefined) { return undefined } if (choice === p.item) { - return { kind: 'InstallElan', success: (await this.installElan()) === 'Success' } + return { kind: 'InstallElan', success: (await this.installElanAndDisplaySettingPrompt()) === 'Success' } } return { kind: 'OtherItem', choice } } @@ -195,71 +146,116 @@ export class LeanInstaller { reason: string | undefined, // eslint-disable-next-line @typescript-eslint/no-redundant-type-constituents options: StickyNotificationOptions<'Install Elan and Lean 4' | string>, - ...otherItems: StickyInput[] + otherItems: StickyInput[] = [], ): Disposable { const p = this.installElanPrompt(reason) const installElanItem: StickyInput<'Install Elan and Lean 4'> = { input: p.item, continueDisplaying: false, action: async () => { - await this.installElan() + await this.installElanAndDisplaySettingPrompt() }, } - return displayStickyNotificationWithOptionalInput(severity, p.message, options, installElanItem, ...otherItems) + return displayStickyNotificationWithOptionalInput(severity, p.message, options, [ + installElanItem, + ...otherItems, + ]) } - private updateElanPrompt( - currentVersion: SemVer, - recommendedVersion: SemVer, - ): { message: string; item: 'Update Elan' } { - return { - message: `Lean's version manager Elan is outdated: the installed version is ${currentVersion.toString()}, but a version of ${recommendedVersion.toString()} is recommended. Do you want to update Elan?`, - item: 'Update Elan', + private updateElanPrompt(mode: UpdateElanMode): { message: string; item: 'Update Elan' } { + switch (mode.kind) { + case 'Manual': + return { + message: + "This command will update Lean's version manager Elan to its most recent version.\n\n" + + 'Do you wish to proceed?', + item: 'Update Elan', + } + case 'Outdated': + return { + message: + `Lean's version manager Elan is outdated: the installed version is ${mode.versions.currentVersion.toString()}, but a version of ${mode.versions.recommendedVersion.toString()} is recommended.\n\n` + + 'Do you wish to update Elan?', + item: 'Update Elan', + } } } - private async updateElan(currentVersion: SemVer): Promise { - if (currentVersion.compare('3.1.0') === 0) { - // `elan self update` was broken in elan 3.1.0, so we need to take a different approach to updating elan here. - const installElanResult = await this.installElan() - return installElanResult === 'Success' + private async displayElanUpdateSuccessfulPrompt(currentVersion: SemVer) { + if (isElanEagerResolutionVersion(currentVersion)) { + displayNotification('Information', 'Elan update successful!') + return } - const elanSelfUpdateResult = await elanSelfUpdate(this.outputChannel) - if (elanSelfUpdateResult.exitCode !== ExecutionExitCode.Success) { - displayResultError( - elanSelfUpdateResult, - "Cannot update Elan. If you suspect that this is due to the way that you have set up Elan (e.g. from a package repository that ships an outdated version of Elan), you can disable these warnings using the 'Lean4: Show Setup Warnings' setting under 'File' > 'Preferences' > 'Settings'.", - ) - return false + const prompt = + 'Elan update successful!\n\n' + + 'Do you want Elan in VS Code to continue downloading and installing Lean versions automatically, or would you prefer it to ask for confirmation before downloading and installing new Lean versions?\n' + + 'Asking for confirmation is especially desirable if you are ever using a limited internet data plan or your internet connection tends to be slow, whereas automatic installs are less tedious on fast and unlimited internet connections.' + + const choice = await displayNotificationWithInput( + 'Information', + prompt, + ['Always Ask For Confirmation'], + 'Install Lean Versions Automatically', + ) + if (choice === 'Always Ask For Confirmation') { + await setAlwaysAskBeforeInstallingLeanVersions(true) + } + if (choice === 'Install Lean Versions Automatically') { + await setAlwaysAskBeforeInstallingLeanVersions(false) } + } + + private async updateElan(currentVersion: SemVer): Promise { + const r = await this.performOperation('Update', async () => { + if (currentVersion.compare('3.1.0') === 0) { + // `elan self update` was broken in elan 3.1.0, so we need to take a different approach to updating elan here. + const installElanResult = await this.installElanAndDisplaySettingPrompt() + if (installElanResult !== 'Success') { + return false + } + await this.displayElanUpdateSuccessfulPrompt(currentVersion) + return true + } + + const elanSelfUpdateResult = await elanSelfUpdate(this.outputChannel, 'Update Elan') + if (elanSelfUpdateResult.exitCode !== ExecutionExitCode.Success) { + displayResultError( + elanSelfUpdateResult, + "Cannot update Elan. If you suspect that this is due to the way that you have set up Elan (e.g. from a package repository that ships an outdated version of Elan), you can disable these warnings using the 'Lean4: Show Setup Warnings' setting under 'File' > 'Preferences' > 'Settings'.", + ) + return false + } + + await this.displayElanUpdateSuccessfulPrompt(currentVersion) - return true + return true + }) + if (r === 'PendingOperation') { + return false + } + return r } async displayUpdateElanPromptWithItems( severity: NotificationSeverity, - currentVersion: SemVer, - recommendedVersion: SemVer, - ...otherItems: string[] + mode: UpdateElanMode, + otherItems: string[] = [], + defaultItem?: string | undefined, ): Promise<{ kind: 'UpdateElan'; success: boolean } | { kind: 'OtherItem'; choice: string } | undefined> { - const p = this.updateElanPrompt(currentVersion, recommendedVersion) - const choice = await displayNotificationWithInput(severity, p.message, p.item, ...otherItems) + const p = this.updateElanPrompt(mode) + const choice = await displayNotificationWithInput(severity, p.message, [p.item, ...otherItems], defaultItem) if (choice === undefined) { return undefined } if (choice === p.item) { - return { kind: 'UpdateElan', success: await this.updateElan(currentVersion) } + return { kind: 'UpdateElan', success: await this.updateElan(mode.versions.currentVersion) } } return { kind: 'OtherItem', choice } } - async displayUpdateElanPrompt( - severity: NotificationSeverity, - currentVersion: SemVer, - recommendedVersion: SemVer, - ): Promise { - const r = await this.displayUpdateElanPromptWithItems(severity, currentVersion, recommendedVersion) + async displayUpdateElanPrompt(severity: NotificationSeverity, mode: UpdateElanMode): Promise { + const r = await this.displayUpdateElanPromptWithItems(severity, mode) if (r !== undefined && r.kind === 'UpdateElan') { return r.success } @@ -268,21 +264,38 @@ export class LeanInstaller { displayStickyUpdateElanPrompt( severity: NotificationSeverity, - currentVersion: SemVer, - recommendedVersion: SemVer, + mode: UpdateElanMode, // eslint-disable-next-line @typescript-eslint/no-redundant-type-constituents options: StickyNotificationOptions<'Update Elan' | string>, - ...otherItems: StickyInput[] + otherItems: StickyInput[] = [], ): Disposable { - const p = this.updateElanPrompt(currentVersion, recommendedVersion) + const p = this.updateElanPrompt(mode) const updateElanItem: StickyInput<'Update Elan'> = { input: p.item, continueDisplaying: false, action: async () => { - await this.updateElan(currentVersion) + await this.updateElan(mode.versions.currentVersion) }, } - return displayStickyNotificationWithOptionalInput(severity, p.message, options, updateElanItem, ...otherItems) + return displayStickyNotificationWithOptionalInput(severity, p.message, options, [updateElanItem, ...otherItems]) + } + + async displayManualUpdateElanPrompt() { + const versionResult = await elanVersion() + switch (versionResult.kind) { + case 'Success': + await this.displayUpdateElanPrompt('Information', { + kind: 'Manual', + versions: { currentVersion: versionResult.version }, + }) + break + case 'ElanNotInstalled': + displayNotification('Error', 'Elan is not installed.') + break + case 'ExecutionError': + displayNotification('Error', `Error while determining current Elan version: ${versionResult.message}`) + break + } } private async autoInstall(): Promise { @@ -291,16 +304,36 @@ export class LeanInstaller { logger.log('[LeanInstaller] Elan installed') } - private async installElan(): Promise<'Success' | 'InstallationFailed' | 'PendingInstallation'> { - if (this.installing) { - displayNotification( - 'Error', - 'Elan is already being installed. Please wait until the installation has finished.', - ) - return 'PendingInstallation' + private async installElanAndDisplaySettingPrompt(): Promise<'Success' | 'InstallationFailed' | 'PendingOperation'> { + const r = await this.installElan() + + if (r !== 'Success') { + return r + } + + const prompt = + 'Elan installation successful!\n\n' + + 'Do you want Elan in VS Code to continue downloading and installing Lean versions automatically, or would you prefer it to ask for confirmation before downloading and installing new Lean versions?\n' + + 'Asking for confirmation is especially desirable if you are ever using a limited internet data plan or your internet connection tends to be slow, whereas automatic installs are less tedious on fast and unlimited internet connections.' + + const choice = await displayNotificationWithInput( + 'Information', + prompt, + ['Always Ask For Confirmation'], + 'Install Lean Versions Automatically', + ) + if (choice === 'Always Ask For Confirmation') { + await setAlwaysAskBeforeInstallingLeanVersions(true) } - this.installing = true - try { + if (choice === 'Install Lean Versions Automatically') { + await setAlwaysAskBeforeInstallingLeanVersions(false) + } + + return r + } + + private async installElan(): Promise<'Success' | 'InstallationFailed' | 'PendingOperation'> { + return await this.performOperation('Install', async () => { const terminalName = 'Lean installation via elan' let terminalOptions: TerminalOptions = { name: terminalName } @@ -345,15 +378,68 @@ export class LeanInstaller { } const result = await resultPromise - this.elanDefaultToolchain = this.freshInstallDefaultToolchain if (!result) { displayNotification('Error', 'Elan installation failed. Check the terminal output for details.') return 'InstallationFailed' } - return 'Success' - } finally { - this.installing = false + }) + } + + async uninstallElan() { + await this.performOperation('Uninstall', async () => { + const prompt = + "This command will uninstall Lean's version manager Elan and all installed Lean versions.\n\n" + + 'Do you wish to proceed?' + const choice = await displayNotificationWithInput('Information', prompt, ['Proceed']) + if (choice !== 'Proceed') { + return + } + + const r = await elanSelfUninstall(this.outputChannel, 'Uninstall Elan') + switch (r.exitCode) { + case ExecutionExitCode.Success: + displayNotification('Information', 'Elan uninstalled successfully.') + break + case ExecutionExitCode.CannotLaunch: + displayNotification('Error', 'Elan is not installed.') + break + case ExecutionExitCode.ExecutionError: + displayNotification('Error', `Error while installing Elan: ${r.combined}`) + break + case ExecutionExitCode.Cancelled: + displayNotification('Information', 'Uninstalling Elan cancelled.') + } + }) + } + + private async performOperation( + kind: 'Install' | 'Update' | 'Uninstall', + op: () => Promise, + ): Promise { + switch (this.pendingOperation) { + case 'Install': + displayNotification( + 'Error', + 'Elan is being installed. Please wait until the installation has finished.', + ) + return 'PendingOperation' + case 'Update': + displayNotification('Error', 'Elan is being updated. Please wait until the update has finished.') + return 'PendingOperation' + case 'Uninstall': + displayNotification( + 'Error', + 'Elan is being uninstalled. Please wait until the deinstallation has finished.', + ) + return 'PendingOperation' + case undefined: + this.pendingOperation = kind + try { + return await op() + } finally { + this.pendingOperation = undefined + } } } } diff --git a/vscode-lean4/src/utils/notifs.ts b/vscode-lean4/src/utils/notifs.ts index e3ce6dbba..2b1c1b01e 100644 --- a/vscode-lean4/src/utils/notifs.ts +++ b/vscode-lean4/src/utils/notifs.ts @@ -1,5 +1,5 @@ /* eslint-disable @typescript-eslint/no-redundant-type-constituents */ -import { Disposable, MessageOptions, commands, window } from 'vscode' +import { Disposable, MessageItem, MessageOptions, commands, window } from 'vscode' import { lean } from './leanEditorProvider' // All calls to window.show(Error|Warning|Information)... should go through functions in this file @@ -146,9 +146,48 @@ export function displayStickyNotification( export async function displayNotificationWithInput( severity: NotificationSeverity, message: string, - ...items: T[] + items: T[], + defaultItem?: T | undefined, ): Promise { - return await toNotif(severity)(message, { modal: true }, ...items) + if (defaultItem === undefined) { + // VS Code renders buttons for modal notifications in the reverse order (which it doesn't do for non-modal notifications), + // so we reverse them for consistency. + // The close button is placed to the left of the primary button. + return await toNotif(severity)(message, { modal: true }, ...[...items].reverse()) + } + + let notif: ( + message: string, + options: MessageOptions, + ...items: V[] + ) => Thenable + switch (severity) { + case 'Information': + notif = window.showInformationMessage + break + case 'Warning': + notif = window.showWarningMessage + break + case 'Error': + notif = window.showErrorMessage + break + } + const messageItems = items.map(item => ({ + title: item, + isCloseAffordance: false, + })) + // VS Code always moves the `isCloseAffordance: true` button to the left of the primary button. + messageItems.push({ + title: defaultItem, + isCloseAffordance: true, + }) + messageItems.reverse() + const choice = await notif(message, { modal: true }, ...messageItems) + return choice?.title +} + +export async function displayModalNotification(severity: NotificationSeverity, message: string) { + await displayNotificationWithInput(severity, message, [], 'Close') } export type Input = { input: T; action: () => void } @@ -177,7 +216,7 @@ export function displayStickyNotificationWithOptionalInput( severity: NotificationSeverity, message: string, options: StickyNotificationOptions, - ...inputs: StickyInput[] + inputs: StickyInput[], ): Disposable { const updatedOptions: StickyNotificationOptions = { ...options, @@ -199,8 +238,8 @@ export function displayStickyNotificationWithOptionalInput( export function displayNotificationWithOutput( severity: NotificationSeverity, message: string, + otherInputs: Input[] = [], finalizer?: (() => void) | undefined, - ...otherInputs: Input[] ) { displayNotificationWithOptionalInput( severity, @@ -216,9 +255,10 @@ export function displayNotificationWithOutput( export async function displayModalNotificationWithOutput( severity: NotificationSeverity, message: string, - ...otherItems: string[] + otherItems: string[] = [], + defaultItem?: string | undefined, ): Promise<'Show Output' | string | undefined> { - const choice = await displayNotificationWithInput(severity, message, 'Show Output', ...otherItems) + const choice = await displayNotificationWithInput(severity, message, ['Show Output', ...otherItems], defaultItem) if (choice === 'Show Output') { await commands.executeCommand('lean4.troubleshooting.showOutput') } @@ -229,21 +269,21 @@ export function displayStickyNotificationWithOutput( severity: NotificationSeverity, message: string, options: StickyNotificationOptions<'Show Output' | string>, - ...otherInputs: StickyInput[] + otherInputs: StickyInput[] = [], ): Disposable { const showOutputItem: StickyInput<'Show Output'> = { input: 'Show Output', continueDisplaying: true, action: async () => await commands.executeCommand('lean4.troubleshooting.showOutput'), } - return displayStickyNotificationWithOptionalInput(severity, message, options, showOutputItem, ...otherInputs) + return displayStickyNotificationWithOptionalInput(severity, message, options, [showOutputItem, ...otherInputs]) } export function displayNotificationWithSetupGuide( severity: NotificationSeverity, message: string, + otherInputs: Input[] = [], finalizer?: (() => void) | undefined, - ...otherInputs: Input[] ) { displayNotificationWithOptionalInput( severity, @@ -260,22 +300,28 @@ export function displayStickyNotificationWithSetupGuide( severity: NotificationSeverity, message: string, options: StickyNotificationOptions<'Open Setup Guide' | string>, - ...otherInputs: StickyInput[] + otherInputs: StickyInput[] = [], ): Disposable { const openSetupGuideItem: StickyInput<'Open Setup Guide'> = { input: 'Open Setup Guide', continueDisplaying: true, action: async () => await commands.executeCommand('lean4.docs.showSetupGuide'), } - return displayStickyNotificationWithOptionalInput(severity, message, options, openSetupGuideItem, ...otherInputs) + return displayStickyNotificationWithOptionalInput(severity, message, options, [openSetupGuideItem, ...otherInputs]) } export async function displayModalNotificationWithSetupGuide( severity: NotificationSeverity, message: string, - ...otherItems: string[] + otherItems: string[] = [], + defaultItem?: string | undefined, ): Promise<'Open Setup Guide' | string | undefined> { - const choice = await displayNotificationWithInput(severity, message, 'Open Setup Guide', ...otherItems) + const choice = await displayNotificationWithInput( + severity, + message, + ['Open Setup Guide', ...otherItems], + defaultItem, + ) if (choice === 'Open Setup Guide') { await commands.executeCommand('lean4.docs.showSetupGuide') } diff --git a/vscode-lean4/src/utils/releaseQuery.ts b/vscode-lean4/src/utils/releaseQuery.ts new file mode 100644 index 000000000..4fffd6e16 --- /dev/null +++ b/vscode-lean4/src/utils/releaseQuery.ts @@ -0,0 +1,111 @@ +import { ProgressLocation, ProgressOptions, window } from 'vscode' +import { z } from 'zod' + +async function fetchJson( + context: string | undefined, +): Promise<{ kind: 'Success'; result: any } | { kind: 'CannotFetch'; error: string } | { kind: 'CannotParse' }> { + const titlePrefix = context ? `[${context}] ` : '' + const progressOptions: ProgressOptions = { + location: ProgressLocation.Notification, + title: titlePrefix + 'Querying Lean release information', + cancellable: true, + } + + let r: Response + try { + r = await window.withProgress(progressOptions, async (_, tk) => { + const controller = new AbortController() + const signal = controller.signal + tk.onCancellationRequested(() => controller.abort()) + return await fetch('https://release.lean-lang.org/', { + signal, + }) + }) + } catch (e) { + if (e instanceof Error) { + return { kind: 'CannotFetch', error: e.message } + } + return { kind: 'CannotFetch', error: 'Unknown error' } + } + + let j: any + try { + j = await r.json() + } catch (e) { + return { kind: 'CannotParse' } + } + return { kind: 'Success', result: j } +} + +function zodReleaseChannel() { + return z.array( + z.object({ + name: z.string(), + created_at: z.string().datetime(), + }), + ) +} + +export type LeanRelease = { + name: string + creationDate: Date +} + +export type LeanReleaseChannel = LeanRelease[] + +export type LeanReleases = { + version: string + stable: LeanReleaseChannel + beta: LeanReleaseChannel + nightly: LeanReleaseChannel +} + +function convertLeanReleaseChannel( + zodReleaseChannel: { + name: string + created_at: string + }[], +): LeanReleaseChannel { + return zodReleaseChannel.map(release => ({ + name: release.name, + creationDate: new Date(release.created_at), + })) +} + +function parseLeanReleases(json: any): LeanReleases | undefined { + const leanReleasesSchema = z.object({ + version: z.string(), + stable: zodReleaseChannel(), + beta: zodReleaseChannel(), + nightly: zodReleaseChannel(), + }) + const r = leanReleasesSchema.safeParse(json) + if (!r.success) { + return undefined + } + return { + version: r.data.version, + stable: convertLeanReleaseChannel(r.data.stable), + beta: convertLeanReleaseChannel(r.data.beta), + nightly: convertLeanReleaseChannel(r.data.nightly), + } +} + +export type LeanReleasesQueryResult = + | { kind: 'Success'; releases: LeanReleases } + | { kind: 'CannotFetch'; error: string } + | { kind: 'CannotParse' } + | { kind: 'Cancelled' } + +export async function queryLeanReleases(context: string | undefined): Promise { + const fetchJsonResult = await fetchJson(context) + if (fetchJsonResult.kind !== 'Success') { + return fetchJsonResult + } + const json = fetchJsonResult.result + const releases = parseLeanReleases(json) + if (releases === undefined) { + return { kind: 'CannotParse' } + } + return { kind: 'Success', releases } +} diff --git a/vscode-lean4/test/suite/simple/simple.test.ts b/vscode-lean4/test/suite/simple/simple.test.ts index e5148da39..513495504 100644 --- a/vscode-lean4/test/suite/simple/simple.test.ts +++ b/vscode-lean4/test/suite/simple/simple.test.ts @@ -2,7 +2,7 @@ import assert from 'assert' import { suite } from 'mocha' import * as path from 'path' import * as vscode from 'vscode' -import { UntitledUri } from '../../../src/utils/exturi' +import { elanInstalledToolchains } from '../../../src/utils/elan' import { logger } from '../../../src/utils/logger' import { displayNotification } from '../../../src/utils/notifs' import { @@ -64,17 +64,16 @@ suite('Lean4 Basics Test Suite', () => { const installer = features.installer assert(installer, 'No LeanInstaller export') - const toolChains = await installer.elanListToolChains(new UntitledUri()) - let defaultToolChain = toolChains.find(tc => tc.indexOf('default') > 0) - if (defaultToolChain) { + const defaultToolchainResult = await elanInstalledToolchains() + if (defaultToolchainResult.kind === 'Success' && defaultToolchainResult.defaultToolchain !== undefined) { + let defaultToolchain = defaultToolchainResult.defaultToolchain // the IO.appPath should output something like this: // FilePath.mk "/home/.elan/toolchains/leanprover--lean4---nightly/bin/lean.exe" // So let's try and find the 'leanprover--lean4---nightly' part. - defaultToolChain = defaultToolChain.replace(' (default)', '').trim() - defaultToolChain = defaultToolChain.replace('/', '--') - defaultToolChain = defaultToolChain.replace(':', '---') + defaultToolchain = defaultToolchain.replace('/', '--') + defaultToolchain = defaultToolchain.replace(':', '---') // make sure this string exists in the info view. - await waitForInfoviewHtml(info, defaultToolChain) + await waitForInfoviewHtml(info, defaultToolchain) } // make sure test is always run in predictable state, which is no file or folder open diff --git a/vscode-lean4/tsconfig.json b/vscode-lean4/tsconfig.json index b9782876a..3c7c8e187 100644 --- a/vscode-lean4/tsconfig.json +++ b/vscode-lean4/tsconfig.json @@ -10,6 +10,7 @@ "alwaysStrict": true, "rootDir": "./", "noImplicitAny": true, + "noFallthroughCasesInSwitch": true, "strictNullChecks": true, "esModuleInterop": true },