Co-authored-by

Stream: general

[Joachim Breitner]

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]

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]

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

[Joachim Breitner]

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]

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]

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]

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

[Eric Rodriguez]

for reference: image.png

[Kyle Miller]

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

[Bryan Gin-ge Chen]

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]

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]

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