Zulip Chat Archive

Stream: general

Topic: Bors adding random co-authors

Moritz Doll (Mar 23 2022 at 21:36):

Bors seems to be very confused: https://github.com/leanprover-community/mathlib/commit/cd942870af69a837bde360337bee1a88eb1611c2

Yaël Dillies (Mar 23 2022 at 21:37):

Have a look at the commit history. @Jujian Zhang must have merged master not cleanly.

Eric Wieser (Mar 23 2022 at 21:38):

Looks like they rebased or merged backwards

Eric Wieser (Mar 23 2022 at 21:38):

A normal merge wouldn't do that

Moritz Doll (Mar 23 2022 at 21:39):

but shouldn't Bors just take the message body of the PR as the commit message no matter what happened in the PR?

Jujian Zhang (Mar 23 2022 at 21:41):

Haha, I am very sorry about this; I think I made a wrong commit somewhere in the timeline. And reverted a commit then merged origin/master again.

Moritz Doll (Mar 23 2022 at 21:45):

don't worry. I was more surprised about what Bors did and I didn't see the full commit history. Seems to be related to https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Co-authored-by

Eric Wieser (Mar 23 2022 at 22:00):

Moritz Doll said:

but shouldn't Bors just take the message body of the PR as the commit message no matter what happened in the PR?

Perhaps that should be an option, but right now the logic is:

  • Take the name of the main committer from the author who made the PR on github
  • Take the email address from the first commit in the PR
  • Assemble a list of co-authored-by entries from all the other commits in the PR

Eric Wieser (Mar 23 2022 at 22:00):

Note that step two is dangerous, as sometimes this isn't the same person as the one submitting the PR!

Yaël Dillies (Mar 23 2022 at 22:01):

Typically, #12746 (although I don't mind)

Eric Wieser (Mar 24 2022 at 10:02):

Maybe we should have a bot that detects that

Joachim Breitner (Mar 25 2022 at 11:09):

Step three is also dangerous, especially together with squash merges to master: depending on your git workflow, if you need to juggle a DAG of dependent PRs, the commits from dependent-upon PR appear as it they are also on the final PR (even if the actual changes from these commits are already in master - git won't know). Not horrible to give credit where no credit is due, but still a bit annoying. Hard to fix, though, without disabling that feature completely.

Moritz Doll (Mar 25 2022 at 11:14):

I think having the option to disable automatic addition of coauthors would be the best (and then disabling it for mathlib). It is not hard to add a line "Coauthored-by: .." in the PR body.

Eric Wieser (Mar 25 2022 at 13:04):

It's somewhat hard, as you have to find the user's email address (which is why bors struggles in some cases)

Last updated: Dec 20 2023 at 11:08 UTC