lake version does not match the toolchain version

Stream: general

[Riccardo Brasca]

After doing lake update in a project I get the warning

info: mathlib: checking out revision 'df27cff57fa72144f1d69257b0619c7390ab7b9a'
info: toolchain not updated; already up-to-date
info: batteries: checking out revision 'c029ceb9956ef9d567fc034e5403ec829f8d0d87'
info: mathlib: running post-update hooks
Not running `lake exe cache get` yet, as the `lake` version does not match the toolchain version in the project.
You should run `lake exe cache get` manually.

It's a not a big deal since lake exe cache get works as expected, but what should I do to fix it?

[Weiyi Wang]

My take is that there is nothing to fix and you only need to follow it by running lake exe cache get once?

[Weiyi Wang]

(I also got this for every project I upgraded )

[Riccardo Brasca]

I did it, but it happened again

[Kim Morrison]

@Riccardo Brasca, this project doesn't have a lean-toolchain, so basically all bets are off for any Lean tooling behaving sanely. :-) Please fix that first.

[Riccardo Brasca]

Not sure I understand this comment, there is a lean-toolchain file.

[Weiyi Wang]

I think I have got the same issue when I tried updating it again today. I also have lean-toolchain file with content

leanprover/lean4:v4.25.0-rc2

as for lake version

lake --version
Lake version 5.0.0-src+744f980 (Lean version 4.25.0-rc2)

[Eric Wieser]

The error is reporting the state in the middle of the update, not after

[Asei Inoue]

I got a same warning

[Kim Morrison]

Hopefully #31523 will resolve this problem.

[Riccardo Brasca]

Thanks a lot!

[Wrenna Robson]

To be clear though - it isn't actually an issue for now?

[Riccardo Brasca]

What happens for me is that I have to run lake exe cache get manually, so it's not a big deal, but it would be nice to have this working.

[Kim Morrison]

Wrenna Robson said:

To be clear though - it isn't actually an issue for now?

Yesterday I was still seeing the issue when running lake update in flt-regular.