Skip to content

Commit 6201cab

Browse files
mhuisimhuisi
committed
wip
1 parent eedf3aa commit 6201cab

File tree

5 files changed

+73
-75
lines changed

5 files changed

+73
-75
lines changed

‎vscode-lean4/src/diagnostics/setupDiagnoser.ts

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ import {
77
ElanDumpStateWithoutNetResult,
88
elanDumpStateWithNet,
99
elanDumpStateWithoutNet,
10-
isElanDumpStateVersion,
10+
isElanEagerResolutionVersion,
1111
} from '../utils/elan'
1212
import { FileUri } from '../utils/exturi'
1313
import { ToolchainUpdateMode, leanRunner } from '../utils/leanCmdRunner'
@@ -245,7 +245,7 @@ export class SetupDiagnoser {
245245
const dumpStateResult = await elanDumpStateWithoutNet(this.cwdUri, this.toolchain)
246246
if (dumpStateResult.kind === 'ExecutionError') {
247247
const versionResult = await this.queryElanVersion()
248-
if (versionResult.kind === 'Success' && !isElanDumpStateVersion(versionResult.version)) {
248+
if (versionResult.kind === 'Success' && !isElanEagerResolutionVersion(versionResult.version)) {
249249
return { kind: 'PreEagerResolutionVersion' }
250250
}
251251
}
@@ -256,7 +256,7 @@ export class SetupDiagnoser {
256256
const dumpStateResult = await elanDumpStateWithNet(this.cwdUri, this.toolchain)
257257
if (dumpStateResult.kind === 'ExecutionError') {
258258
const versionResult = await this.queryElanVersion()
259-
if (versionResult.kind === 'Success' && !isElanDumpStateVersion(versionResult.version)) {
259+
if (versionResult.kind === 'Success' && !isElanEagerResolutionVersion(versionResult.version)) {
260260
return { kind: 'PreEagerResolutionVersion' }
261261
}
262262
}

‎vscode-lean4/src/utils/elan.ts

Lines changed: 39 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,12 @@ import { batchExecute, batchExecuteWithProgress, ExecutionExitCode, ExecutionRes
55
import { FileUri } from './exturi'
66
import { groupByUniqueKey } from './groupBy'
77

8+
export const elanEagerResolutionMajorVersion = 3 // TODO: for debugging purposes. Change to 4 before merge
9+
10+
export function isElanEagerResolutionVersion(version: SemVer) {
11+
return version.major >= elanEagerResolutionMajorVersion
12+
}
13+
814
// Suggested at https://semver.org/#is-there-a-suggested-regular-expression-regex-to-check-a-semver-string
915

1016
const semVerRegex =
@@ -147,10 +153,10 @@ function convertElanResult<T, V>(
147153
if ('Ok' in zodResult) {
148154
return { kind: 'Ok', value: f(zodResult.Ok) }
149155
}
150-
if ('Err' in zodResult) {
151-
return { kind: 'Error', message: zodResult.Err }
156+
zodResult satisfies {
157+
Err: string
152158
}
153-
return zodResult
159+
return { kind: 'Error', message: zodResult.Err }
154160
}
155161

156162
function convertElanOption<T, V>(zodNullable: T | null, f: (v: T) => V): ElanOption<V> {
@@ -178,15 +184,19 @@ function convertElanUnresolvedToolchain(
178184
if ('Local' in zodElanUnresolvedToolchain) {
179185
return { kind: 'Local', toolchain: zodElanUnresolvedToolchain.Local.name }
180186
}
181-
if ('Remote' in zodElanUnresolvedToolchain) {
182-
return {
183-
kind: 'Remote',
184-
githubRepoOrigin: zodElanUnresolvedToolchain.Remote.origin,
185-
release: zodElanUnresolvedToolchain.Remote.release,
186-
fromChannel: convertElanOption(zodElanUnresolvedToolchain.Remote.from_channel, c => c),
187+
zodElanUnresolvedToolchain satisfies {
188+
Remote: {
189+
origin: string
190+
release: string
191+
from_channel: string | null
187192
}
188193
}
189-
return zodElanUnresolvedToolchain
194+
return {
195+
kind: 'Remote',
196+
githubRepoOrigin: zodElanUnresolvedToolchain.Remote.origin,
197+
release: zodElanUnresolvedToolchain.Remote.release,
198+
fromChannel: convertElanOption(zodElanUnresolvedToolchain.Remote.from_channel, c => c),
199+
}
190200
}
191201

192202
function convertElanOverrideReason(
@@ -217,10 +227,8 @@ function convertElanOverrideReason(
217227
if ('LeanpkgFile' in zodElanOverrideReason) {
218228
return { kind: 'LeanpkgFile', leanpkgPath: new FileUri(zodElanOverrideReason.LeanpkgFile) }
219229
}
220-
if ('InToolchainDirectory' in zodElanOverrideReason) {
221-
return { kind: 'ToolchainDirectory', directoryPath: new FileUri(zodElanOverrideReason.InToolchainDirectory) }
222-
}
223-
return zodElanOverrideReason
230+
zodElanOverrideReason satisfies { InToolchainDirectory: string }
231+
return { kind: 'ToolchainDirectory', directoryPath: new FileUri(zodElanOverrideReason.InToolchainDirectory) }
224232
}
225233

226234
function parseElanStateDump(elanDumpStateOutput: string): ElanStateDump | undefined {
@@ -363,18 +371,6 @@ export async function elanDumpStateWithNet(
363371
}
364372
}
365373

366-
export function isElanEagerToolchainResolutionVersion(elanVersion: SemVer): boolean {
367-
return elanVersion.major >= 3
368-
}
369-
370-
export function isElanDumpStateVersion(elanVersion: SemVer): boolean {
371-
return elanVersion.major >= 3
372-
}
373-
374-
export function isElanGcVersion(elanVersion: SemVer): boolean {
375-
return elanVersion.major >= 3
376-
}
377-
378374
export type ElanInstalledToolchainsResult =
379375
| { kind: 'Success'; toolchains: string[]; defaultToolchain: string | undefined }
380376
| { kind: 'ElanNotFound' }
@@ -573,15 +569,26 @@ export async function elanSelfUninstall(
573569
})
574570
}
575571

572+
export type ElanSetDefaultToolchainResult =
573+
| { kind: 'Success' }
574+
| { kind: 'ElanNotFound' }
575+
| { kind: 'Error'; message: string }
576+
576577
export async function elanSetDefaultToolchain(
577578
channel: OutputChannel | undefined,
578-
context: string | undefined,
579579
toolchain: string,
580-
) {
581-
return await batchExecuteWithProgress('elan', ['default', toolchain], context, 'Setting default Lean version', {
582-
channel,
583-
allowCancellation: true,
584-
})
580+
): Promise<ElanSetDefaultToolchainResult> {
581+
const r = await batchExecute('elan', ['default', toolchain], undefined, { combined: channel })
582+
switch (r.exitCode) {
583+
case ExecutionExitCode.Success:
584+
return { kind: 'Success' }
585+
case ExecutionExitCode.CannotLaunch:
586+
return { kind: 'ElanNotFound' }
587+
case ExecutionExitCode.ExecutionError:
588+
return { kind: 'Error', message: r.combined }
589+
case ExecutionExitCode.Cancelled:
590+
throw new Error('Unexpected cancellation of `elan default <toolchain>`')
591+
}
585592
}
586593

587594
export type ElanUsedToolchain = {

‎vscode-lean4/src/utils/elanCommands.ts

Lines changed: 20 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -5,13 +5,14 @@ import { LeanClientProvider } from './clientProvider'
55
import {
66
ActiveToolchainInfo,
77
elanActiveToolchain,
8+
elanEagerResolutionMajorVersion,
89
elanInstalledToolchains,
910
elanInstallToolchain,
1011
elanQueryGc,
1112
elanSetDefaultToolchain,
1213
elanUninstallToolchains,
1314
elanVersion,
14-
isElanDumpStateVersion,
15+
isElanEagerResolutionVersion,
1516
toolchainVersion,
1617
} from './elan'
1718
import { FileUri, UntitledUri } from './exturi'
@@ -66,31 +67,21 @@ export class ElanCommandProvider implements Disposable {
6667
return
6768
}
6869

69-
const setDefaultToolchainResult = await elanSetDefaultToolchain(
70-
this.channel,
71-
selectDefaultToolchainContext,
72-
selectedDefaultToolchain,
73-
)
74-
switch (setDefaultToolchainResult.exitCode) {
75-
case ExecutionExitCode.Success:
70+
const setDefaultToolchainResult = await elanSetDefaultToolchain(this.channel, selectedDefaultToolchain)
71+
switch (setDefaultToolchainResult.kind) {
72+
case 'Success':
7673
displayNotification(
7774
'Information',
7875
`Default Lean version '${selectedDefaultToolchain}' set successfully.`,
7976
)
8077
const clientForUntitledFiles = this.clientProvider?.findClient(new UntitledUri())
8178
await clientForUntitledFiles?.restart()
8279
break
83-
case ExecutionExitCode.CannotLaunch:
80+
case 'ElanNotFound':
8481
displayNotification('Error', 'Cannot set Lean default version: Elan is not installed.')
8582
break
86-
case ExecutionExitCode.ExecutionError:
87-
displayNotification('Error', `Cannot set Lean default version: ${setDefaultToolchainResult.combined}`)
88-
break
89-
case ExecutionExitCode.Cancelled:
90-
displayNotification(
91-
'Information',
92-
'Default Lean version selection cancelled. Default Lean version has not been set.',
93-
)
83+
case 'Error':
84+
displayNotification('Error', `Cannot set Lean default version: ${setDefaultToolchainResult.message}`)
9485
break
9586
}
9687
}
@@ -330,11 +321,12 @@ export class ElanCommandProvider implements Disposable {
330321
}
331322

332323
const prompt =
333-
`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` +
334-
'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' +
335-
"Additionally, if your project has a 'lakefile.lean' or a 'lakefile.toml', the project configuration may be incompatible with the new version.\n" +
336-
'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. ' +
337-
"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" +
324+
`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` +
325+
'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' +
326+
'- The Lean code in this project\n' +
327+
"- The 'lakefile.toml' or 'lakefile.lean' configuring this project\n" +
328+
'- Lake dependencies of this project\n\n' +
329+
"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" +
338330
'Do you wish to proceed?'
339331
const choice = await displayNotificationWithInput('Information', prompt, ['Proceed'])
340332
if (choice !== 'Proceed') {
@@ -383,6 +375,9 @@ export class ElanCommandProvider implements Disposable {
383375
"Could not fetch Lean versions: Cannot parse response from 'https://release.lean-lang.org/'.",
384376
)
385377
}
378+
if (leanReleasesQueryResult.kind === 'CannotFetch') {
379+
displayNotification('Warning', `Could not fetch Lean versions: ${leanReleasesQueryResult.error}`)
380+
}
386381
const toToolchainNames = (channel: LeanReleaseChannel) =>
387382
channel.map(t => `leanprover/lean4:${t.name}`).filter(t => !installedToolchainIndex.has(t))
388383
if (leanReleasesQueryResult.kind === 'Success') {
@@ -466,6 +461,7 @@ export class ElanCommandProvider implements Disposable {
466461
}
467462
return undefined
468463
}
464+
r.kind satisfies 'Success'
469465
return r.info
470466
}
471467

@@ -492,10 +488,10 @@ export class ElanCommandProvider implements Disposable {
492488
const r = await elanVersion()
493489
switch (r.kind) {
494490
case 'Success':
495-
if (!isElanDumpStateVersion(r.version)) {
491+
if (!isElanEagerResolutionVersion(r.version)) {
496492
displayNotification(
497493
'Error',
498-
`This command can only be used with Elan versions >= 4.0.0, but the installed Elan version is ${r.version.toString()}.`,
494+
`This command can only be used with Elan versions >= ${elanEagerResolutionMajorVersion}.0.0, but the installed Elan version is ${r.version.toString()}.`,
499495
)
500496
return false
501497
}

‎vscode-lean4/src/utils/leanCmdRunner.ts

Lines changed: 8 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -203,10 +203,9 @@ export class LeanCommandRunner {
203203
message: leanNotInstalledError(elanState.toolchains.activeOverride?.reason, unresolvedToolchain),
204204
}
205205
}
206-
if (choice === 'Install Version') {
207-
return await installNewToolchain()
208-
}
209-
return choice
206+
choice satisfies 'Install Version'
207+
208+
return await installNewToolchain()
210209
}
211210

212211
if (unresolvedToolchain.fromChannel === undefined) {
@@ -323,10 +322,8 @@ export class LeanCommandRunner {
323322
if (choice === undefined || choice === 'Use Old Version') {
324323
return runWithCachedToolchain(undefined)
325324
}
326-
if (choice === 'Update Lean Version') {
327-
return await updateToolchain()
328-
}
329-
return choice
325+
choice satisfies 'Update Lean Version'
326+
return await updateToolchain()
330327
}
331328

332329
async decideToolchain(
@@ -370,7 +367,7 @@ export class LeanCommandRunner {
370367
)
371368
if (withNetAnalysisResult.kind === 'RunWithCachedToolchain') {
372369
this.stickyUpdateDecisions.set(key, 'DoNotUpdate')
373-
if (withNetAnalysisResult.warning) {
370+
if (withNetAnalysisResult.warning !== undefined) {
374371
displayNotification('Warning', withNetAnalysisResult.warning)
375372
}
376373
return { kind: 'RunWithSpecificToolchain', toolchain: cachedToolchain }
@@ -395,10 +392,8 @@ export class LeanCommandRunner {
395392
if (toolchainDecision.kind === 'RunWithActiveToolchain') {
396393
return await this.runCmd(executablePath, args, options, undefined)
397394
}
398-
if (toolchainDecision.kind === 'RunWithSpecificToolchain') {
399-
return await this.runCmd(executablePath, args, options, toolchainDecision.toolchain)
400-
}
401-
return toolchainDecision
395+
toolchainDecision.kind satisfies 'RunWithSpecificToolchain'
396+
return await this.runCmd(executablePath, args, options, toolchainDecision.toolchain)
402397
}
403398
}
404399

‎vscode-lean4/src/utils/leanInstaller.ts

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ import { SemVer } from 'semver'
22
import { Disposable, EventEmitter, OutputChannel, TerminalOptions, window } from 'vscode'
33
import { getPowerShellPath, isRunningTest, setAlwaysAskBeforeInstallingLeanVersions } from '../config'
44
import { ExecutionExitCode, displayResultError } from './batch'
5-
import { elanSelfUninstall, elanSelfUpdate, elanVersion, isElanEagerToolchainResolutionVersion } from './elan'
5+
import { elanSelfUninstall, elanSelfUpdate, elanVersion, isElanEagerResolutionVersion } from './elan'
66
import { FileUri } from './exturi'
77
import { logger } from './logger'
88
import {
@@ -173,7 +173,7 @@ export class LeanInstaller {
173173
}
174174

175175
private async displayElanUpdateSuccessfulPrompt(currentVersion: SemVer) {
176-
if (!isElanEagerToolchainResolutionVersion(currentVersion)) {
176+
if (isElanEagerResolutionVersion(currentVersion)) {
177177
displayNotification('Information', 'Elan update successful!')
178178
return
179179
}
@@ -385,7 +385,7 @@ export class LeanInstaller {
385385

386386
async uninstallElan() {
387387
const prompt =
388-
"This command will uninstall Lean's version manager Elan and all installed Lean version.\n" +
388+
"This command will uninstall Lean's version manager Elan and all installed Lean versions.\n" +
389389
'Do you wish to proceed?'
390390
const choice = await displayNotificationWithInput('Information', prompt, ['Proceed'])
391391
if (choice !== 'Proceed') {

0 commit comments

Comments
 (0)