Lake cache asks me to run lake cache manually.

Stream: lean4

[Shreyas Srinivas]

Steps to run

1. Start a project on toolchain v4.25.1
2. Run lake update. lake says you need to run cache manually because the default toolchain outside the project is 4.24.0
3. cd into the project directory
4. run lake exe cache get
5. Lake again says

You should run `lake exe cache get` manually.
Fetching ProofWidgets cloud release... done!
Current branch: HEAD
Using cache (Azure) from origin: leanprover-community/mathlib4
No files to download
Decompressing 7536 file(s)
Unpacked in 7400 ms
Completed successfully!

6. Run lake build. lake is now building all of mathlib

[Ruben Van de Velde]

Try 4.25.2

[Shreyas Srinivas]

Okay. I made it work by going to 4.26.0-rc2

[Shreyas Srinivas]

I'll note that I also tried setting Mathlib's rev to stable and lake fixed the toolchain to v4.25.1

[Ruben Van de Velde]

Shreyas Srinivas said:

I'll note that I also tried setting Mathlib's rev to stable and lake fixed the toolchain to v4.25.1

So it seems. @Kim Morrison Kiiiiiiiiiiiiiiiiiiim! :)

[Kim Morrison]

Thanks, stable has been updated to v4.25.2. (The dangers of doing things manually when you have perfectly good automated scripts to handle it...)