Automatic setup and distribution of git hooks

Stream: mathlib4

[Robin Carlier]

Git has a nice "hooks" feature that allows one to run scripts before/after different git actions (commit, push, etc. ) and allows for instance to prevent pushing if lake exe lint-style fails, or running lake exe cache get upon branch switching.

As these hooks have to be put in the .git folder by default, they are not subject to version control, and so it’s normally up to each and everyone to setup their hooks, but I believe some of them could (and should) be distributed and put up automatically when setting up mathlib (for instance, the lint-style one before pushing) or when running lake update on mathlib.

• What should be the "right way" to do this? Would adding a lake exe setup-hooks, documenting its existence and recommend running it once when setting up a mathlib fork be acceptable?
• Which hooks would be considered good as having "by default"? I would say lake exe lint-style before pushing would be nice, what are other "cheap linters" that could be run before pushing? Conditioning pushing to a lake build is perhaps too much given that it might take a while on some systems.

[Ruben Van de Velde]

We used to have that in lean 3, though I ended up turning it off because I often didn't want/need the cache and it takes a while to try to download everything

[Robin Carlier]

yes, post-checkout lake exe cache get should probably not be a default, I’d say most defaults should concern pre-push-type of hooks.

[Johan Commelin]

Before think about if/how to distribute, I think we can start by having a nice collection that we can point to, on the website

[Johan Commelin]

And once that has stabilized we can think about distributing it by default