From a65a35723267e15a716a677c3c6eb26fdaa529c2 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Tue, 10 Dec 2024 15:15:55 +0100 Subject: [PATCH] wip --- package-lock.json | 2 +- vscode-lean4/package.json | 2 +- vscode-lean4/src/config.ts | 3 +- vscode-lean4/src/infoview.ts | 12 ++- vscode-lean4/src/projectinit.ts | 5 +- vscode-lean4/src/utils/elan.ts | 128 +++++++++++++++--------- vscode-lean4/src/utils/elanCommands.ts | 34 ++++--- vscode-lean4/src/utils/leanCmdRunner.ts | 35 ++----- 8 files changed, 129 insertions(+), 92 deletions(-) diff --git a/package-lock.json b/package-lock.json index 5adc8ba6..e6f3efb7 100644 --- a/package-lock.json +++ b/package-lock.json @@ -17015,7 +17015,7 @@ }, "vscode-lean4": { "name": "lean4", - "version": "0.0.185", + "version": "0.0.186", "license": "Apache-2.0", "dependencies": { "@leanprover/infoview": "~0.7.0", diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json index b5bc996f..111d1a58 100644 --- a/vscode-lean4/package.json +++ b/vscode-lean4/package.json @@ -84,7 +84,7 @@ "lean4.alwaysAskBeforeInstallingLeanVersions": { "type": "boolean", "default": false, - "markdownDescription": "Enable to display a confirmation prompt whenever Elan is about to download and install a new Lean version" + "markdownDescription": "Enable to display a confirmation prompt whenever Elan is about to download and install a new Lean version. Needs Elan >= 4.0.0." }, "lean4.serverArgs": { "type": "array", diff --git a/vscode-lean4/src/config.ts b/vscode-lean4/src/config.ts index 6726abae..305ab4bd 100644 --- a/vscode-lean4/src/config.ts +++ b/vscode-lean4/src/config.ts @@ -1,4 +1,5 @@ import { ConfigurationTarget, workspace } from 'vscode' +import { elanStableChannel } from './utils/elan' import { PATH } from './utils/envPath' // TODO: does currently not contain config options for `./abbreviation` @@ -119,7 +120,7 @@ export function getTestFolder(): string { export function getDefaultLeanVersion(): string { return typeof process.env.DEFAULT_LEAN_TOOLCHAIN === 'string' ? process.env.DEFAULT_LEAN_TOOLCHAIN - : 'leanprover/lean4:stable' + : elanStableChannel } /** The editor line height, in pixels. */ diff --git a/vscode-lean4/src/infoview.ts b/vscode-lean4/src/infoview.ts index 38e4dea1..1b995dd8 100644 --- a/vscode-lean4/src/infoview.ts +++ b/vscode-lean4/src/infoview.ts @@ -142,7 +142,7 @@ export class InfoProvider implements Disposable { sendClientRequest: async (uri: string, method: string, params: any): Promise => { const extUri = parseExtUri(uri) if (extUri === undefined) { - return undefined + throw Error(`Unexpected URI scheme: ${Uri.parse(uri).scheme}`) } const client = this.clientProvider.findClient(extUri) @@ -162,7 +162,7 @@ export class InfoProvider implements Disposable { throw ex } } - return undefined + throw Error('No active Lean client.') }, sendClientNotification: async (uri: string, method: string, params: any): Promise => { const extUri = parseExtUri(uri) @@ -292,15 +292,17 @@ export class InfoProvider implements Disposable { createRpcSession: async uri => { const extUri = parseExtUri(uri) if (extUri === undefined) { - return '' + throw Error(`Unexpected URI scheme: ${Uri.parse(uri).scheme}`) } const client = this.clientProvider.findClient(extUri) - if (!client) return '' + if (client === undefined) { + throw Error('No active Lean client.') + } const sessionId = await rpcConnect(client, uri) const session = new RpcSessionAtPos(client, sessionId, uri) if (!this.webviewPanel) { session.dispose() - throw Error('infoview disconnect while connecting to RPC session') + throw Error('InfoView disconnected while connecting to RPC session.') } else { this.rpcSessions.set(sessionId, session) return sessionId diff --git a/vscode-lean4/src/projectinit.ts b/vscode-lean4/src/projectinit.ts index 55645dcc..aa50263c 100644 --- a/vscode-lean4/src/projectinit.ts +++ b/vscode-lean4/src/projectinit.ts @@ -8,6 +8,7 @@ import { ExecutionExitCode, ExecutionResult, } from './utils/batch' +import { elanStableChannel } from './utils/elan' import { ExtUri, extUriToCwdUri, FileUri } from './utils/exturi' import { lake } from './utils/lake' import { LeanInstaller } from './utils/leanInstaller' @@ -81,7 +82,7 @@ export class ProjectInitializationProvider implements Disposable { private async createStandaloneProject() { const createStandaloneProjectContext = 'Create Standalone Project' - const toolchain = 'leanprover/lean4:stable' + const toolchain = elanStableChannel const projectFolder: FileUri | 'DidNotComplete' = await this.createProject( createStandaloneProjectContext, undefined, @@ -169,7 +170,7 @@ export class ProjectInitializationProvider implements Disposable { private async createProject( context: string, kind?: string | undefined, - toolchain: string = 'leanprover/lean4:stable', + toolchain: string = elanStableChannel, ): Promise { const projectFolder: FileUri | undefined = await ProjectInitializationProvider.askForNewProjectFolderLocation({ saveLabel: 'Create project folder', diff --git a/vscode-lean4/src/utils/elan.ts b/vscode-lean4/src/utils/elan.ts index 0ac31d70..c26f5727 100644 --- a/vscode-lean4/src/utils/elan.ts +++ b/vscode-lean4/src/utils/elan.ts @@ -5,7 +5,10 @@ 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 const elanStableChannel = 'leanprover/lean4:stable' +export const elanNightlyChannel = 'leanprover/lean4:nightly' + +export const elanEagerResolutionMajorVersion = 4 export function isElanEagerResolutionVersion(version: SemVer) { return version.major >= elanEagerResolutionMajorVersion @@ -83,9 +86,14 @@ export namespace ElanUnresolvedToolchain { } } +export type ElanToolchainResolution = { + resolvedToolchain: ElanResult + cachedToolchain: ElanOption +} + export type ElanDefaultToolchain = { unresolved: ElanUnresolvedToolchain - resolved: ElanResult + resolved: ElanToolchainResolution } export type ElanOverrideReason = @@ -104,7 +112,21 @@ export type ElanToolchains = { installed: Map default: ElanOption activeOverride: ElanOption - resolvedActive: ElanOption> + resolvedActive: ElanOption +} + +export namespace ElanToolchains { + export function unresolvedToolchain(toolchains: ElanToolchains): ElanOption { + return toolchains.activeOverride?.unresolved ?? toolchains.default?.unresolved + } + + export function unresolvedToolchainName(toolchains: ElanToolchains): ElanOption { + const unresolvedToolchain = ElanToolchains.unresolvedToolchain(toolchains) + if (unresolvedToolchain === undefined) { + return undefined + } + return ElanUnresolvedToolchain.toolchainName(unresolvedToolchain) + } } export type ElanStateDump = { @@ -140,6 +162,13 @@ function zodElanUnresolvedToolchain() { ]) } +function zodElanToolchainResolution() { + return z.object({ + live: zodElanResult(z.string()), + cached: z.nullable(z.string()), + }) +} + function convertElanResult( zodResult: | { @@ -199,6 +228,29 @@ function convertElanUnresolvedToolchain( } } +function covertElanToolchainResolution( + installed: Map, + zodElanToolchainResolution: { + live: + | { + Ok: string + } + | { + Err: string + } + cached: string | null + }, +): ElanToolchainResolution { + let cachedToolchain = convertElanOption(zodElanToolchainResolution.cached, t => t) + if (cachedToolchain !== undefined && !installed.has(cachedToolchain)) { + cachedToolchain = undefined + } + return { + resolvedToolchain: convertElanResult(zodElanToolchainResolution.live, t => t), + cachedToolchain, + } +} + function convertElanOverrideReason( zodElanOverrideReason: | 'Environment' @@ -254,7 +306,7 @@ function parseElanStateDump(elanDumpStateOutput: string): ElanStateDump | undefi default: z.nullable( z.object({ unresolved: zodElanUnresolvedToolchain(), - resolved: zodElanResult(z.string()), + resolved: zodElanToolchainResolution(), }), ), active_override: z.nullable( @@ -269,7 +321,7 @@ function parseElanStateDump(elanDumpStateOutput: string): ElanStateDump | undefi ]), }), ), - resolved_active: z.nullable(zodElanResult(z.string())), + resolved_active: z.nullable(zodElanToolchainResolution()), }), }) const stateDumpResult = stateDumpSchema.safeParse(parsedJson) @@ -278,25 +330,29 @@ function parseElanStateDump(elanDumpStateOutput: string): ElanStateDump | undefi } const s = stateDumpResult.data + const installed = groupByUniqueKey( + s.toolchains.installed.map(i => ({ resolvedName: i.resolved_name, path: new FileUri(i.path) })), + i => i.resolvedName, + ) + const stateDump: ElanStateDump = { elanVersion: { current: new SemVer(s.elan_version.current), newest: convertElanResult(s.elan_version.newest, version => new SemVer(version)), }, toolchains: { - installed: groupByUniqueKey( - s.toolchains.installed.map(i => ({ resolvedName: i.resolved_name, path: new FileUri(i.path) })), - i => i.resolvedName, - ), + installed, default: convertElanOption(s.toolchains.default, d => ({ unresolved: convertElanUnresolvedToolchain(d.unresolved), - resolved: convertElanResult(d.resolved, r => r), + resolved: covertElanToolchainResolution(installed, d.resolved), })), activeOverride: convertElanOption(s.toolchains.active_override, r => ({ reason: convertElanOverrideReason(r.reason), unresolved: convertElanUnresolvedToolchain(r.unresolved), })), - resolvedActive: convertElanOption(s.toolchains.resolved_active, r => convertElanResult(r, a => a)), + resolvedActive: convertElanOption(s.toolchains.resolved_active, r => + covertElanToolchainResolution(installed, r), + ), }, } return stateDump @@ -444,50 +500,30 @@ export async function elanActiveToolchain( context: string | undefined, toolchain?: string | undefined, ): Promise { - const stateDumpWithoutNetResult = await elanDumpStateWithoutNet(cwdUri, toolchain) - if (stateDumpWithoutNetResult.kind !== 'Success') { - return stateDumpWithoutNetResult + const stateDumpResult = await elanDumpStateWithNet(cwdUri, context, toolchain) + if (stateDumpResult.kind !== 'Success') { + return stateDumpResult } - const cachedToolchainInfo = stateDumpWithoutNetResult.state.toolchains.resolvedActive - if (cachedToolchainInfo === undefined) { + const unresolvedToolchain = ElanToolchains.unresolvedToolchainName(stateDumpResult.state.toolchains) + if (unresolvedToolchain === 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 toolchainResolution = stateDumpResult.state.toolchains.resolvedActive + if (toolchainResolution === undefined) { + return { kind: 'NoActiveToolchain' } } - 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 cachedToolchain = toolchainResolution.cachedToolchain + const resolvedToolchainResult = toolchainResolution.resolvedToolchain - const resolvedToolchainInfo = stateDumpWithNetResult.state.toolchains.resolvedActive - if (resolvedToolchainInfo === undefined) { - return { kind: 'NoActiveToolchain' } - } - if (resolvedToolchainInfo.kind === 'Error') { - return { kind: 'ExecutionError', message: resolvedToolchainInfo.message } + if (resolvedToolchainResult.kind === 'Error') { + return { kind: 'ExecutionError', message: resolvedToolchainResult.message } } - const resolvedToolchain = resolvedToolchainInfo.value + const resolvedToolchain = resolvedToolchainResult.value - const overrideReason = overrideInfo?.reason + const overrideReason = stateDumpResult.state.toolchains.activeOverride?.reason const origin: ElanOverrideReason | { kind: 'Default' } = overrideReason !== undefined ? overrideReason : { kind: 'Default' } @@ -563,7 +599,7 @@ export async function elanSelfUninstall( channel: OutputChannel | undefined, context: string | undefined, ): Promise { - return await batchExecuteWithProgress('elan', ['self', 'uninstall'], context, 'Uninstalling Elan', { + return await batchExecuteWithProgress('elan', ['self', 'uninstall', '-y'], context, 'Uninstalling Elan', { channel, allowCancellation: true, }) diff --git a/vscode-lean4/src/utils/elanCommands.ts b/vscode-lean4/src/utils/elanCommands.ts index bef617e8..0fcb5d84 100644 --- a/vscode-lean4/src/utils/elanCommands.ts +++ b/vscode-lean4/src/utils/elanCommands.ts @@ -8,8 +8,10 @@ import { elanEagerResolutionMajorVersion, elanInstalledToolchains, elanInstallToolchain, + elanNightlyChannel, elanQueryGc, elanSetDefaultToolchain, + elanStableChannel, elanUninstallToolchains, elanVersion, isElanEagerResolutionVersion, @@ -58,10 +60,19 @@ export class ElanCommandProvider implements Disposable { 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?' + let prompt: string + if (selectedDefaultToolchain === elanStableChannel) { + prompt = + `This operation will set the '${selectedDefaultToolchain}' Lean release channel to be the global default Lean release channel.\n` + + 'This means that the most recent stable Lean version at any given time will be used for files in VS Code that do not belong to a Lean project, as well as for Lean commands on the command line outside of Lean projects.\n' + + 'When a new stable Lean version becomes available, VS Code will issue a prompt about whether to update to the most recent Lean version. On the command line, the new stable Lean version will be downloaded automatically without a prompt.\n\n' + + 'Do you wish to proceed?' + } else { + prompt = + `This operation will set '${selectedDefaultToolchain}' to be the global default Lean version.\n` + + 'This means that it will be used for files in VS Code that do not belong to a Lean project, as well as for Lean commands on the command line outside of Lean projects.\n\n' + + 'Do you wish to proceed?' + } const promptChoice = await displayNotificationWithInput('Information', prompt, ['Proceed']) if (promptChoice !== 'Proceed') { return @@ -95,11 +106,11 @@ export class ElanCommandProvider implements Disposable { const channels = [ { name: 'Stable', - identifier: 'leanprover/lean4:stable', + identifier: elanStableChannel, }, { name: 'Nightly', - identifier: 'leanprover/lean4:nightly', + identifier: elanNightlyChannel, }, ] @@ -201,9 +212,9 @@ export class ElanCommandProvider implements Disposable { if (toolchainInfo === undefined) { return } - const installedToolchains = toolchainInfo.toolchains.filter(t => t !== toolchainInfo.defaultToolchain) + const installedToolchains = toolchainInfo.toolchains if (installedToolchains.length === 0) { - displayNotification('Information', 'No non-default Lean version installed.') + displayNotification('Information', 'No Lean versions installed.') return } const installedToolchainItems = installedToolchains.map(t => { @@ -357,7 +368,6 @@ export class ElanCommandProvider implements Disposable { title: string, includeStable: boolean, ): Promise { - const stableChannel = 'leanprover/lean4:stable' const toolchainInfo = await this.installedToolchains() if (toolchainInfo === undefined) { return undefined @@ -389,7 +399,7 @@ export class ElanCommandProvider implements Disposable { const stableItem: QuickPickItem = { label: 'Always use most recent stable version', - description: stableChannel, + description: elanStableChannel, picked: true, } const installedToolchainSeparator: QuickPickItem = { label: '', kind: QuickPickItemKind.Separator } @@ -427,8 +437,8 @@ export class ElanCommandProvider implements Disposable { if (choice === undefined) { return undefined } - if (choice.description === stableChannel) { - return stableChannel + if (choice.description === elanStableChannel) { + return elanStableChannel } else { return choice.label } diff --git a/vscode-lean4/src/utils/leanCmdRunner.ts b/vscode-lean4/src/utils/leanCmdRunner.ts index 14bb7648..c1d530bb 100644 --- a/vscode-lean4/src/utils/leanCmdRunner.ts +++ b/vscode-lean4/src/utils/leanCmdRunner.ts @@ -11,6 +11,7 @@ import { ElanOverrideReason, ElanRemoteUnresolvedToolchain, ElanStateDump, + ElanToolchains, ElanUnresolvedToolchain, } from './elan' import { FileUri } from './exturi' @@ -59,7 +60,7 @@ function leanNotInstalledError( let toolchainName: string if (unresolvedActiveToolchain.fromChannel !== undefined) { const prefix = activeOverride === undefined ? 'default ' : '' - toolchainName = `Lean version for ${prefix}release channel '${unresolvedActiveToolchain.fromChannel}'` + toolchainName = `Lean version for ${prefix}release channel '${ElanUnresolvedToolchain.toolchainName(unresolvedActiveToolchain)}'` } else { const prefix = activeOverride === undefined ? 'Default ' : '' toolchainName = `${prefix}Lean version '${ElanUnresolvedToolchain.toolchainName(unresolvedActiveToolchain)}'` @@ -130,10 +131,9 @@ export class LeanCommandRunner { return runWithActiveToolchain } - const unresolvedToolchain = - elanState.toolchains.activeOverride?.unresolved ?? elanState.toolchains.default?.unresolved - const resolvedToolchainResult = elanState.toolchains.resolvedActive - if (unresolvedToolchain === undefined || resolvedToolchainResult === undefined) { + const unresolvedToolchain = ElanToolchains.unresolvedToolchain(elanState.toolchains) + const toolchainResolutionResult = elanState.toolchains.resolvedActive + if (unresolvedToolchain === undefined || toolchainResolutionResult === undefined) { return runWithActiveToolchain } @@ -141,20 +141,7 @@ export class LeanCommandRunner { 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 - } - + const cachedToolchain = toolchainResolutionResult.cachedToolchain if (cachedToolchain === undefined) { const installNewToolchain: () => Promise< { kind: 'RunWithActiveToolchain' } | { kind: 'Error'; message: string } @@ -250,10 +237,9 @@ export class LeanCommandRunner { ) } - const unresolvedToolchain = - elanState.toolchains.activeOverride?.unresolved ?? elanState.toolchains.default?.unresolved - const resolvedToolchainResult = elanState.toolchains.resolvedActive - if (unresolvedToolchain === undefined || resolvedToolchainResult === undefined) { + const unresolvedToolchain = ElanToolchains.unresolvedToolchain(elanState.toolchains) + const toolchainResolutionResult = elanState.toolchains.resolvedActive + if (unresolvedToolchain === undefined || toolchainResolutionResult === undefined) { return runWithActiveToolchain } @@ -261,6 +247,7 @@ export class LeanCommandRunner { return runWithActiveToolchain } + const resolvedToolchainResult = toolchainResolutionResult.resolvedToolchain let resolvedToolchain: string switch (resolvedToolchainResult.kind) { case 'Error': @@ -312,7 +299,7 @@ export class LeanCommandRunner { 'Information', updatePrompt( elanState.toolchains.activeOverride?.reason, - unresolvedToolchain.fromChannel, + ElanUnresolvedToolchain.toolchainName(unresolvedToolchain), cachedToolchain, resolvedToolchain, ),