Can't Download Any Lean Release , Slow Internet

Stream: lean4

[Jad Abou Hawili]

Gave up on having elan toolchain install or lake build in an existing project download a new toolchain.(or lake exe cache get etc..)
https://github.com/leanprover-community/mathlib4/issues/29015

Forgot about it for a while then i tried today going to lean 4 releases on github and just downloading from the browser, tried on different devices and networks to no avail, tried several versions like 4.21.0 , 4.23.0 to no avail.

browser says something along the lines of network error , contact server administrator , can't read source file

[Jad Abou Hawili]

Interesting Observation:
The error mentioned in the above github issue happens after the download reaches 200-240 megabytes and I have tested this multiple times.
I tried and was able to download the v4.9.0 release which is under 200 megabytes.

[Jad Abou Hawili]

I was able to download the v4.23.0 release by:

aria2c -x 16 https://releases.lean-lang.org/lean4/v4.23.0/lean-4.23.0-linux.tar.zst

I tried to place this in an appropriate .elan/toolchain folder and doing lake update in my project that has mathlib as a dependency, but it fails with errors related to cache. im guessing there is a build step , how would i do this manually because lake update fails preventing these subsequent steps
edit: placing in .elan/toolchain and doing lake update would work

[Jad Abou Hawili]

This github discussion discusses this , and possible workarounds when using curl. Im assuming lake uses curl so this should be relevant.

[Jad Abou Hawili]

tldr: if your internet is too slow , then jwt would expire because of the way github configured that. downloading using the aria2c command , or downloading chunks of the file using curl etc... would work and then placing in ~/.elan/toolchain. closing... although it would be desirable if lake's usage of curl accounts for this(if possible)

[Notification Bot]

This topic was moved here from #lean4 > Can't Download Any Lean Release by Jad Abou Hawili.