cache down?

Stream: mathlib4

[Kim Morrison]

I'm seeing no cache available on mathlib master at the moment. Anyone else?

% git describe
v2024-405-ge808ef0e67
% lake exe cache get
Attempting to download 4149 file(s)
Downloaded: 0 file(s) [attempted 4149/4149 = 100%] (0% success)

[Yury G. Kudryashov]

Same here

[Yury G. Kudryashov]

It looks like uploads fail, not downloads: cache works for 69a8f62cf1

[Yury G. Kudryashov]

99315bf71cec8eb94c2cc14e8198a032a7d9b12c #9725 is the first commit w/o a cache

[Yury G. Kudryashov]

Nothing suspicious in the log but I'm not sure that "Attempting to upload N file(s)" reports an error if it happens.

[Jeremy Tan]

I note that GitHub is rolling out a new behaviour for CI – it now always shows you the last 1000 lines of log. And the build times for our repository are now even slower than before – building counterexamples used to take less than a minute, now it takes 3+ minutes

[Eric Rodriguez]

The reason we don't seem to notice this is that currently the "check the cache" steps are toothless - the files are already in place so they're not redownloaded in CI to make sure stuff is working properly. I will push a fix for this.

[Eric Rodriguez]

#9933, I expect the run to fail

[David Renshaw]

It looks to me like maybe the upload curl command does not check the HTTP status code of the response. https://github.com/leanprover-community/mathlib4/blob/2475f305cecbfdf1fb57959e0634db06563c985a/Cache/Requests.lean#L206-L208

[David Renshaw]

The --fail-with-body flag might help: https://curl.se/docs/manpage.html#--fail-with-body

[David Renshaw]

(Lean's static curl is new enough to support that flag: https://github.com/leanprover-community/static-curl/releases/tag/v7.88.1 )

[David Renshaw]

My hypothesis is that the upload is returning a 4XX or 5XX HTTP response code (maybe Bad Request because it's too big somehow, or maybe something auth-related), and then we don't get to see what the error is because we ignore stderr (we set stderrAsErr := false : https://github.com/leanprover-community/mathlib4/blob/2475f305cecbfdf1fb57959e0634db06563c985a/Cache/IO.lean#L159-L165

[Eric Rodriguez]

David, could you make a patch to the CI that runs this and outputs the error code in order to see what the issue is? One thing I do worry about is that it may accidentaly leak the secrets if this is done

[David Renshaw]

I submitted #9934 to try --fail-with-body, but looks like that CI run isn't going to be so informative, because the machine seems to already have the cache locally.

[David Renshaw]

Maybe I should make a trivial change inside of mathlib, so that it needs to upload something

[David Renshaw]

One thing I do worry about is that it may accidentaly leak the secrets if this is done

Makes me want a Lean binding to libcurl, so that we would have tighter control.

[Eric Rodriguez]

For fast CI running, you could in theory just clear most of Mathlib I think?

[David Renshaw]

Aha, we got ~4000 lines of

curl: (22) The requested URL returned error: 403

[David Renshaw]

https://github.com/leanprover-community/mathlib4/actions/runs/7626176854/job/20772003823

[David Renshaw]

403 means authorization failure ("forbidden").

[David Renshaw]

I wonder if we need to refresh secrets.MATHLIB_CACHE_SAS. I don't know how that stuff is set up.

[Yury G. Kudryashov]

In the meantime, 5a0540a5b1 is the last revision with cache.

[Matthew Ballard]

Does the FRO cache also have a secrets problem?

[David Renshaw]

It looks to me like the FRO/R2 code puts the secret token in a command-line argument, which potentially gets printed on error.

[David Renshaw]

The Azure codepath (currently active) puts the token in a config file, which does not get printed.

[Matthew Ballard]

Does the FRO code path error?

[David Renshaw]

If the curl subprocess exits with a non-zero code (and we should assume that can happen), then it prints out the args: https://github.com/leanprover-community/mathlib4/blob/e53e613abdea8d5b8863cbfb93014b9493e719d1/Cache/IO.lean#L161-L162

[David Renshaw]

It's possible that Github actions has some smart logic that will redact the token from logs, but I wouldn't count on it.

[David Renshaw]

I'm also a bit confused about why the Cloudflare R2 code path is being referred to as the "FRO" path (e.g. the useFROCache variable name). My understanding is that the FRO is footing the bill under both configurations?

[Mario Carneiro]

I've added a new MATHLIB_CACHE_SAS. If someone who is using CI could report whether uploads work now that would be helpful

[David Renshaw]

I rebased #9934, triggering a job.

[Matthew Ballard]

This seems to work

[David Renshaw]

on #9939 (based on an older commit) we get

curl: (22) The requested URL returned error: 409

[David Renshaw]

maybe that's the expected error for cache files that have already been uploaded?

[Mario Carneiro]

seems likely

[Mario Carneiro]

I think there are ways to make curl treat specific http response codes as a success

[David Renshaw]

I got the HTTP 409 error also on #9934, -- but less than 1000 instances of it.

[David Renshaw]

And then when I do lake exe cache get locally for that branch, it succeeds.

[David Renshaw]

So I think this confirms

1. Mario's token update fixed things
2. the 409 response indicates cache files that have already been uploaded (typically from other commits)

[David Renshaw]

I suppose we'll really see whether things are fixed once the next commit lands on master

[David Renshaw]

actually, cache for the latest master commit seems to be working now too. :tada:

[Jeremy Tan]

Yes, but why are tests still taking 3+ minutes rather than about 1?
https://github.com/leanprover-community/mathlib4/actions/runs/7631758536/job/20790451359#step:22:8

[Mario Carneiro]

this has nothing to do with cache

[Mario Carneiro]

you may need to bisect to find when this happened

[Mauricio Collares]

(The slowdown discussion here continues at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Testing.20slowdown)