Zulip Chat Archive
Stream: new members
Topic: I can't install lean's version manager Elan
David Leroie (Mar 26 2025 at 15:21):
I can't install lean's version manager Elan on Visual Studio Code
I am currently following the Lean 4 Setup guide
I am in the install lean version manager section and when I click on "click to install" I get error messages
PS C:\Users\admin\math2001> Start-BitsTransfer -Source "https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1" -Destination "elan-init.ps1"
PS C:\Users\admin\math2001> Set-ExecutionPolicy -ExecutionPolicy Unrestricted -Scope Process
PS C:\Users\admin\math2001> $rc = .\elan-init.ps1 -NoPrompt 1 -DefaultToolchain leanprover/lean4:stable
info: downloading installer to C:\Users\admin\AppData\Local\Temp\
Download failed for https://github.com/leanprover/elan/releases/latest/download/elan-x86_64-pc-windows-msvc.zip
La demande a été abandonnée : Impossible de créer un canal sécurisé SSL/TLS.
PS C:\Users\admin\math2001> Write-Host "elan-init returned [$rc]"
elan-init returned [1]
PS C:\Users\admin\math2001> del .\elan-init.ps1
PS C:\Users\admin\math2001> if ($rc -ne 0) {
Read-Host -Prompt "Press ENTER to continue"
}
exit
Henrik Böving (Mar 26 2025 at 15:36):
Do you have an anti virus software apart from Windows Defender that might interfere here?
David Leroie (Mar 27 2025 at 08:21):
@Henrik Böving I don't have any other antivirus besides Windows Defender. I checked the Action Center. I'm using Windows 8.1.
I tried disabling Windows Defender, but the problem persists.
Sebastian Ullrich (Mar 27 2025 at 08:44):
That doesn't(?) explain the elan error but you are using an unsupported Windows version https://lean-lang.org/lean4/doc/setup.html#supported-platforms
Last updated: May 02 2025 at 03:31 UTC