Potential problem with v4.28.0-rc1

Stream: nightly-testing

[Kim Morrison]

Mathlib is now on v4.28.0-rc1. However the PRs cslib#292 and repl#143 appear to be rebuilding Mathlib rather than using the cache.

Locally, the cache seems to work fine for me, both in Mathlib and in downstream projects. (Testing on macos in case that is relevant.)

If anyone is available to take a look, and report here, that would be great. Diagnosing the problem would be even more amazing. (It's late here, but I'll look at this after sleeping.)

[Kim Morrison]

(Pinging @Mac Malone in case he recognizes these symptoms as possibly caused by recent changes in lake.)

[Chris Henson]

For me, locally on Linux the cache seems to work for CSLib. I'll hold off merging until this is resolved.

[Mac Malone]

Sadly, I don't recognize this. I can't think of any recent Lake changes in the area (there will be this month, but I have not merged any yet).

[Mac Malone]

Looking at the CSLib CI run, the problem appears to be cache itself partially failed. It found only 1449 of 7873 in the cache.

[Mac Malone]

The REPL run encountered the same failure. It had the exact same file count, so it is likelynot a transient error.

[Mac Malone]

Inversely, the Mathlib CI run cache check for v4.28.0-rc1 did succeed in downloading all the files.

[Mac Malone]

Local testing works for both Mathlib and the PRs. Perhaps this was some temporary unavailability for those files from the Azure side? @Kim Morrison, I would suggest reruning the CI to verify whether the issue reproduces.

[Chris Henson]

Rerunning the CSLib CI seemed to work, so I am going to go ahead and merge.