Increase lake exe cache get timeout

Stream: lean4

[Jafar Tanoukhi]

Is there a way to increase the timeout duration of lake exe cache get. I have quite a slow internet connection and I don't mind waiting for it an hour or so just to download, but it seems that it disconnects after some minutes of time even if the internet connection is stable.

[Bryan Gin-ge Chen]

Cache does all of its requests using curl so we could in principle let users increase the timeout by setting curl options, but I don't think we have a way to do that yet. Do you have an example log of lake exe cache get disconnecting?

[Jafar Tanoukhi]

I can start it up and wait a couple minutes for it to fail and show you the message but it's something to do with "Transfered partial file, n bytes remaining" .
Which to me looks almost certainly a timeout and nothing to do with an unstable internet.

[Jafar Tanoukhi]

Bryan Gin-ge Chen said:

let users increase the timeout by setting curl options, but I don't think we have a way to do that yet.

Also if that's the case, it sounds like a simple PR? Not sure if lake is open for PRs but maybe i can give that a go?

[Mac Malone]

As far as I am aware, curl has no default timeout for downlaods [c.f. StackExchange) and cache does not set one, so it is a bit confusing what would be timing it out.

[Bryan Gin-ge Chen]

If you want to give it a shot, here's where Cache is: https://github.com/leanprover-community/mathlib4/tree/master/Cache

[Bryan Gin-ge Chen]

Another thought: you could maybe try running Cache in a loop until it succeeds in downloading everything; I seem to remember it picks up where it left off if you run it again if only some of the files were downloaded (?).

[Jafar Tanoukhi]

Mac Malone said:

As far as I am aware, curl has no default timeout for downlaods [c.f. StackExchange) and cache does not set one, so it is a bit confusing what would be timing it out.

Hmmmm, i think it has to do with the server itself, as I requested the url https://releases.lean-lang.org/lean4/v4.22.0/lean-4.22.0-windows.tar.zst directly from my browser and it just refused to continue downloading after a couple minutes. My hopes for a PR that will fix this are shattered :smiling_face_with_tear:

[Jafar Tanoukhi]

Bryan Gin-ge Chen said:

Another thought: you could maybe try running Cache in a loop until it succeeds in downloading everything; I seem to remember it picks up where it left off if you run it again if only some of the files were downloaded (?).

I already wrote that as a little batch file it just fails at the same point over and over again xD. It does not pick up from where it left sadly.

[Jafar Tanoukhi]

image.png
Here's the annoying error

[Mac Malone]

Oh, that is an error downloading Lean itself (via elan), not Mathlib's cache.

[Jafar Tanoukhi]

I'm not sure I understand much what that implies? Also, does this mean that after this completes, there will be another one for the actual mathlib cache ?

[Jafar Tanoukhi]

I did run lake exe cache get successfully around a week or a little bit more ago. It asked it again and i assumed it's because of recents PRs pushed to mathlib-master?

[Mac Malone]

For context, Mathlib was recently updated to the latest Lean stable (v4.22.0) and when you run lake exe cache get it attempts to update Lean/Lake to that version by downloading the new release. That download is the one failing. It never gets to the point of running cache to download the Mathlib build.

[Jafar Tanoukhi]

Oh alright.