maintainer merge

Stream: mathlib4

[Kevin Buzzard]

Do we have maintainer merge for mathlib4? If not, is it reasonable to just post directly in the (private) reviewer maintainer merge thread?

[Heather Macbeth]

We really need to get that set up ...

[Adam Topaz]

It should be relatively easy, I think it’s just a matter of copying the right yml file to mathlib4

[Adam Topaz]

Well, that plus setting up the right secrets for Zulip

[Eric Wieser]

Privately posting sounds fine as an interim solution

[Alex J. Best]

Adam Topaz said:

It should be relatively easy, I think it’s just a matter of copying the right yml file to mathlib4

The action is already there and as far as i can tell there is nothing wrong with it. But it seems that there is no key set up to give the action permission to post (it gives access denied whenever anyone tries to invoke it). This seems very strange to me but I can't see what the secrets look like on mathlib4 :man_shrugging:

[Scott Morrison]

If someone wants to merge !4#3992, I think it should work.

[Scott Morrison]

It was using a bot github-bot managed by @Johan Commelin, and I have changed it to a different bot github-mathlib4-bot which I have access to, and updated the secret with the relevant API key.

[Johan Commelin]

Thanks! I kicked it on the queue

[Eric Wieser]

@Johan Commelin, you managed to claim https://github.com/github-bot? I'm surprised that username wasn't already in use!

[Johan Commelin]

Did I? I thought this was only some name on zulip?

[Eric Wieser]

Whoops, I confused zulip and GitHub bot accounts