Zulip Chat Archive
Stream: lean4
Topic: Installing ELAN on windows resulting in error
Xwtek (Jan 20 2024 at 06:48):
This is my first time on lean4, so sorry if I placed this on the wrong stream.
I tried to install lean as the lean4 extension's setup documentation described. At the ELAN installation setup, I tried to click the given button, but it returned an error:
info: downloading installer to C:\Users\Xwtek\AppData\Local\Temp\ error: could not create link from 'C:\Users\Xwtek\.elan\bin\elan.exe' to 'C:\Users\Xwtek\.elan\bin\lake.exe'
Elan failed with error code 1
PS E:\Projects\lean\mathematics_in_lean> Write-Host "elan-init returned [$rc]"
elan-init returned [1]
PS E:\Projects\lean\mathematics_in_lean> del .\elan-init.ps1
PS E:\Projects\lean\mathematics_in_lean> if ($rc -ne 0) {
>> Read-Host -Prompt "Press ENTER to continue"
>> }
Anyone knows how to resolve this, or is there any other information I need to supply?
Last updated: May 02 2025 at 03:31 UTC