scripts/githelper.py

Stream: mathlib4

[Joscha Mennicken]

After being nerdsniped by #mathlib4 > all future PRs should be made from forks @ 💬, I went and actually wrote the script. It is available in PR #26023. If you want to try it out right now, you can run curl https://raw.githubusercontent.com/Garmelon/mathlib4/refs/heads/githelper/scripts/githelper.py -o scripts/githelper.py in the root directory of your mathlib repo to download it.

One possible use is to run it before running the migrate_to_fork.py script to prepare the repo and fork, or after running migrate_to_fork.py if it seems like it has messed something up. My script tries to be more general than migrate_to_fork.py in understanding the repository state, and my hope is that it is more robust as a result. However, it is also a bit more opinionated than migrate_to_fork.py. This can be a good thing - it helps with troubleshooting if everyone has the same setup.

The script was only tested on Linux, not on Windows, its output could be more helpful, and there might of course be bugs. If you notice anything that seems wrong, please let me know :)

[Bryan Gin-ge Chen]

I just tested this on macOS and I got an error at this step:

WARNING: Branch 'master' should have pushRemote 'origin'.
Update pushRemote of 'master'? [Y/n]:
$ git config set -- branch.master.pushRemote origin
usage: git config [<options>]

Config file location
<deleted help output from git config>
ERROR: Command failed with status 129

[Joscha Mennicken]

Hmm, maybe the -- syntax is only allowed after the config name in older git versions? Or maybe it is not allowed at all? Can you run git config set branch.master.pushRemote -- originmanually?

[Bryan Gin-ge Chen]

I get the same output when I run it manually. My version of git is apparently:

$ git --version
git version 2.39.5 (Apple Git-154)

[Joscha Mennicken]

What happens when you move the -- one argument to the right, or if that doesn't work, remove it entirely?

[Bryan Gin-ge Chen]

git config set branch.master.pushRemote origin -- gives the usage output again, and git config set branch.master.pushRemote origin gives:

error: key does not contain a section: set

[Joscha Mennicken]

I see, the git config set subcommand was only added in git 2.46.0. Thanks for the report, I've updated the PR.

[Bryan Gin-ge Chen]

The new version runs succeeds without errors, thanks!