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