co-authored-by bors issue

Stream: mathlib4

[Lua Viana Reis]

It seems that Co-authored-by: lines in the main PR text are not being placed in the right spot in the commits created by bors :frustration: either that, or I'm missing something about how this works in GitHub?

The context is the following merged PRs which have me as coauthor: #26853 #26852 #26807

as you can see Oliver did write the "Co-authored-by" line, but the commits pushed to master do not show me as coauthor (like, nicely with the two profile pictures in the interface :upside_down:). It seems to be working for other PRs when the coauthor sends some message in the PR thread like a review

[Ruben Van de Velde]

That's odd, because it does seem to be in the right spot on the commit: https://github.com/leanprover-community/mathlib4/commit/737d0422c5185dd0fa7f37adbf178b493b037099

[Ruben Van de Velde]

I hope it's not github being weird about the number of empty lines

[Bryan Gin-ge Chen]

Is the email shown there the same as your email in GitHub?

[Lua Viana Reis]

I saw that, and I double checked that my email is verified (in fact, it's the one shown in my profile there)

[Bryan Gin-ge Chen]

Here's GitHub's help page on the co-authored lines. They do warn against putting in blank lines, though they don't explicitly say that that will cause some coauthors to be dropped:

If you're adding multiple co-authors, give each co-author their own line and Co-authored-by: commit trailer. Do not add blank lines between each co-author line.

[Lua Viana Reis]

Ruben Van de Velde said:

I hope it's not github being weird about the number of empty lines

it's very odd, because this one https://github.com/leanprover-community/mathlib4/commit/bca1e1d88a213e8d3ee33b1742f136dc232659cc looks no different from https://github.com/leanprover-community/mathlib4/commit/2a234c6631d737f8d8ab5886b9599016c97d1b62 and yet it doesn't work

[Bryan Gin-ge Chen]

That is indeed strange. I can't think of anything else. Maybe you can try GitHub's "noreply" email next time just in case there's still some issue with the email?

Otherwise I would try writing to GitHub support - it may take a few weeks for them to respond though.

[Lua Viana Reis]

@Ruben Van de Velde one possibility: git show -s --format=%B bca1e1d88 locally shows that in Oliver's commit, there are a lot of trailing whitespace, and in the one that works, there is just one newline at the end

[Lua Viana Reis]

image.png

[Lua Viana Reis]

this may be it

[Lua Viana Reis]

the other commits that don't work also have a lot of whitespace before other "co-authored-by" automatically inserted by bors

[Bryan Gin-ge Chen]

bors is supposed to take everything above the --- in the PR comment and turn it into the commit message. It looks like there are only two newlines before --- in #26848 though, so it's possible there's something wrong with that functionality. I guess you could also try deleting --- and everything below in the PR comment next time, maybe that will make a difference?

Unfortunately bors itself is no longer under development, so if there is some bug, we may have to figure out how to fix it ourselves in our fork.

[Lua Viana Reis]

perhaps bors could be made to strip the whitespace, but it still can insert some "Used by: #26810" after the coauthored line and I'm not sure if this also breaks it oops, sorry, it was Oliver who wrote this line

[Lua Viana Reis]

Ok, it seems that stripping the whitespace could be a solution then. If I find how to do it, perhaps I can send a pr to bors-ng?

[Lua Viana Reis]

well, I'm not sure if this bothers me to the point that it prompts me to install elixir and fix it

[Lua Viana Reis]

I will ask oliver to create some empty commit with me as author next time instead of using the PR text. but mathlib's PR instructions should be updated because what it instructs does not work

https://raw.githubusercontent.com/leanprover-community/mathlib4/refs/heads/master/.github/PULL_REQUEST_TEMPLATE.md

[Bryan Gin-ge Chen]

I did some digging in mathlib4's commits and it looks like the issue has been with us since at least 2022: cf. #237 and associated commit. This also proves that my various suggestions above are wrong -- to fix this we will unfortunately need to look more closely at what bors is doing.

[Lua Viana Reis]

Would it help if meanwhile the template instructed to add an empty commit instead of using the commit message? like this:

- To indicate co-authors, include lines at the bottom of the commit message
- (that is, before the `---`) using the following format:

- Co-authored-by: Author Name <author@email.com>

+ To indicate co-authors, include at least one commit authored by each co-author
+ among the commits in the pull request. If necessary, create empty commits to
+ indicate co-authorship, like so:

+ git commit --author="Author Name <author@email.com>" --allow-empty -m "add Author Name as coauthor"

+ When merging, all the commits will be squashed into a single commit listing all co-authors.

[Lua Viana Reis]

relevant bors-ng source:

https://github.com/robertylewis/bors-ng/blob/7c57469b9d8588cb3bb3d53c1d7a76057b7f8107/lib/worker/batcher/message.ex#L195-L200

[Bryan Gin-ge Chen]

Sure, feel free to open a PR to the pull request template and I'll merge it.

[Lua Viana Reis]

@Bryan Gin-ge Chen: #27618

[Eric Wieser]

Did we determine if GitHub is behaving to-spec by ignoring these trailers in the presence of whitespace?

[Bryan Gin-ge Chen]

I don't know that there's a spec, but GitHub's help page doesn't say anything about empty lines after the "Co-authored-by" lines. Lua's commits and the example from #237 seem to show that GitHub won't show the icon if extra lines are present though.

[Lua Viana Reis]

From what I could find there is no official Git spec for the Co-authored-by, it seems to be a convention made by GitHub

[Michael Rothgang]

It would be easy to have CI check that a PR description has the right form. Can somebody summarise for me what the exact requirements are, then I can try to write one.

[Michael Rothgang]

(If you want to write that check yourself, be my guest - I'm also happy to review that!)

[Oliver Butterley]

Michael Rothgang said:

It would be easy to have CI check that a PR description has the right form.

In the context of coauthors, the issue is that bors doesn't take notice of coauthors listed in the commit message, as seen in the code linked above, coauthors are sourced from the commits and then listed in the new commit message.

[Oliver Butterley]

If there is a CI check for PR description, this is an issue that I encountered previously:
- [ ] depends on: works but * [ ] depends on: doesn't work even thought both display identically in markdown (and so took a while for me to figure out the issue).

[Ruben Van de Velde]

Oliver Butterley said:

Michael Rothgang said:

It would be easy to have CI check that a PR description has the right form.

In the context of coauthors, the issue is that bors doesn't take notice of coauthors listed in the commit message, as seen in the code linked above, coauthors are sourced from the commits and then listed in the new commit message.

No, that's not the issue here. The Co-authored-by lines were in the PR description, and did end up in the final commit message, but github is ignoring them

[Bryan Gin-ge Chen]

I've just deployed a potential fix for this issue in our fork of bors. Here's the relevant code, which should strip out all the unnecessary extra empty lines that were confusing GitHub:

https://github.com/robertylewis/bors-ng/blob/6ddf68711c86c2e33e8c5daaedd024527ba5bf5b/lib/worker/batcher/message.ex#L201-L208

(See also test case).

Thanks @Lua Viana Reis for the report and for tracking down the broken function in the source!

[Bryan Gin-ge Chen]

I've opened #31030 adding back the instructions for adding co-authors via "Co-authored-by" lines in the PR message.