mathlib4 bot

Stream: mathlib4

[Jon Eugster]

Currently the bot doing all the labels on github runs under @Scott Morrison's name semorrison. Would it be trivial to change that to a different name? obvsly does not really matter but I think it is somewhat confusing. In mathlib3 it used to be a "github-actions (bot)".

[Scott Morrison]

Sorry yes, I really need to get on to this. Consider it bumped.

[Scott Morrison]

That problem is that we were running out of bot accounts, and there is a certain overhead to making more (including making the email accounts associated with them, tracking the passwords and tokens, etc, and we already have a backlog on managing this properly).

[Eric Wieser]

And presumably the reason we need lots of bot accounts is due to hitting quota limits from a single account

[Eric Wieser]

Something like https://github.com/marketplace/actions/github-app-token might be a solution

[Alex J. Best]

I think you can make numerous additional github accounts using one gmail address by using the + trick (https://support.cloudhq.net/how-to-setup-gmail-aliases/). Essentially myname@gmail.com and myname+github2@gmail.com are different email addresses from github's perspective that forward to the first address only with gmail (the second one incoming emails are automatically labelled with github2)

[Eric Wieser]

We still have to manage passwords and tokens for all those accounts, but I agree that avoids spawning email addresses

[Scott Morrison]

Use the +XXX trick has limitations; I have tried this and run into problems with Github flagging accounts. Still working on solutions here.