leanprover / elan

The Lean version manager
Apache License 2.0
292 stars 34 forks source link

powershell installation fails on Windows ARM, but succeeds via git bash #108

Open semorrison opened 11 months ago

semorrison commented 11 months ago

On Windows 11, running inside Parallels on Apple Silicon (perhaps an unusual combination):

Running

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

in a Windows cmd terminal results in:

C:\Users\kim>curl -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  2522  100  2522    0     0   5745      0 --:--:-- --:--:-- --:--:--  5771

C:\Users\kim>powershell -ExecutionPolicy Bypass -f elan-init.ps1
### Elan install only supports 64-bit Windows with AMD64 architecture
1

C:\Users\kim>del elan-init.ps1

However in a git bash terminal

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

gives me a working lean/lake with no issues.

Kha commented 11 months ago

If we can just delete this, great! I don't think we need to worry about 32-bit systems anymore, but if we want to be sure...

semorrison commented 11 months ago

At least on my window-inside-parallels-on-M2 system, deleting those lines works great, and the standard install instructions succeed!