post-update hooks

Stream: lean4

[Marcello Paris]

When running lake update, I noticed that Lake currently runs post-update hooks for all dependencies unconditionally, even when the dependency revision has not changed.
This is somewhat costly for mathlib, whose post-update hook decompresses ~7,800 files on every run, making lake update noticeably slower in cases where nothing actually updates.
I’m wondering whether it might make sense to have a way to skip post-update hooks (e.g. a --no-hooks flag), or some mechanism to avoid running them when the dependency hash is unchanged (possibly just for mathlib)

[Kim Morrison]

Are you running lake update often? Usually this is best handled by CI, e.g. via the lean-update-action.

[Marcello Paris]

That's a fair point, I think I've been overcomplicating my workflow. I'm using Mathlib in an application, so I rebuild frequently, but I'm not actually relying on new features, so there's no real reason to track HEAD. Pinning to a specific commit and updating deliberately makes more sense. Thanks