Zulip Chat Archive

Stream: new members

Topic: can't install from git bash

Alex (Jan 06 2022 at 04:49):

Hello everyone! I'm trying to install lean+mathlib, and getting the following error in the console:

$ ./elan-init.sh
info: downloading installer
curl: (22) The requested URL returned error: 404
elan: command failed: curl -sSfL https://github.com/leanprover/elan/releases/download/v1.3.1/elan-i686-pc-windows-msvc.zip -o /tmp/tmp.kLJZMIuV9l/elan-init.zip

Mario Carneiro (Jan 06 2022 at 04:51):

It's true that elan-i686-pc-windows-msvc.zip does not exist: see https://github.com/leanprover/elan/releases/

Mario Carneiro (Jan 06 2022 at 04:52):

not sure why it is getting i686 as the architecture instead of x86_64

Mario Carneiro (Jan 06 2022 at 04:52):

maybe this means you are on a 32 bit machine?

Alex (Jan 06 2022 at 04:56):

64-bit machine, win7

Alex (Jan 06 2022 at 04:56):

latest available git

Alex (Jan 06 2022 at 04:56):

I've manually replaced the corresponding switch in elan-init.sh

Alex (Jan 06 2022 at 04:57):

moving forward it seems :)

Alex (Jan 06 2022 at 04:57):

still it is a problem if the script fails to detect the platform

Last updated: Dec 20 2023 at 11:08 UTC