Cache failures with the Lean bump

Stream: mathlib4

[Jeremy Tan]

Screenshot_20230421_174848_Firefox.png
!4#3557 by @Gabriel Ebner was merged, but caches are not being downloaded or uploaded at all. This means I have to wait 2 to 3 hours on every staging. This is a CI regression

[Jeremy Tan]

(i.e. all of Mathlib is being rebuilt with every stage, instead of just the files that need to change)

[Eric Wieser]

Can you link to the CI run rather than pasting a screenshot?

[Jeremy Tan]

https://github.com/leanprover-community/mathlib4/actions/runs/4762768528/jobs/8465383505

[Mauricio Collares]

Did you merge master in the PRs you want to download caches for?

[Mauricio Collares]

Or are you talking about master?

[Jeremy Tan]

I am talking about master

[Jeremy Tan]

It's happening again with https://github.com/leanprover-community/mathlib4/actions/runs/4763966428. Even though just one file is added, CI is rebuilding everything from scratch

[Eric Wieser]

I wonder when the last successful cache upload was; is the new lean version to blame, or has it been broken for a while and the lean version just invalidated some already-stale caches?

[Sebastian Ullrich]

I think !4#3571 should fix it

[Sebastian Ullrich]

Running put after a partial build on master and the PR:

 ~/lean/mathlib4   master  MATHLIB_CACHE_SAS=1 lake exe cache put
Compressing cache
No files to upload
 ~/lean/mathlib4   master  git co -
Switched to branch 'fix-cache-c-trace'
Your branch is up to date with 'origin/fix-cache-c-trace'.
 ~/lean/mathlib4   fix-cache-c-trace  MATHLIB_CACHE_SAS=1 lake exe cache put
info: [0/8] Building Cache.IO
info: [1/8] Compiling Cache.IO
info: [1/8] Building Cache.Hashing
info: [3/8] Building Cache.Requests
info: [5/8] Building Cache.Main
info: [8/8] Linking cache
Compressing cache
Attempting to upload 122 file(s)

[Eric Wieser]

I guess we may as well wait for CI to finish, since then it will use the new cache after merging

[MonadMaverick]

2023-04-21-221706_3840x2160_scrot.png
CI status is "passing" now.
But cache dosn't work.

[Anne Baanen]

"Could not resolve host" suggests an outage on the internet commection somewhere between your computer and the olean cache server, not a CI failure. For me, dig lakecache.blob.core.windows.net returns an address but pinging it gives "Destination Host Unreachable".

[Anne Baanen]

So it being down for both of us suggests an issue on Azure. On the other hand, Azure doesn't report any outages: https://portal.azure.com/#view/Microsoft_Azure_Health/AzureHealthBrowseBlade/~/serviceIssues

[Sebastian Ullrich]

Not every server likes to be pinged, try curl instead. In any case, the issue will not be resolved before the PR is merged.

[Eric Wieser]

The issue will be mostly resolved once the PR is built; the cache will then be available for everyone for a single more recent commit, which at least will have accurate caches for all the early files.

[Mauricio Collares]

That's done