New script: run_before_push.sh

Stream: Equational

[Terence Tao]

@Pietro Monticone has created a new script, run_before_push.sh (see equational#238) to allow one to locally run most (though not all) of the CI checks in advance of a PR. It can be run from the top level directory of the local copy of the repository.

I have just recently implemented branch protection to try to force myself to not abuse admin privileges by pushing to the main branch directly. Ironically in my experiments to do so I have still accidentally broken the build at least once today by clicking on the wrong button, but hopefully this will all get worked out soon.

[Pietro Monticone]

Added the related warning in the relevant section of the contributing guide.

CONTRIBUTING-WARNING.png

[Shreyas Srinivas]

I applaud this effort. In practice I expect mixed results because a lot of people have a set up where they automatically keep pushing commits.

[Shreyas Srinivas]

You can have your editor of choice handle this automatically, only asking for a commit message from the user.

[Shreyas Srinivas]

Vscode encourages this in particular if one uses the included git GUI

[Shreyas Srinivas]

What we need to do is embed your script as a git pre-push hook : https://stackoverflow.com/questions/4196148/git-pre-push-hooks

[Shreyas Srinivas]

Better source: https://git-scm.com/book/ms/v2/Customizing-Git-Git-Hooks

[Pietro Monticone]

Seems a good idea. Let me test it.

[Pietro Monticone]

Done.

[Pietro Monticone]

I have tested on VS Code, Git CLI and GitHub Desktop. It seems to work everywhere.

[Pietro Monticone]

If I understand correctly git hooks work only locally. Therefore I need to add another paragraph to the CONTRIBUTING guide.

[Floris van Doorn]

I don't want this script as a mandatory requirement before pushing. It's quite long, and it's doing the same as the CI already running on PRs, right?

[Shreyas Srinivas]

Something less than that

[Pietro Monticone]

Much less.

It ensures that the key components of the Lean project are functional before changes are pushed to the repository by checking that:

1. You are in the correct directory;
2. The project builds successfully;
3. The blueprint is successfully generated in both PDF and web versions;
4. LaTeX declarations in the blueprint match Lean declarations in the codebase.

It takes seconds, not minutes.

[Shreyas Srinivas]

It doesn't compile docs

[Shreyas Srinivas]

It doesn't do Jekyll compilation

[Pietro Monticone]

But it covers basically all errors I have manually fixed in different PR branches

[Pietro Monticone]

It seems to be a decent tradeoff.

[Shreyas Srinivas]

Does the git hook get pushed to GitHub?

[Shreyas Srinivas]

Okay it doesn't

[Pietro Monticone]

No no, but I wrote the installation script. It's coming.

[Shreyas Srinivas]

(deleted)

[Floris van Doorn]

the reply here gives a way to add it to the repository which is then very easy to enable by each user that wants it: https://stackoverflow.com/questions/3462955/putting-git-hooks-into-a-repository

[Pietro Monticone]

Done https://github.com/teorth/equational_theories/pull/256/

[Shreyas Srinivas]

https://stackoverflow.com/questions/427207/can-git-hook-scripts-be-managed-along-with-the-repository/37861972#37861972

[Shreyas Srinivas]

Oh okay

[Floris van Doorn]

Pietro Monticone said:

It takes seconds, not minutes.

If you can build this project in seconds, I am very interested to know what hardware you're running, because I would also like a 10-100x speedup in my Lean compilation time. For me it takes 6m15.691s to run the script (and this number likely grows as the repository grows).

[Shreyas Srinivas]

Btw, Floris, the end user still has the option to not run the install script

[Shreyas Srinivas]

What Pietro has implemented is close to the solution in your link and it requires user action on the client side to enable the hook

[Floris van Doorn]

I know, but thanks for the reminder.

[Pietro Monticone]

Floris van Doorn said:

Pietro Monticone said:

It takes seconds, not minutes.

If you can build this project in seconds, I am very interested to know what hardware you're running, because I would also like a 10-100x speedup in my Lean compilation time. For me it takes 6m15.691s to run the script (and this number likely grows as the repository grows).

I am confused here. I might have run after some lake exe cache get and lake build...

[Pietro Monticone]

Of course I did not have a fresh build

[Pietro Monticone]

I will remove the "strongly recommended" in the CONTRIBUTING guide and offer the 3 alternatives:

• installing the hook
• running the script
• waiting for the CI

[Pietro Monticone]

Done

[Pietro Monticone]

Updated the warning block.

Screenshot 2024-10-04 at 02.02.02.png

[Cody Roux]

Cool! Thanks for all the hard work! I think we'll need many more devops before the AI overlords take us...