Download from `lean-lang.org` slow

Stream: general

[Wrenna Robson]

Hi, I am doing a tooling update and currently I am getting a download speed of around 50 KiB/s from lean-lang.org, on a 1Gbps connection. This seems... off.

[Wrenna Robson]

Also seems to happen from my browser when trying to download https://releases.lean-lang.org/lean4/v4.24.0/lean-4.24.0-linux.tar.zst so it would at the very least seem to be not confined to the command line tool. I would be grateful to know if it's just me or not.

[Wrenna Robson]

Though weirdly wget appears to be fine... I am not sure what's going on there.

[Sebastian Ullrich]

Note that these are just redirects to GitHub releases, so the title is misleading. It is of course still important to us to know when users have problems there.

[Wrenna Robson]

Ah yes, I see that from the wget output. But yeah - absolutely zero idea why wget should be fine but lake and my browser would be painfully slow.

[Sebastian Ullrich]

Elan uses libcurl though I don't know either if or how that could make a difference

[Wrenna Robson]

Oh now wget is slow!

[Wrenna Robson]

Going to try restarting my machine in case it's something stupid locally.

[Sebastian Ullrich]

If only restarting the internet were an option sometimes :)

[Wrenna Robson]

That appears to have exorcised the ghosts. I shall assume it was just a me problem unless anyone else experiences it.

[Wrenna Robson]

Having this problem again today.

[Kevin Buzzard]

Could it be the Cloudflare outage?

[Wrenna Robson]

No, it fixed on a restart again. So it's clearly something local to a degree, but I've no idea why it happens sometimes.

[Antoine Chambert-Loir]

now, github is down…

[Kevin Buzzard]

(looks like it's back now)

[Christian Krause]

I am experiencing the same issue:

[🧱] × lake --version
info: downloading https://releases.lean-lang.org/lean4/v4.25.1/lean-4.25.0-linux.tar.zst
  2.3 MiB / 473.8 MiB (  0 %)  60.8 KiB/s ETA: 132 min 22 s

I have a 1gig connection, speedtest.net shows 500mbit.
(I am located in germany, maybe this is important)

[Christian Krause]

Downloading the release in firefox directly on the github repo is also very slow, so this is clearly not a lake issue.

[Christian Krause]

This is very weird: Before posting this, i also tried lake --version on my pc to see if this is an issue with my laptop and it was also very slow. I tried it a bunch of times (sometimes for several minutes) and was always slow. Then, on the last run, it just worked with normal download speeds (On my laptop).
I immediately tried it again on my pc and it also magically fixed itself there without me doing anything.

[Wrenna Robson]

Yeah I find restarting generally fixes it for me. But it's still very annoying

[Christian Krause]

Do you mean restarting the command or the device? Because I did not restart the computers... (And i had to restart the command on the laptop like 5 times before it worked :laughing: )

[Wrenna Robson]

The device! But you may be having a different issue with the same symptom of course (or conversely it is the same underlying cause but with different incidental causes).

[Christian Krause]

My issue does not seem to be local to my device, because it is slow again on my pc and my laptop (and i changed nothing). Maybe the network over at github is somewhat instable....

[Wrenna Robson]

They may also be the case!

[Christian Krause]

It's getting even funnier: I just left the command running at about 100 kib/s on my pc and after a minute or so, it just went up to 10 mib/s. (I immediately tried it on my laptop and it was also fast again). I think we will just have to wait unti they move the server at github a bit closer to the wifi.