diff --git a/vscode-lean4/src/diagnostics/setupDiagnoser.ts b/vscode-lean4/src/diagnostics/setupDiagnoser.ts index c4ddb16e..74d39212 100644 --- a/vscode-lean4/src/diagnostics/setupDiagnoser.ts +++ b/vscode-lean4/src/diagnostics/setupDiagnoser.ts @@ -7,7 +7,7 @@ import { ElanDumpStateWithoutNetResult, elanDumpStateWithNet, elanDumpStateWithoutNet, - isElanDumpStateVersion, + isElanEagerResolutionVersion, } from '../utils/elan' import { FileUri } from '../utils/exturi' import { ToolchainUpdateMode, leanRunner } from '../utils/leanCmdRunner' @@ -245,7 +245,7 @@ export class SetupDiagnoser { const dumpStateResult = await elanDumpStateWithoutNet(this.cwdUri, this.toolchain) if (dumpStateResult.kind === 'ExecutionError') { const versionResult = await this.queryElanVersion() - if (versionResult.kind === 'Success' && !isElanDumpStateVersion(versionResult.version)) { + if (versionResult.kind === 'Success' && !isElanEagerResolutionVersion(versionResult.version)) { return { kind: 'PreEagerResolutionVersion' } } } @@ -256,7 +256,7 @@ export class SetupDiagnoser { const dumpStateResult = await elanDumpStateWithNet(this.cwdUri, this.toolchain) if (dumpStateResult.kind === 'ExecutionError') { const versionResult = await this.queryElanVersion() - if (versionResult.kind === 'Success' && !isElanDumpStateVersion(versionResult.version)) { + if (versionResult.kind === 'Success' && !isElanEagerResolutionVersion(versionResult.version)) { return { kind: 'PreEagerResolutionVersion' } } } diff --git a/vscode-lean4/src/utils/elan.ts b/vscode-lean4/src/utils/elan.ts index 14319004..0ac31d70 100644 --- a/vscode-lean4/src/utils/elan.ts +++ b/vscode-lean4/src/utils/elan.ts @@ -5,6 +5,12 @@ import { batchExecute, batchExecuteWithProgress, ExecutionExitCode, ExecutionRes import { FileUri } from './exturi' import { groupByUniqueKey } from './groupBy' +export const elanEagerResolutionMajorVersion = 3 // TODO: for debugging purposes. Change to 4 before merge + +export function isElanEagerResolutionVersion(version: SemVer) { + return version.major >= elanEagerResolutionMajorVersion +} + // Suggested at https://semver.org/#is-there-a-suggested-regular-expression-regex-to-check-a-semver-string const semVerRegex = @@ -147,10 +153,10 @@ function convertElanResult( if ('Ok' in zodResult) { return { kind: 'Ok', value: f(zodResult.Ok) } } - if ('Err' in zodResult) { - return { kind: 'Error', message: zodResult.Err } + zodResult satisfies { + Err: string } - return zodResult + return { kind: 'Error', message: zodResult.Err } } function convertElanOption(zodNullable: T | null, f: (v: T) => V): ElanOption { @@ -178,15 +184,19 @@ function convertElanUnresolvedToolchain( 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), + zodElanUnresolvedToolchain satisfies { + Remote: { + origin: string + release: string + from_channel: string | null } } - return zodElanUnresolvedToolchain + return { + kind: 'Remote', + githubRepoOrigin: zodElanUnresolvedToolchain.Remote.origin, + release: zodElanUnresolvedToolchain.Remote.release, + fromChannel: convertElanOption(zodElanUnresolvedToolchain.Remote.from_channel, c => c), + } } function convertElanOverrideReason( @@ -217,10 +227,8 @@ function convertElanOverrideReason( 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 + zodElanOverrideReason satisfies { InToolchainDirectory: string } + return { kind: 'ToolchainDirectory', directoryPath: new FileUri(zodElanOverrideReason.InToolchainDirectory) } } function parseElanStateDump(elanDumpStateOutput: string): ElanStateDump | undefined { @@ -363,18 +371,6 @@ export async function elanDumpStateWithNet( } } -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' } @@ -573,15 +569,26 @@ export async function elanSelfUninstall( }) } +export type ElanSetDefaultToolchainResult = + | { kind: 'Success' } + | { kind: 'ElanNotFound' } + | { kind: 'Error'; message: string } + 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, - }) +): Promise { + const r = await batchExecute('elan', ['default', toolchain], undefined, { combined: channel }) + switch (r.exitCode) { + case ExecutionExitCode.Success: + return { kind: 'Success' } + case ExecutionExitCode.CannotLaunch: + return { kind: 'ElanNotFound' } + case ExecutionExitCode.ExecutionError: + return { kind: 'Error', message: r.combined } + case ExecutionExitCode.Cancelled: + throw new Error('Unexpected cancellation of `elan default `') + } } export type ElanUsedToolchain = { diff --git a/vscode-lean4/src/utils/elanCommands.ts b/vscode-lean4/src/utils/elanCommands.ts index 61d9077f..bef617e8 100644 --- a/vscode-lean4/src/utils/elanCommands.ts +++ b/vscode-lean4/src/utils/elanCommands.ts @@ -5,13 +5,14 @@ import { LeanClientProvider } from './clientProvider' import { ActiveToolchainInfo, elanActiveToolchain, + elanEagerResolutionMajorVersion, elanInstalledToolchains, elanInstallToolchain, elanQueryGc, elanSetDefaultToolchain, elanUninstallToolchains, elanVersion, - isElanDumpStateVersion, + isElanEagerResolutionVersion, toolchainVersion, } from './elan' import { FileUri, UntitledUri } from './exturi' @@ -66,13 +67,9 @@ export class ElanCommandProvider implements Disposable { return } - const setDefaultToolchainResult = await elanSetDefaultToolchain( - this.channel, - selectDefaultToolchainContext, - selectedDefaultToolchain, - ) - switch (setDefaultToolchainResult.exitCode) { - case ExecutionExitCode.Success: + const setDefaultToolchainResult = await elanSetDefaultToolchain(this.channel, selectedDefaultToolchain) + switch (setDefaultToolchainResult.kind) { + case 'Success': displayNotification( 'Information', `Default Lean version '${selectedDefaultToolchain}' set successfully.`, @@ -80,17 +77,11 @@ export class ElanCommandProvider implements Disposable { const clientForUntitledFiles = this.clientProvider?.findClient(new UntitledUri()) await clientForUntitledFiles?.restart() break - case ExecutionExitCode.CannotLaunch: + case 'ElanNotFound': 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.', - ) + case 'Error': + displayNotification('Error', `Cannot set Lean default version: ${setDefaultToolchainResult.message}`) break } } @@ -330,11 +321,12 @@ export class ElanCommandProvider implements Disposable { } 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" + + `This operation will set '${selectedProjectToolchain}' to be the Lean version of the Lean project at '${activeClientUri.fsPath}'. It is only intended to be used by maintainers of this project.\n\n` + + 'Changing the Lean version of this project may lead to breakages induced by incompatibilities with the new Lean version. For example, the following components of this project may end up being incompatible with the new Lean version:\n' + + '- The Lean code in this project\n' + + "- The 'lakefile.toml' or 'lakefile.lean' configuring this project\n" + + '- Lake dependencies of this project\n\n' + + "If you simply want to update a Lake dependency of this project and use its Lean version to ensure that the Lean version of the dependency is compatible with the Lean version of this project, it is preferable to use the 'Project: Update Dependency' command instead of this one.\n\n" + 'Do you wish to proceed?' const choice = await displayNotificationWithInput('Information', prompt, ['Proceed']) if (choice !== 'Proceed') { @@ -383,6 +375,9 @@ export class ElanCommandProvider implements Disposable { "Could not fetch Lean versions: Cannot parse response from 'https://release.lean-lang.org/'.", ) } + if (leanReleasesQueryResult.kind === 'CannotFetch') { + displayNotification('Warning', `Could not fetch Lean versions: ${leanReleasesQueryResult.error}`) + } const toToolchainNames = (channel: LeanReleaseChannel) => channel.map(t => `leanprover/lean4:${t.name}`).filter(t => !installedToolchainIndex.has(t)) if (leanReleasesQueryResult.kind === 'Success') { @@ -466,6 +461,7 @@ export class ElanCommandProvider implements Disposable { } return undefined } + r.kind satisfies 'Success' return r.info } @@ -492,10 +488,10 @@ export class ElanCommandProvider implements Disposable { const r = await elanVersion() switch (r.kind) { case 'Success': - if (!isElanDumpStateVersion(r.version)) { + if (!isElanEagerResolutionVersion(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()}.`, + `This command can only be used with Elan versions >= ${elanEagerResolutionMajorVersion}.0.0, but the installed Elan version is ${r.version.toString()}.`, ) return false } diff --git a/vscode-lean4/src/utils/leanCmdRunner.ts b/vscode-lean4/src/utils/leanCmdRunner.ts index 4269451e..14bb7648 100644 --- a/vscode-lean4/src/utils/leanCmdRunner.ts +++ b/vscode-lean4/src/utils/leanCmdRunner.ts @@ -203,10 +203,9 @@ export class LeanCommandRunner { message: leanNotInstalledError(elanState.toolchains.activeOverride?.reason, unresolvedToolchain), } } - if (choice === 'Install Version') { - return await installNewToolchain() - } - return choice + choice satisfies 'Install Version' + + return await installNewToolchain() } if (unresolvedToolchain.fromChannel === undefined) { @@ -323,10 +322,8 @@ export class LeanCommandRunner { if (choice === undefined || choice === 'Use Old Version') { return runWithCachedToolchain(undefined) } - if (choice === 'Update Lean Version') { - return await updateToolchain() - } - return choice + choice satisfies 'Update Lean Version' + return await updateToolchain() } async decideToolchain( @@ -370,7 +367,7 @@ export class LeanCommandRunner { ) if (withNetAnalysisResult.kind === 'RunWithCachedToolchain') { this.stickyUpdateDecisions.set(key, 'DoNotUpdate') - if (withNetAnalysisResult.warning) { + if (withNetAnalysisResult.warning !== undefined) { displayNotification('Warning', withNetAnalysisResult.warning) } return { kind: 'RunWithSpecificToolchain', toolchain: cachedToolchain } @@ -395,10 +392,8 @@ export class LeanCommandRunner { 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 + toolchainDecision.kind satisfies 'RunWithSpecificToolchain' + return await this.runCmd(executablePath, args, options, toolchainDecision.toolchain) } } diff --git a/vscode-lean4/src/utils/leanInstaller.ts b/vscode-lean4/src/utils/leanInstaller.ts index ea9e0c37..4392cfbe 100644 --- a/vscode-lean4/src/utils/leanInstaller.ts +++ b/vscode-lean4/src/utils/leanInstaller.ts @@ -2,7 +2,7 @@ import { SemVer } from 'semver' import { Disposable, EventEmitter, OutputChannel, TerminalOptions, window } from 'vscode' import { getPowerShellPath, isRunningTest, setAlwaysAskBeforeInstallingLeanVersions } from '../config' import { ExecutionExitCode, displayResultError } from './batch' -import { elanSelfUninstall, elanSelfUpdate, elanVersion, isElanEagerToolchainResolutionVersion } from './elan' +import { elanSelfUninstall, elanSelfUpdate, elanVersion, isElanEagerResolutionVersion } from './elan' import { FileUri } from './exturi' import { logger } from './logger' import { @@ -173,7 +173,7 @@ export class LeanInstaller { } private async displayElanUpdateSuccessfulPrompt(currentVersion: SemVer) { - if (!isElanEagerToolchainResolutionVersion(currentVersion)) { + if (isElanEagerResolutionVersion(currentVersion)) { displayNotification('Information', 'Elan update successful!') return } @@ -385,7 +385,7 @@ export class LeanInstaller { async uninstallElan() { const prompt = - "This command will uninstall Lean's version manager Elan and all installed Lean version.\n" + + "This command will uninstall Lean's version manager Elan and all installed Lean versions.\n" + 'Do you wish to proceed?' const choice = await displayNotificationWithInput('Information', prompt, ['Proceed']) if (choice !== 'Proceed') {