Github actions

Stream: mathlib4

[Heather Macbeth]

Could we move the Github actions for the merge-conflict label (and similar, e.g. blocked-by-other-PR) from semorrison to leanprover-community-bot? I have found it a little confusing in conversations featuring both Scott-the-person and Scott-the-bot. (Eg mathlib4#856)

[Scott Morrison]

Yes, I asked about this when I set it up, but no one seemed to know which account I should be creating the relevant tokens from. :-)

[Heather Macbeth]

So secret that nobody knows who knows it :)

[Scott Morrison]

I think it's just a matter of:

• decide which account should be associated with adding these labels
• find out how to login to it
• create new access tokens
• have an admin add these to the github secrets on the mathlib4 repo

[Eric Wieser]

I assume it was a deliberate choice (motivated by quota limits?) to not use the default "GitHub actions" user token

[Heather Macbeth]

Is that the same as leanprover-community-bot or different? There's also leanprover-community-bot-helper if the quota limits rules out leanprover-community-bot, right?

[Jagadish Bapanapally]

(deleted)