Stale branches

Stream: mathlib4

[Yury G. Kudryashov]

Please have a look at https://github.com/leanprover-community/mathlib4/branches/stale
If you see your old branch here and you know you aren't going to need it anymore, then please delete it.

E.g., I suggest that we remove branch#port-status and branch#add-src-headers by @Reid Barton

[Kim Morrison]

Okay, I deleted >20 of mine!

[Eric Rodriguez]

Why should we do this?

[Yury G. Kudryashov]

E.g., if we setup gc for cache (I hope, we'll do it), then it will store oleans for all live branch heads.

[Xavier Roblot]

What is the most efficient way to delete a branch?

[Yury G. Kudryashov]

In web interface: there is a trash bin sign on the right.

[Yury G. Kudryashov]

From command line: git push origin :my-branch-name

[Yury G. Kudryashov]

If you're using some Git GUI (e.g., VS Code integration), then it depends on the GUI. In Emacs Magit, you can list branches, then press k on the branch you want to delete.

[Patrick Massot]

Is there any point in keeping branches corresponding to closed PRs?

[Johan Commelin]

Right now I can't think of a concrete reason to keep them. But my gut says that it's safer to keep them for 2~4 weeks.

[Joachim Breitner]

If the PR is on a repo that others may be using, the hash may occur in peoples lakefiles; deleting branches too quickly can cause confusion: https://github.com/leanprover/lean4/issues/3167#issuecomment-1888717265

[Sebastian Ullrich]

From a technical PoV I would wager that identifying stale branches would be far from the hardest part of cache GC, though it would certainly help if they weren't there at all

[Eric Wieser]

Patrick Massot said:

Is there any point in keeping branches corresponding to closed PRs?

bors deletes these by default anyway

[Eric Wieser]

So probably you're seeing local branches on your local machine that are already gone on github

[Patrick Massot]

No, I'm looking at GitHub only here.

[Patrick Massot]

Actually I'm fully confused by what I see here:
image.png
I am pretty sure I didn't update any branch yesterday.

[Joachim Breitner]

Could it be that you created the token that the bot is using? Sometimes github does such kind of misattribution

[Eric Wieser]

I think the bot might be reviving those branches?

[Patrick Massot]

This is probably a question for @Scott Morrison

[Kim Morrison]

If you look at #7845, it says:
7845.png

[Kim Morrison]

(That is the PR associated to lean-pr-testing-2732, which is otherwise long quiescent.)

[Kim Morrison]

(Patrick did make the final commit on that branch back in October, which explains why it showed up for him in the first place, but presumably not as "yesterday".)

[Yury G. Kudryashov]

Is it possible that you pushed all your branches, restoring those that were deleted on the server?

[Patrick Massot]

Ah, maybe I deleted it yesterday and then I wasn't sure so I restored it. But it doesn't explain why it wasn't automatically deleted long ago.

[Eric Wieser]

Only branches merged with bors are automatically deleted

[Eric Wieser]

That branch was closed and not merged