Zulip Chat Archive

Stream: mathlib4

Topic: see commits in deleted branch?

Thomas Murrills (Jan 05 2023 at 19:10):

More of a git question than a mathlib4 question, but—is it possible to see commits in a deleted branch?

This normally wouldn’t be an issue, but an opportunity to apply to something came up, and I thought I’d include my contributions to Data.List.Basic.

However, I wasn’t listed as a coauthor on the commit, so it doesn’t appear as a contribution on github, I don’t think—and the squash merge squashes together all of the different contributions anyway, so I wouldn’t be able to point to exactly what I contributed.

If I had to show someone the commits I made there, what’s the best way?

Niels Voss (Jan 05 2023 at 19:15):

I might be wrong, but I think the commits in a PR are permanently recorded in the PR so I'd you view a closed PR on GitHub they will still be available in the commits tab

Thomas Murrills (Jan 05 2023 at 19:17):

ah, that works, thanks!

Niels Voss (Jan 05 2023 at 19:22):

I think local deleted branches are a bit different, since their commits get automatically deleted after a few months (you might be able to access them with git reflog until then)

Thomas Murrills (Jan 05 2023 at 21:29):

Semi-related question, I guess: is it normal to not receive contribution credit in squash merges? or maybe github doesn’t allow coauthorship for people without certain permissions?

I think there were a few contributors to Data.List.Basic who got left out of coauthorship…it’s just a green square, but it would have been nice :)

Reid Barton (Jan 05 2023 at 21:32):

maybe bors only looks at the first 100 commits or something

Thomas Murrills (Jan 05 2023 at 21:36):

If so it has to be less…I was commit 43 apparently

Ruben Van de Velde (Jan 05 2023 at 21:42):

Doesn't seem like it: https://github.com/bors-ng/bors-ng/blob/771d1fe34884cae4ae889eb17c5b5da363508f45/lib/worker/batcher/message.ex#L171

Gabriel Ebner (Jan 05 2023 at 21:43):

The limit is 30:

$ curl -s https://api.github.com/repos/leanprover-community/mathlib4/pulls/966/commits | jq -r '.[].author.login'
rosborn
rosborn
rosborn
semorrison
ChrisHughes24
ChrisHughes24
ChrisHughes24
ChrisHughes24
ChrisHughes24
ChrisHughes24
ChrisHughes24
ChrisHughes24
ChrisHughes24
ChrisHughes24
ChrisHughes24
semorrison
semorrison
semorrison
semorrison
jcommelin
jcommelin
siddhartha-gadgil
siddhartha-gadgil
jcommelin
jcommelin
jcommelin
jcommelin
jcommelin
jcommelin
jcommelin

Gabriel Ebner (Jan 05 2023 at 21:44):

Richard wasn't mentioned because he's already the author of the merge commit:

Author: Chris Hughes <richardosborn@mac.com>

Ruben Van de Velde (Jan 05 2023 at 22:02):

That's because of pagination in the API, right? Does bors not take that into account?

Kevin Buzzard (Jan 05 2023 at 22:22):

Oh that's what the green squares mean?

Ruben Van de Velde (Jan 05 2023 at 22:29):

I'm assuming that's a reference to the activity graph on your github profile:
/user_uploads/3121/EsmSEly9nGERIgKsqQty51wJ/Screenshot-from-2023-01-05-23-28-40.png

Thomas Murrills (Jan 05 2023 at 22:42):

Yep—mine is, er, a bit sparser than that, so I was looking forward to the Data.List.Basic one as a little representation/record of the work I had done for it. I don't plan to stop contributing, though, so there'll be more to come soon :)

Thomas Murrills (Jan 05 2023 at 22:42):

Re: bors not taking pagination into account, I think that's here.

Last updated: Dec 20 2023 at 11:08 UTC