Old stale PRs

Stream: mathlib4

[Laura Monk]

Hi! I was trying to start reviewing PRs on Mathlib for the first time, but got quite intimidated by the numbers. Then I had a look at the older PRs and it looks like most (or all?) of them are abandoned and now completely conflicted. I was discussing this with someone and he told me some repos use a bot who writes a comment (say after 1 month) saying if there is no activity in the next x days the PR will be closed. To keep it open you can just write a comment. I was wondering if we could maybe consider using such a bot to diminish the amount of open PRs? We could make the bot take into account dependencies obviously. I am assuming for the most experienced reviewers it is easy to filter what is what and understand which issues are active or not, but from my newbie viewpoint it feels it would help at the entry level.

[Aaron Liu]

You can try commenting on the PR to get the author to do something

[Junyan Xu]

You can check https://leanprover-community.github.io/queueboard/review_dashboard.html for the "active, ready for review" PRs.

[Laura Monk]

Sure, but is there really an advantage to keeping a lot of abandoned PRs which will never be merged open?

[Bryan Gin-ge Chen]

We actually have some automation that we were testing for this, but it broke I broke it and didn't get around to fixing it while awaiting further maintainer discussion. I believe there should be some movement on this front in the near future!

[Laura Monk]

Nice, thank you! Looking forward to it :)

[Johan Commelin]

@Laura Monk Also, thanks a lot for wanting to help with reviews! Much appreciated!

[Yaël Dillies]

It turns out there's a lot of good stuff in some old PRs, which is why I am reluctant to close them. From time to time I look around and revive a few

[Yaël Dillies]

Also note that we moved to a fork-based workflow two months ago, and a lot of people haven't yet closed their PRs made from branches, even though they won't be able to edit them further

[Junyan Xu]

There are mathlib3 PRs to be rescued too and I've suggested that the repo may need to be un-archived in order for PRs to be searchable. (Update: reported to Github)

[Yaël Dillies]

Also please please delete the branch when you close a PR. A week ago we have 6.5k branches on the mathlib repo, and a lot of people copied all 6.5k of them to their fork when switching to a fork-based workflow (doesn't help that this is what github does by default when you try to edit a file in mathlib from the interface...), which in turn means that I cannot review PRs from many people simultaneously, because to review PRs from N different people I need to clone N different forks and their 6.5k * N branches. For not even that big values of N, this makes branch switching from within the vscode UI impossibly slow.

[Aaron Liu]

I just ran the migrate to fork script and it copied all the branches when I ran it

[Aaron Liu]

I suspect this is what happened for many other people too

[Yaël Dillies]

I thought so too, but I wasn't sure because I didn't run it

[Yaël Dillies]

Just by deleting branches from closed PRs and obsolete pr-testing branches, I got that number down to 2.2k branches!

[Junyan Xu]

Johan Commelin said:

Junyan Xu said:

So now if I want to review a PR locally (not in Gitpod/codespace) I'll need to add the author's fork as a remote. The git command is nontrivial to type. Can we add a VS Code command in the palette or a lake command to minimize typing / memorization?

gh pr checkout 12345 should work, which I think is similar in difficulty to the old approach of git checkout some_branch_name.

Does this solution clone the whole repo or just check out the branch? I haven't really tried as I'm still mostly relying on Gitpod for PR reviews.

[Johan Commelin]

I run it inside an existing clone.

[Yaël Dillies]

Yes, but a clone of the fork you're reviewing a PR from, or your own fork?

[Yakov Pechersky]

gh pr checkout does it within your own fork

[Joscha Mennicken]

Aaron Liu said:

I just ran the migrate to fork script and it copied all the branches when I ran it

githelper.py only keeps the master branch when forking, while migrate_to_fork.py keeps all branches (the default behavior). Probably worth a PR.

Maybe githelper.py could gain a command to delete all branches in your own fork except those mentioned by your own open PRs?

[Joscha Mennicken]

Yakov Pechersky said:

gh pr checkout does it within your own fork

gh pr checkout does not add the branch to your own fork, only to your local repo. It does not require adding a separate remote or anything, and only checks out the single branch from the PR.

(For those interested in the details: A repo on GitHub basically has a hidden branch for every PR, even if the PR itself comes from a branch in a different repo. gh pr checkout checks out that hidden branch and gives it a nice name locally. Thus there's no need to add the repo the PR comes from as a remote.)

A fork here is a GitHub-specific term for a repo on GitHub that's been forked (split off/based on) from another repo on GitHub. Your locally cloned repo is a separate thing that can have multiple other repos as remotes. Usually those remotes include both your fork as well as the original GitHub repo that it was forked from, but there may also be other remotes.

[Joscha Mennicken]

Opened a PR that limits forks to only the master branch when using migrate_to_fork.py: #28643

[Yakov Pechersky]

Yes, sorry, I meant shorthand for the local on-machine clone.

[Joscha Mennicken]

I've now opened #28657 which adds a prune subcommand to githelper.py that deletes unused branches in your fork (i.e. branches that are not used in any open PRs). Branches in your local clone are not affected. I'd appreciate any feedback.

To try it out with your fork, run

1. gh pr checkout 28657
2. python scripts/githelper.py prune (add --help to see available options)

[Kim Morrison]

I'm happy to merge on the basis of someone reporting that it works for them. :-)