Co-authored-by: finding emails

Stream: mathlib4

[Thomas Murrills]

Currently my best bet for when I need to manually add Co-authored-by is searching for Co-authored-by: <Name> on the zulip, and hoping that the coauthor has already coauthored at least one commit to mathlib, and thus has had their email appear in the rss feed. :) Surely there's a better way?

(Aside: if not, I wish we could write simply Co-authored-by: @<github-username> on the PR, and have it automatically translated by bors on the mathlib commit!)

[Snir Broshi]

I do git log | grep ..., it also finds the main authors of commits
You can also search for one of their PRs

[Ruben Van de Velde]

Or git log --author

[Julian Berman]

Thomas Murrills said:

(Aside: if not, I wish we could write simply Co-authored-by: @<github-username> on the PR, and have it automatically translated by bors on the mathlib commit!)

Some Johan person once asked for that feature it looks like -- https://github.com/bors-ng/bors-ng/issues/1041#issue-713538562

[Julian Berman]

Oh look, and there's a hynek post about it, with a tool linked that you can use: https://hynek.me/til/easier-crediting-contributors-github/

[Bryan Gin-ge Chen]

Addressing Johan's issue is on my list for bors -- the pieces are there (we're already using the numeric id+username@noreply email when we add coauthors from commits on the branch before it gets squashed) but they haven't been put together yet. (PRs welcome at https://github.com/leanprover-community/bors-ng !)