Zulip Chat Archive

Stream: general

Topic: Co-authored-by


Joachim Breitner (Mar 16 2022 at 13:50):

Did bors get smarter about Co-Authored-by headers? I added them manually as advised in the PR template, but now we have

commit 717b11ecf5807c48409375806e38ca13ee2a356e
Author: Joachim Breitner <mail@joachim-breitner.de>
Date:   Wed Mar 16 11:53:35 2022 +0000

    feat(group_theory/noncomm_pi_coprod): homomorphism from pi monoids or groups (#11744)

    Co-authored-by: Junyan Xu <junyanxumath@gmail.com>



    Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

Yakov Pechersky (Mar 16 2022 at 13:52):

If you used the github UI to commit a suggestion that someone else provided, not editing it, then it already knows:
image.png

Yakov Pechersky (Mar 16 2022 at 13:53):

And if they make commits explicitly, also:
image.png

Joachim Breitner (Mar 16 2022 at 13:55):

Right, that’s the non-squashed commits on the PR, and if we’d use Github’s merge, I see how that would work. But bors creates a squashed commit from the branch, and takes the commit description from the PR title, so I am somewhat (positively) surprised to see it automatically added.

Joachim Breitner (Mar 16 2022 at 13:56):

Maybe the template in
https://github.com/leanprover-community/mathlib/blob/master/.github/PULL_REQUEST_TEMPLATE.md?plain=1#L8-L11
should indicate that this is not needed when co-authors are known to git.
Or better, bors should deduplicate the list of co-authors.
Or we just don’t worry :-)

Gabriel Ebner (Mar 16 2022 at 16:23):

bors only appends the author names, it doesn't look at the PR body at all.
https://github.com/bors-ng/bors-ng/blob/a779f47b2dc8865e5c94d46fc0097b675754cca5/lib/worker/batcher/message.ex#L157-L168

Gabriel Ebner (Mar 16 2022 at 16:24):

There's also a weird bug where bors mixes up the email address and name of the author.

Eric Rodriguez (Mar 16 2022 at 16:25):

for reference: image.png

Kyle Miller (Mar 16 2022 at 16:26):

I didn't realize @Eric Wieser was a collective pseudonym

Bryan Gin-ge Chen (Mar 16 2022 at 16:28):

I'm not sure if it's bors or github, but I believe that can happen when someone opens a PR from a branch where they didn't author the first commit.

Gabriel Ebner (Mar 16 2022 at 16:30):

https://github.com/bors-ng/bors-ng/blob/f1e8251afbc3acf425c4db98734ae0b6b7893d08/lib/worker/batcher.ex#L488-L495

# If a user doesn't have a public email address in their GH profile
# then get the email from the first commit to the PR

Eric Wieser (Mar 16 2022 at 23:11):

https://github.com/bors-ng/bors-ng/issues/1393


Last updated: Aug 03 2023 at 10:10 UTC