lake exe cache get not respecting lean-toolchain?

Stream: lean4

[Mikhail Mayorov]

I encountered the following today:

I only have 4.28 toolchain installed and i just cloned a mathlib-dependent project that's using 4.26.
Running lake exe cache get fails with an error(some String function was there in 4.26 but got removed in 4.28), because it just uses the default/only toolchain I have(4.28).

But when I run lake build it correctly identifies that i don't have the needed toolchain installed and starts downloading it.

So my question is, why doesn't lake exe... respect lean-toolchain file? Or maybe my story just doesn't add up and I missed something? I understand I can probably find the answer in the reference if I read it long enough, still some help would be appreciated.

Another perhaps important detail is that the project didn't have lake-manifest.json in it.

[Ruben Van de Velde]

I don't think we can say anything more than "this is supposed to work" from your description

[Mikhail Mayorov]

Yes, I apologize, it was indeed a mistake on my end. The project had an unversioned dependency on another project that got bumped to 4.28(and my description of what happened was not totally accurate).

Still I was surprised to learn that building a project without lake-manifest can just bump its toolchain.

[Jon Eugster]

indeed, I find lake --keep-toolchain ... much more predictable and have yet to find a use case where I would want lake to interfere with the project's toolchain...

I think the feature would be much better if there was a way to prioritise the toolchain required by mathlib over toolchains from other dependencies, but I doubt lake would want to hardcode that so it would need to be yet another configuration option