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