bot access

Stream: batteries

[Kim Morrison]

I would like to start having Lean CI automatically create the lean-pr-testing-NNNN branches at Std, like it already does at Mathlib.

To do so we need a bot that has write access at Std, with a token available in Lean CI.

I think an acceptable solution would be to make sure that leanprover-community-mathlib4-bot has write access at Std. (It's possible it already does.)

Could @Mario Carneiro or @Joe Hendrix either give that bot permission, or suggest an alternative?

I'll update our records of bots and tokens to reflect this permission after it is done.

[Kim Morrison]

lean#3200 is the PR that will make this change

[Mario Carneiro]

lean4#3200 I guess

[Kim Morrison]

My PR std4#547 seems to be breaking things on nightly-testing and #9960, so I am reverting it in std4#559, and as soon as CI is green I'm going to merge it myself.

I'm about to leave for a long weekend, and without reverting this there's no change to get nightly-testing and bump/v4.6.0 back on track before I leave.