Cache for v4.24.0-rc1

Stream: mathlib4

[Kitsune Kiriha]

Is .oleans for Mathlib v4.24.0-rc1 cached? Why my cache does not download cache of mathlib successfully?

Current branch: HEAD
Using cache (Cloudflare) from origin: leanprover-community/mathlib4
Attempting to download 6972 file(s) from leanprover-community/mathlib4 cache
Downloaded: 0 file(s) [attempted 6972/6972 = 100%, 88 KB/s]
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.
Alternatively, if you already have pushed your commits to a branch, this may mean the CI build has failed part-way through building.
Decompressing 227 file(s)
Unpacked in 21 ms
Completed successfully!

[Kevin Buzzard]

What is the output of git status?

[Kitsune Kiriha]

$ git status

Not currently on any branch.
nothing to commit, working tree clean

$ git tag -l

v4.24.0-rc1

$ git log

commit eed770a434957369c6262aa3fb1d6426419016d4 (grafted, HEAD, tag: v4.24.0-rc1)
Author: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date:   Mon Sep 15 12:54:32 2025 +0000

    chore: bump toolchain to v4.24.0-rc1 (#29671)



    Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
    Co-authored-by: leanprover-community-bot-assistant <97194829+leanprover-community-bot-assistant@users.noreply.github.com>

[Kevin Buzzard]

I did git checkout v4.24.0-rc1 and tried lake exe cache get but unfortunately I already had all the oleans from that commit locally, so it succeeded but with this message:

Current branch: HEAD
Using cache (Azure) from origin: kbuzzard/mathlib4
No files to download
No files to download
Decompressing 7199 file(s)
Unpacked in 38273 ms
Completed successfully!

[Kitsune Kiriha]

It seems you already have cached locally, could you clean the .lake folder and try again?
(Another: Your source seems to be kbuzzard/mathlib4, while mine is leanprover-community/mathlib4)
(Both Azure and Cloudflare fails)

[Kitsune Kiriha]

Solved. It seems one of the dependency of mathlib4 have the wrong revision. I manually fixed through the lake-manifest.json file.