From 66597f29d0a740013530adc77abf91d5a99d5610 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Fri, 22 Nov 2024 18:34:02 +0100 Subject: [PATCH] feat: support for elan 4.0.0 --- package-lock.json | 2 +- vscode-lean4/package.json | 92 ++- vscode-lean4/src/config.ts | 16 +- .../src/diagnostics/fullDiagnostics.ts | 96 ++- .../src/diagnostics/setupDiagnoser.ts | 117 +++- .../src/diagnostics/setupDiagnostics.ts | 64 +- vscode-lean4/src/diagnostics/setupNotifs.ts | 109 +-- vscode-lean4/src/exports.ts | 2 + vscode-lean4/src/extension.ts | 56 +- vscode-lean4/src/leanclient.ts | 110 ++- vscode-lean4/src/projectinit.ts | 86 ++- vscode-lean4/src/projectoperations.ts | 26 +- vscode-lean4/src/utils/batch.ts | 33 +- vscode-lean4/src/utils/clientProvider.ts | 22 +- vscode-lean4/src/utils/elan.ts | 663 +++++++++++++++++- vscode-lean4/src/utils/elanCommands.ts | 517 ++++++++++++++ vscode-lean4/src/utils/groupBy.ts | 18 + vscode-lean4/src/utils/internalErrors.ts | 3 +- vscode-lean4/src/utils/lake.ts | 56 +- vscode-lean4/src/utils/leanCmdRunner.ts | 417 +++++++++++ vscode-lean4/src/utils/leanEditorProvider.ts | 27 +- vscode-lean4/src/utils/leanInstaller.ts | 246 ++++--- vscode-lean4/src/utils/notifs.ts | 74 +- vscode-lean4/src/utils/releaseQuery.ts | 111 +++ vscode-lean4/test/suite/simple/simple.test.ts | 15 +- vscode-lean4/tsconfig.json | 1 + 26 files changed, 2570 insertions(+), 409 deletions(-) create mode 100644 vscode-lean4/src/utils/elanCommands.ts create mode 100644 vscode-lean4/src/utils/groupBy.ts create mode 100644 vscode-lean4/src/utils/leanCmdRunner.ts create mode 100644 vscode-lean4/src/utils/releaseQuery.ts diff --git a/package-lock.json b/package-lock.json index 3e8ff2ee1..5adc8ba6d 100644 --- a/package-lock.json +++ b/package-lock.json @@ -17015,7 +17015,7 @@ }, "vscode-lean4": { "name": "lean4", - "version": "0.0.184", + "version": "0.0.185", "license": "Apache-2.0", "dependencies": { "@leanprover/infoview": "~0.7.0", diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json index a95eae3f9..40b02e1b4 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 prompt whenever Elan will download and install a new Lean version" + }, "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": "lean4.isLeanFeatureSetActive || lean4.isLeanFeatureSetActive", + "group": "1_toolchains@1" + }, + { + "command": "lean4.setup.updateReleaseChannel", + "when": "lean4.isLeanFeatureSetActive || lean4.isLeanFeatureSetActive", + "group": "1_toolchains@2" + }, + { + "command": "lean4.setup.uninstallToolchains", + "when": "lean4.isLeanFeatureSetActive || 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..6726abae4 100644 --- a/vscode-lean4/src/config.ts +++ b/vscode-lean4/src/config.ts @@ -1,4 +1,4 @@ -import { workspace } from 'vscode' +import { ConfigurationTarget, workspace } from 'vscode' import { PATH } from './utils/envPath' // TODO: does currently not contain config options for `./abbreviation` @@ -17,6 +17,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', []) } 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..c4ddb16ee 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, + isElanDumpStateVersion, +} 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' && !isElanDumpStateVersion(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' && !isElanDumpStateVersion(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/leanclient.ts b/vscode-lean4/src/leanclient.ts index 48dbb2515..ec4353614 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() @@ -181,18 +199,61 @@ export class LeanClient implements Disposable { title: '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..55645dcce 100644 --- a/vscode-lean4/src/projectinit.ts +++ b/vscode-lean4/src/projectinit.ts @@ -34,9 +34,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 +56,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', + }), ) } @@ -83,12 +91,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 +127,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 +142,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 } @@ -181,21 +192,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 +293,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 +396,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 +432,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..e1c3dac60 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 @@ -87,7 +87,8 @@ export class ProjectOperationProvider implements Disposable { 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 } @@ -333,7 +334,7 @@ export class ProjectOperationProvider implements Disposable { : `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 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 @@ -343,13 +344,13 @@ export class ProjectOperationProvider implements Disposable { } 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 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..a9bf6871f 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', + }) }, ) } @@ -130,7 +132,7 @@ export class LeanClientProvider implements Disposable { const preconditionCheckResult = await checkLean4ProjectPreconditions( this.outputChannel, - 'Restart Client', + 'Client Restart', projectUri, ) if (preconditionCheckResult !== 'Fatal') { @@ -224,9 +226,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,7 +245,7 @@ export class LeanClientProvider implements Disposable { const preconditionCheckResult = await checkLean4ProjectPreconditions( this.outputChannel, - 'Start Client', + 'Client Startup', folderUri, ) if (preconditionCheckResult === 'Fatal') { @@ -255,9 +254,7 @@ export class LeanClientProvider implements Disposable { } 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) @@ -276,12 +273,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..143190043 100644 --- a/vscode-lean4/src/utils/elan.ts +++ b/vscode-lean4/src/utils/elan.ts @@ -1,6 +1,663 @@ +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 }) +// 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 ElanDefaultToolchain = { + unresolved: ElanUnresolvedToolchain + resolved: ElanResult +} + +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 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 convertElanResult( + zodResult: + | { + Ok: T + } + | { + Err: string + }, + f: (v: T) => V, +): ElanResult { + if ('Ok' in zodResult) { + return { kind: 'Ok', value: f(zodResult.Ok) } + } + if ('Err' in zodResult) { + return { kind: 'Error', message: zodResult.Err } + } + return zodResult +} + +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 } + } + if ('Remote' in zodElanUnresolvedToolchain) { + return { + kind: 'Remote', + githubRepoOrigin: zodElanUnresolvedToolchain.Remote.origin, + release: zodElanUnresolvedToolchain.Remote.release, + fromChannel: convertElanOption(zodElanUnresolvedToolchain.Remote.from_channel, c => c), + } + } + return zodElanUnresolvedToolchain +} + +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) } + } + if ('InToolchainDirectory' in zodElanOverrideReason) { + return { kind: 'ToolchainDirectory', directoryPath: new FileUri(zodElanOverrideReason.InToolchainDirectory) } + } + return zodElanOverrideReason +} + +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: zodElanResult(z.string()), + }), + ), + 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(zodElanResult(z.string())), + }), + }) + const stateDumpResult = stateDumpSchema.safeParse(parsedJson) + if (!stateDumpResult.success) { + return undefined + } + const s = stateDumpResult.data + + const stateDump: ElanStateDump = { + elanVersion: { + current: new SemVer(s.elan_version.current), + newest: convertElanResult(s.elan_version.newest, version => new SemVer(version)), + }, + toolchains: { + installed: groupByUniqueKey( + s.toolchains.installed.map(i => ({ resolvedName: i.resolved_name, path: new FileUri(i.path) })), + i => i.resolvedName, + ), + default: convertElanOption(s.toolchains.default, d => ({ + unresolved: convertElanUnresolvedToolchain(d.unresolved), + resolved: convertElanResult(d.resolved, r => r), + })), + activeOverride: convertElanOption(s.toolchains.active_override, r => ({ + reason: convertElanOverrideReason(r.reason), + unresolved: convertElanUnresolvedToolchain(r.unresolved), + })), + resolvedActive: convertElanOption(s.toolchains.resolved_active, r => convertElanResult(r, a => a)), + }, + } + 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 function isElanEagerToolchainResolutionVersion(elanVersion: SemVer): boolean { + return elanVersion.major >= 3 +} + +export function isElanDumpStateVersion(elanVersion: SemVer): boolean { + return elanVersion.major >= 3 +} + +export function isElanGcVersion(elanVersion: SemVer): boolean { + return elanVersion.major >= 3 +} + +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 stateDumpWithoutNetResult = await elanDumpStateWithoutNet(cwdUri, toolchain) + if (stateDumpWithoutNetResult.kind !== 'Success') { + return stateDumpWithoutNetResult + } + + const cachedToolchainInfo = stateDumpWithoutNetResult.state.toolchains.resolvedActive + if (cachedToolchainInfo === undefined) { + return { kind: 'NoActiveToolchain' } + } + let cachedToolchain: string | undefined + if ( + cachedToolchainInfo.kind === 'Ok' && + stateDumpWithoutNetResult.state.toolchains.installed.has(cachedToolchainInfo.value) + ) { + cachedToolchain = cachedToolchainInfo.value + } + + const stateDumpWithNetResult = await elanDumpStateWithNet(cwdUri, context, toolchain) + if (stateDumpWithNetResult.kind !== 'Success') { + return stateDumpWithNetResult + } + + const overrideInfo = stateDumpWithNetResult.state.toolchains.activeOverride + let unresolvedToolchain: string + if (overrideInfo === undefined) { + const defaultToolchainInfo = stateDumpWithNetResult.state.toolchains.default + if (defaultToolchainInfo === undefined) { + return { kind: 'NoActiveToolchain' } + } + unresolvedToolchain = ElanUnresolvedToolchain.toolchainName(defaultToolchainInfo.unresolved) + } else { + unresolvedToolchain = ElanUnresolvedToolchain.toolchainName(overrideInfo.unresolved) + } + + const resolvedToolchainInfo = stateDumpWithNetResult.state.toolchains.resolvedActive + if (resolvedToolchainInfo === undefined) { + return { kind: 'NoActiveToolchain' } + } + if (resolvedToolchainInfo.kind === 'Error') { + return { kind: 'ExecutionError', message: resolvedToolchainInfo.message } + } + const resolvedToolchain = resolvedToolchainInfo.value + + const overrideReason = overrideInfo?.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'], context, 'Uninstalling Elan', { + channel, + allowCancellation: true, + }) +} + +export async function elanSetDefaultToolchain( + channel: OutputChannel | undefined, + context: string | undefined, + toolchain: string, +) { + return await batchExecuteWithProgress('elan', ['default', toolchain], context, 'Setting default Lean version', { + channel, + allowCancellation: true, + }) +} + +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..61d9077fe --- /dev/null +++ b/vscode-lean4/src/utils/elanCommands.ts @@ -0,0 +1,517 @@ +import { promises } from 'fs' +import { commands, Disposable, OutputChannel, QuickPickItem, QuickPickItemKind, window } from 'vscode' +import { ExecutionExitCode } from './batch' +import { LeanClientProvider } from './clientProvider' +import { + ActiveToolchainInfo, + elanActiveToolchain, + elanInstalledToolchains, + elanInstallToolchain, + elanQueryGc, + elanSetDefaultToolchain, + elanUninstallToolchains, + elanVersion, + isElanDumpStateVersion, + toolchainVersion, +} from './elan' +import { FileUri, UntitledUri } from './exturi' +import { fileExists } from './fsHelper' +import { groupByUniqueKey } 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 + } + + const 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, + selectDefaultToolchainContext, + selectedDefaultToolchain, + ) + switch (setDefaultToolchainResult.exitCode) { + case ExecutionExitCode.Success: + displayNotification( + 'Information', + `Default Lean version '${selectedDefaultToolchain}' set successfully.`, + ) + const clientForUntitledFiles = this.clientProvider?.findClient(new UntitledUri()) + await clientForUntitledFiles?.restart() + break + case ExecutionExitCode.CannotLaunch: + displayNotification('Error', 'Cannot set Lean default version: Elan is not installed.') + break + case ExecutionExitCode.ExecutionError: + displayNotification('Error', `Cannot set Lean default version: ${setDefaultToolchainResult.combined}`) + break + case ExecutionExitCode.Cancelled: + displayNotification( + 'Information', + 'Default Lean version selection cancelled. Default Lean version has not been set.', + ) + break + } + } + + async updateReleaseChannel() { + if (!(await this.checkElanSupportsDumpState())) { + return + } + + const context = 'Update Release Channel Lean Version' + const channels = [ + { + name: 'Stable', + identifier: 'leanprover/lean4:stable', + }, + { + name: 'Nightly', + identifier: 'leanprover/lean4:nightly', + }, + ] + + 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 = groupByUniqueKey(queryGcResult.info.usedToolchains, u => u.toolchain) + + const toolchainInfo = await this.installedToolchains() + if (toolchainInfo === undefined) { + return + } + const installedToolchains = toolchainInfo.toolchains.filter(t => t !== toolchainInfo.defaultToolchain) + if (installedToolchains.length === 0) { + displayNotification('Information', 'No non-default Lean version installed.') + return + } + const installedToolchainItems = installedToolchains.map(t => { + let user = usedToolchainIndex.get(t)?.user + if (user === 'default toolchain') { + // Translate Elan nomenclature to vscode-lean4 nomenclature + user = 'default Lean version' + } else if (user !== undefined) { + user = `'${user}'` + } + return { + label: t, + description: user !== undefined ? `(used by ${user})` : '(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 the project.\n\n` + + 'After setting the Lean version of the project, Lean code in this project that worked before may be incompatible with the new Lean version.\n' + + "Additionally, if your project has a 'lakefile.lean' or a 'lakefile.toml', the project configuration may be incompatible with the new version.\n" + + 'Finally, Lake project dependencies that worked before may also be incompatible with the new version and may potentially need to be updated to a version that supports the new Lean version of this project. ' + + "If you simply want to update a dependency 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.\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 stableChannel = 'leanprover/lean4:stable' + 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/'.", + ) + } + 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: stableChannel, + 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 === stableChannel) { + return stableChannel + } 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 + } + 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 (!isElanDumpStateVersion(r.version)) { + displayNotification( + 'Error', + `This command can only be used with Elan versions >= 4.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..4269451e5 --- /dev/null +++ b/vscode-lean4/src/utils/leanCmdRunner.ts @@ -0,0 +1,417 @@ +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, + 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 { + let toolchainName: string + if (unresolvedActiveToolchain.fromChannel !== undefined) { + const prefix = activeOverride === undefined ? 'default ' : '' + toolchainName = `Lean version for ${prefix}release channel '${unresolvedActiveToolchain.fromChannel}'` + } else { + const prefix = activeOverride === undefined ? 'Default ' : '' + toolchainName = `${prefix}Lean version '${ElanUnresolvedToolchain.toolchainName(unresolvedActiveToolchain)}'` + } + + const or = overrideReason(activeOverride) + return `${toolchainName}${or !== undefined ? ' ' + or : ''} is not installed.` +} + +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. Do you want 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 = + elanState.toolchains.activeOverride?.unresolved ?? elanState.toolchains.default?.unresolved + const resolvedToolchainResult = elanState.toolchains.resolvedActive + if (unresolvedToolchain === undefined || resolvedToolchainResult === undefined) { + return runWithActiveToolchain + } + + if (unresolvedToolchain.kind === 'Local') { + return runWithActiveToolchain + } + + let cachedToolchain: string | undefined + switch (resolvedToolchainResult.kind) { + case 'Error': + cachedToolchain = undefined + break + case 'Ok': + if (elanState.toolchains.installed.has(resolvedToolchainResult.value)) { + cachedToolchain = resolvedToolchainResult.value + } else { + cachedToolchain = undefined + } + break + } + + 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', + `${leanNotInstalledError(elanState.toolchains.activeOverride?.reason, unresolvedToolchain)} Do you want to install it?`, + ['Install Version'], + ) + if (choice === undefined) { + return { + kind: 'Error', + message: leanNotInstalledError(elanState.toolchains.activeOverride?.reason, unresolvedToolchain), + } + } + if (choice === 'Install Version') { + return await installNewToolchain() + } + return choice + } + + 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 = + elanState.toolchains.activeOverride?.unresolved ?? elanState.toolchains.default?.unresolved + const resolvedToolchainResult = elanState.toolchains.resolvedActive + if (unresolvedToolchain === undefined || resolvedToolchainResult === undefined) { + return runWithActiveToolchain + } + + if (unresolvedToolchain.kind === 'Local' || unresolvedToolchain.fromChannel === undefined) { + return runWithActiveToolchain + } + + 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, + unresolvedToolchain.fromChannel, + cachedToolchain, + resolvedToolchain, + ), + ['Update Lean Version'], + 'Use Old Version', + ) + if (choice === undefined || choice === 'Use Old Version') { + return runWithCachedToolchain(undefined) + } + if (choice === 'Update Lean Version') { + return await updateToolchain() + } + return choice + } + + 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) { + 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) + } + if (toolchainDecision.kind === 'RunWithSpecificToolchain') { + return await this.runCmd(executablePath, args, options, toolchainDecision.toolchain) + } + return toolchainDecision + } +} + +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..26109f7bc 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, isElanEagerToolchainResolutionVersion } from './elan' +import { FileUri } from './exturi' import { logger } from './logger' import { NotificationSeverity, @@ -20,6 +20,16 @@ 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' @@ -27,9 +37,6 @@ export class LeanInstaller { private prompting: boolean = false private installing: boolean = false 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,68 +97,6 @@ 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 = @@ -163,7 +108,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,7 +118,7 @@ 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 } @@ -195,7 +141,7 @@ 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'> = { @@ -205,16 +151,51 @@ export class LeanInstaller { await this.installElan() }, } - 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: 'Do you want to update Elan?', + 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. Do you want to update Elan?`, + item: 'Update Elan', + } + } + } + + private async displayElanUpdateSuccessfulPrompt(currentVersion: SemVer) { + if (!isElanEagerToolchainResolutionVersion(currentVersion)) { + displayNotification('Information', 'Elan update successful!') + return + } + + const prompt = + 'Elan update successful!' + + '\n\n' + + 'Do you want Elan in VS Code to download and install 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) } } @@ -222,10 +203,14 @@ export class LeanInstaller { 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' + if (installElanResult !== 'Success') { + return false + } + await this.displayElanUpdateSuccessfulPrompt(currentVersion) + return true } - const elanSelfUpdateResult = await elanSelfUpdate(this.outputChannel) + const elanSelfUpdateResult = await elanSelfUpdate(this.outputChannel, 'Update Elan') if (elanSelfUpdateResult.exitCode !== ExecutionExitCode.Success) { displayResultError( elanSelfUpdateResult, @@ -234,32 +219,30 @@ export class LeanInstaller { return false } + await this.displayElanUpdateSuccessfulPrompt(currentVersion) + return true } 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 +251,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 { @@ -345,15 +345,59 @@ 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' } + const prompt = + 'Elan installation successful!' + + '\n\n' + + 'Do you want Elan in VS Code to download and install 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) + } + return 'Success' } finally { this.installing = false } } + + async uninstallElan() { + const prompt = + "This command will uninstall Lean's version manager Elan and all installed Lean version.\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.') + } + } } 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 },