Zulip Chat Archive

Stream: new members

Topic: Error installing elan


view this post on Zulip Natalie S (Apr 01 2021 at 20:29):

Hi! Sorry very basic question - I was following the instructions to install lean on Windows (https://leanprover-community.github.io/install/windows.html) and got stuck at the first curl command, the github link seems to be down? Thanks

$ curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh
info: downloading installer
curl: (22) The requested URL returned error: 404
elan: command failed: curl -sSfL https://github.com/Kha/elan/releases/download/v0.11.0/elan-i686-pc-windows-msvc.zip -o /tmp/tmp.priBLupaHi/elan-init.zip

view this post on Zulip Patrick Massot (Apr 01 2021 at 20:31):

@Sebastian Ullrich

view this post on Zulip Kevin Buzzard (Apr 01 2021 at 20:32):

wget https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh is working for me right now -- maybe just try again?

view this post on Zulip Kevin Buzzard (Apr 01 2021 at 20:32):

no sorry, you're right: wget https://github.com/Kha/elan/releases/download/v0.11.0/elan-i686-pc-windows-msvc.zip is failing.

view this post on Zulip Sebastian Ullrich (Apr 01 2021 at 20:34):

32-bit Windows is not supported, neither by elan nor Lean (official releases)

view this post on Zulip Natalie S (Apr 01 2021 at 21:34):

Thanks for the help - realised the default git install is 32 bit and I didn't check :face_palm:, installing the 64 bit version solved it (was on 64 bit Windows).


Last updated: May 08 2021 at 02:46 UTC