Support project-specific post-update hooks called after running lake update
#185
Description
It would likely be convenient if lake
supported a way to define post-update operations within a lakefile
.
I.e., a project could define within its lakefile
what to run after a user runs lake update
within the project and lake finishes updating it.
In particular, such a thing seems like it might help some of the Mathlib update issues by at least "packaging up" running lake exe cache get
into lake update
, which could be done by Mathlib defining such a post-update hook.
The advantage of doing so over a new command is that it would mean Mathlib did not go around telling users to never run lake update
and to instead run lake exe update-mathlib
or what have you -- which creates a bit of ecosystem confusion for users on the current "biggest project" -- when moving to some other project they'd have a different workflow. Whereas with post-update hooks, Mathlib could present the same interface.
Other miscellaneous considerations:
- Would it run on failure of whatever kind? (seems like it shouldn't)
- Some mechanism will likely be needed for not running the hook even when running
lake update
. In Mathlib's case for example, sometimes someone will not want to runlake exe cache get
during a particular update. Some syntax likelake update --without-hook post-update:cache
seems like it might be needed here so that users who aren't as advanced always get the default behavior, but someone could disable the hook (where I've proposed there making hooks be named so that they can be turned off by name, which is something thelakefile
hook definition syntax would need to support) - Would post-update hooks run recursively -- e.g. if a dependency has a post-update hook, does it run when lake updates it, or does that only happen for the "current project" someone is running?
- What version of the post-update hook is used if the lakefile changes during updating?
- Obviously such a thing is generalizable (to running hooks before or after other commands, or to replacing what commands do entirely). To me I might be conservative with adding them initially, given it seems like only one or two is likely to be needed for some of the Mathlib UX needs.
Original context can be found in and around https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Updating.20using.20lake.20again/near/393936116
Additionally related is also leanprover/lean4#2752 inasmuch as it too is trying to reduce the number of commands someone needs to run by 1.
Activity