This repository was archived by the owner on Oct 25, 2023. It is now read-only.
Support project-specific post-update hooks called after running lake update
#185
Labels
enhancement
New feature or request
It would likely be convenient if
lake
supported a way to define post-update operations within alakefile
.I.e., a project could define within its
lakefile
what to run after a user runslake 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
intolake 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 runlake 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:
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)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.
The text was updated successfully, but these errors were encountered: