Mathlib CI doesn't get all available cache

Stream: mathlib4

[Jovan Gerbscheid]

In the past, if I made a change to a PR in a leaf file or a file like noshake that isn't related to building mathlib, then CI would be very fast, because it would get the cache from the previous CI run. Now, it doesn't get any cache from the previous CI run (instead getting just the cache from base mathlib).

This is very apparent in #27888, where I only changed the noshake file, and now have to wait for 40 minutes again for CI to be done.

I think this started happening when we switched to the new Github contribution model with forks.

[Kim Morrison]

Could you show the output from lake exe cache get? It should include diagnostic information about which cache it is trying to retrieve from.

[Kim Morrison]

I see, it says just:

Using cache from origin: leanprover-community/mathlib4
Attempting to download 6325 file(s) from leanprover-community/mathlib4 cache

so ... we have a problem here, and need to work out why cache is not trying to use the JovanGerb cache (in addition to the central one).

[Kim Morrison]

If someone would like to investigate this, that would be great.

[Bryan Gin-ge Chen]

This issue turns out to be part of what's causing CI trouble, see #mathlib4 > Failing CI @ 💬

[Sébastien Gouëzel]

Maybe it's well known here, but let me still mention it again: our CI (on the runners), when building a PR to mathlib from a fork, only downloads the cache from the leanprover community cache, and not from the fork's cache. I noticed that in https://github.com/leanprover-community/mathlib4/actions/runs/16864962436/job/47770567564: this is a PR which modifies a very basic file, and each time I push a commit then CI rebuilds all of mathlib, although most of it is already available from the fork cache. You can see that in the step get cache (3/3) .

[Sébastien Gouëzel]

This could maybe be solved by adding the --repo flag, as in the post-build step checking the cache.

[Bryan Gin-ge Chen]

Sébastien Gouëzel said:

This could maybe be solved by adding the --repo flag, as in the post-build step checking the cache.

I've opened #28253 for this.

[Frederick Pu]

are you free in 30 minutes?

[Frederick Pu]

oops wrong thread lol