Zulip Chat Archive

Stream: lean4

Topic: elan#119 doc: fix installation instructions for Windows


Bulhwi Cha (Jan 31 2024 at 10:30):

elan's README.md says,

Windows: run the following commands in a terminal:

curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1
powershell -ExecutionPolicy Bypass -f elan-init.ps1
del elan-init.ps1

@Sebastian Ullrich When I run the first command in Command Prompt, it creates a file named elan-init.ps1. But when I do the same in Windows PowerShell, the name of the created file is --location.

Sebastian Ullrich (Jan 31 2024 at 10:37):

@Bulhwi Cha Thanks for the clarification, that is extremely puzzling. What happens if you use curl.exe in Powershell?

Bulhwi Cha (Jan 31 2024 at 10:46):

PS C:\Users\chabulhwi> & "C:\Windows\System32\curl.exe" -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
100  2365  100  2365    0     0  46554      0 --:--:-- --:--:-- --:--:-- 48265
PS C:\Users\chabulhwi> ls elan-init.ps1


    Directory: C:\Users\chabulhwi


Mode                 LastWriteTime         Length Name
----                 -------------         ------ ----
-a----         1/31/2024   7:45 PM           2365 elan-init.ps1

Bulhwi Cha (Jan 31 2024 at 10:47):

A file named elan-init.ps1 is created.

Bulhwi Cha (Jan 31 2024 at 11:33):

PowerShell 7.4.1 works fine; the culprit turned out to be PowerShell 5.1. But there's another problem: the former doesn't replace the latter even after you installed the newer version.

Bulhwi Cha (Jan 31 2024 at 12:09):

Shall I open a pull request that makes the following change? Edit: the new PR is elan#120.

-**Windows**: run the following commands in a terminal:
+**Windows**: run the following commands in a terminal (Command Prompt or PowerShell 7.4.1 or later):

Sebastian Ullrich (Jan 31 2024 at 12:51):

Yes, please go ahead


Last updated: May 02 2025 at 03:31 UTC