diff --git a/vscode-lean4/src/globalDiagnostics.ts b/vscode-lean4/src/globalDiagnostics.ts index afc280b37..5eb840878 100644 --- a/vscode-lean4/src/globalDiagnostics.ts +++ b/vscode-lean4/src/globalDiagnostics.ts @@ -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( diff --git a/vscode-lean4/src/projectinit.ts b/vscode-lean4/src/projectinit.ts index 6c6ffd562..ef5ee2dcf 100644 --- a/vscode-lean4/src/projectinit.ts +++ b/vscode-lean4/src/projectinit.ts @@ -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' @@ -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,