Skip to content

Commit

Permalink
fix: special update handling for elan 3.1.0 (#448)
Browse files Browse the repository at this point in the history
Since `elan self update` was broken in Elan 3.1.0, we can't actually
update `elan` that way. Instead, we now re-run the installation script
for this version.

Also removes the `elan self update` call when attempting to create a
project.
  • Loading branch information
mhuisi authored May 21, 2024
1 parent 3f67fd6 commit 75f511f
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 4 deletions.
5 changes: 5 additions & 0 deletions vscode-lean4/src/globalDiagnostics.ts
Original file line number Diff line number Diff line change
Expand Up @@ -115,6 +115,11 @@ class GlobalDiagnosticsProvider {
if (updateElanChoice === undefined) {
return false
}
if (elanDiagnosis.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.installer.installElan()
return installElanResult !== 'InstallationFailed'
}
const elanSelfUpdateResult = await elanSelfUpdate(this.channel)
if (elanSelfUpdateResult.exitCode !== ExecutionExitCode.Success) {
displayResultError(
Expand Down
4 changes: 0 additions & 4 deletions vscode-lean4/src/projectinit.ts
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@ import {
ExecutionExitCode,
ExecutionResult,
} from './utils/batch'
import { elanSelfUpdate } from './utils/elan'
import { FileUri } from './utils/exturi'
import { lake } from './utils/lake'
import { displayError, displayInformationWithInput } from './utils/notifs'
Expand Down Expand Up @@ -107,9 +106,6 @@ export class ProjectInitializationProvider implements Disposable {
return 'DidNotComplete'
}

// This can fail silently in setups without Elan.
await elanSelfUpdate(this.channel)

const projectName: string = path.basename(projectFolder.fsPath)
const result: ExecutionResult = await lake(this.channel, projectFolder, toolchain).initProject(
projectName,
Expand Down

0 comments on commit 75f511f

Please sign in to comment.