Zulip Chat Archive

Stream: new members

Topic: Problems with downloading

Damir Gabitov (Oct 03 2022 at 07:18):

Hello. I 've installed GitBash for Windows 7 (32bit) and try to install Lean. So, I copy the command in GitBash: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
But there is a message:
info: downloading installer
curl: (22) The requested URL returned error: 404
elan: command failed: curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-i686-pc-windows-msvc.zip -o /tmp/tmp.TAqC0zj5as/elan-init.zip
I thougth, that maybe I have problems with connecton to Interne, but other web-sites work well

Damir Gabitov (Oct 03 2022 at 10:40):

Finally, I've understood what happens: The command curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
download some shell that next will download https://github.com/leanprover/elan/releases/download/v1.4.2/elan-i686-pc-windows-msvc.zip
and /tmp/tmp.TAqC0zj5as/elan-init.zip. This shell like .bat file in Windows that contain commands for downloading these two files, if I undersand correct. But, I couldn't download elan-i686-pc-windows-msvc.zip file with options for curl -sSfL, but when I used culr -O <url> I've downloaded that file. So, problem now is that I don't know URL for /tmp/tmp.TAqC0zj5as/elan-init.zip. And hwo then install Leand, using that .zip files?

Damir Gabitov (Oct 03 2022 at 10:41):

*how install

Last updated: Dec 20 2023 at 11:08 UTC