New CI cache workflow not working properly

Stream: mathlib4

[Sébastien Gouëzel]

CI has been modified recently wrt cache. As far as I can see, the cache is not uploaded any more for a failing build (see for instance the run of #35252). This means that one can not any more fix iteratively a PR, which looks very bad to me. Is that by design, or should we fix/revert?

[Matthew Ballard]

PR?

[Damiano Testa]

This is certainly not intended.

[Damiano Testa]

This may be the culprit: https://github.com/leanprover-community/mathlib4/blob/c1475f9635e4b0a4effd917098e2fa3acf2cb8be/.github/workflows/build_template.yml#L607

[Damiano Testa]

It seems that uploading the cache is subject to the build step succeeding. EDIT: maybe not exactly there.

[Sébastien Gouëzel]

The CI change comes from #34847, I guess.

[Matthew Ballard]

We really need some CI behavior tests

[Damiano Testa]

It looks like the script that builds mathlib should have tried up to 5 times, but errored before finishing the first round.

[Damiano Testa]

Let's ping @Marcelo Lynch, since he is more knowledgeable of the current setup.

[Bryan Gin-ge Chen]

Marcelo already made a fix for this in #35390. I would also like to bring attention to another fix he made in #35389 which will make PRs like #35390 easier to merge.

[Bryan Gin-ge Chen]

(I would have merged these myself, but I pushed a commit to #35389.)

[Damiano Testa]

I just sent #35389 to bors.

[Bryan Gin-ge Chen]

OK, I've put #35390 in the same batch.

[Bryan Gin-ge Chen]

These PRs are now merged so hopefully the the cache will be uploaded for failing builds as well. (The new versions of the build workflows should work even without merging master, although I'm not sure if re-running previous jobs will trigger the new versions or not.)

[Kim Morrison]

It would be lovely if we could recover the old (back in mathlib3 days??) behaviour whereby even when a build was cancelled due to a new push, it would take the time to upload what it had so far.

[Yaël Dillies]

I am pretty sure cancelled workflows do upload their cache currently ?

[Kim Morrison]

I thought I saw this not working today, but indeed the yaml files suggest it should work!

[Marcelo Lynch]

Here's an example

[Andrew Yang]

I'm not sure if this is related to the new CI workflow but lake exe cache get is not working for me on #29550.
When I cross compare the output of lake exe cache get

Fetching ProofWidgets cloud release... done!
Current branch: Raph-DG-DVR
Using cache (Azure) from Raph-DG: raph-dg/mathlib4
Attempting to download 7997 file(s) from leanprover-community/mathlib4 cache
Downloaded: 4351 file(s) [attempted 7997/7997 = 100%, 63 KB/s]
Attempting to download 7997 file(s) from raph-dg/mathlib4 cache
Downloaded: 0 file(s) [attempted 7997/7997 = 100%, 0 KB/s]
Warning: some files were not found in the cache.

and the output of the CI on that commit

Attempting to download 3646 file(s) from Raph-DG/mathlib4 cache

I noticed that the capitalization are different, and when I went into Cache/Requests.lean and overwrote getRepoFromRemote to always return Raph-DG/mathlib4 instead it successfully got cache.

My local machine is running on MacOS and it might be related as MacOS seems to treat capitalization weirdly.

[Marcelo Lynch]

Looking at the logs, this indeed should be caused by the mismatch in capitalization between the URL that Github returns (which has the capitalization) and the one used locally (which is 'chosen' when you git clone http://..., and GitHub treats this case insensitvely at this point so the mismatch would not cause an issue here

This is not a regression caused by the recent changes, --repo has been treated case-sensitively since before those.

A manual git clone ... with all-lowercase would be my best guess of how this happened. If you run git remote -v you should see your local all-lowercase URL. You can change it to match the mixed-case one that is canonical for GitHub with git remote set-url origin <normalized-url> (assuming origin is the name here), and cache should use the updated one.

[Marcelo Lynch]

.