Why does CI fail on my branch?

Stream: mathlib4

[Martin Dvořák]

#9838

Downloaded: 1699 file(s) [attempted 4146/4146 = 100%] (40% success)
Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.
If you push your commits to a branch of the mathlib4 repository, CI will build the oleans and they will be available later.
/home/lean/.cache/mathlib/02274134bfaa6d3d.ltar: failed to fill whole buffer
Decompressing 1699 file(s)
uncaught exception: leantar failed with error code 1
Error: Process completed with exit code 1.

[Mario Carneiro]

the file 02274134bfaa6d3d.ltar is corrupted, you should delete it

[Mario Carneiro]

this should not happen with recent versions of cache though

[Martin Dvořák]

Where is 02274134bfaa6d3d.ltar please? My cache seems to be pretty new.

[Mario Carneiro]

the path is listed in the message

[Mario Carneiro]

I see this error happens in CI... do you get the same error locally?

[Mario Carneiro]

I won't be able to get to this today, a quick workaround is to invalidate the whole cache by adding some whitespace in lake-manifest.json

[Emilie (Shad Amethyst)]

I've had lake exe cache get! fix that for me in the past, it happened because I had done a lake exe cache get before the CI was over

[Michael Rothgang]

Also happened on CI for #9856 and #9809. The former is from recent master (1h old, at most).

[Michael Rothgang]

Retrying fixing it on the former PR.

[Martin Dvořák]

Mario's trick solved it for me.

[Matthew Ballard]

Is the white space trick still the best option here?

[Jack Valmadre]

+1. I encountered this issue in CI a few times yesterday and today. e.g. https://github.com/leanprover-community/mathlib4/actions/runs/7660457408

(CI failing in stage "get cache" with error "/home/lean/.cache/mathlib/xxx.ltar: failed to fill whole buffer")

[Kevin Buzzard]

You could try merging master but if that doesn't fix it then you'll have to summon the maintainers.