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