Skip to content
This repository has been archived by the owner on Oct 25, 2023. It is now read-only.
This repository has been 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

Closed
leanprover/lean4
#2603
@Julian

Description

@Julian

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 run lake exe cache get during a particular update. Some syntax like lake 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 the lakefile 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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions