lake update updating toolchain

Stream: lean4

[Jon Eugster]

Would it be possible to come up with a solution that would allow lake projects to keep their toolchain fixed to match one specific dependency? (i.e. usually mathlib). It has tripped me and others repeatedly up that the required commands are

lake update
cp ./lake-packages/mathlib/lean-toolchain ./lean-toolchain

and honestly at least 70% of my lean4 projects just want to have their lean-toolchain matching exactly the one of a specific dependency. Even if it's not mathlib, I'd probably still want the option to keep the toolchain of a project always in sync with the most fragile/largest dependency, be it std or proofwidgets or whatever is the biggest dependency in my project.

[Jon Eugster]

I'm happy to try to work out a proposal, but I'd like some encouragement from the relevant people that such a PR/issue would be welcome :blush:

[James Gallicchio]

my personal hesitation is that it is a brittle fix for a much more complicated problem that we haven't even started to address (managing dependency updates). maybe a nice first step would be for lake to have "update hooks" that let you execute scripts as part of lake update? that way you can configure your project to track mathlib toolchain without such a feature being a part of lake?

[Mac Malone]

Actually, the newest version of elan now has sime support for this. See elan#99. With the new elan, you can set your toolchain to leanprover-community/mathlib4:lean-toolchain and it will automatically use the latest mathlib toolchain.

[Sebastian Ullrich]

Oh my, is it already time to regret that feature? It should go without saying, but do not put an unpinned Lean version like that in your lean-toolchain. Really the only correct use of that specifier is in combination with lake new/init.

[Mac Malone]

@Sebastian Ullrich Yeah, that fact that it was unpinned occurred to me while I was writing that, but I did not listen to my better angels and wrote it anyway. :sweat_smile:

[Jon Eugster]

on second thought, probably it would completely suffice to have the instructions at

https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency#updating-mathlib4

bundled into a command like lake exe up that comes shipped with mathlib:thinking:

[Mac Malone]

I would suggest, given how short it is, to just make a Lake script that does it (e.g., lake run mathlib/update-toolchain).