permission to push to non-main branches

Stream: batteries

[Heather Macbeth]

Can I please have permission to create a branch of Std? I'm trying to carry out the instructions for adapting to a breaking change in a core PR (namely lean4#3127):

When changes are required to Std to adapt to a breaking change in Lean, you will need to make a branch, and later open a PR from that branch.

• If the change was made in leanprover/lean4#NNNN, then the Std adaptation branch should be called lean-pr-testing-NNNN.
• The Std adaptation branch should be based off the branch nightly-testing-YYYY-MM-DD where YYYY-MM-DD is the date of the nightly release that your Lean PR is based off.
• Ideally you will push the lean-pr-testing-NNNN branch to the main Std repository; we can provide write access if needed.

[Mario Carneiro]

hm, I'm not so sure about those instructions, push access to std is maintainer only

[Heather Macbeth]

OK, should I create the branch on my fork and a maintainer can move it to the main repo? (Is that possible?)

[Mario Carneiro]

yes

[Mario Carneiro]

you can't move branches per se but you can create a branch pointing to a commit from a fork

[Heather Macbeth]

Thanks, the branch is https://github.com/hrmacbeth/std4/tree/lean-pr-testing-3127

[Heather Macbeth]

(based off nightly-testing-2023-12-29)

[Kim Morrison]

What shall we do here? Shall I just change the instructions advising people to create this branch in their own fork?

[Kim Morrison]

The alternative would be to advise that + asking a Std maintainer to then create the branch on the main repo.

[Mario Carneiro]

Well I'm not clear on what exactly needs to happen, what the bot is doing that needs this

[Kim Morrison]

There is no bot interaction on std at present.

[Kim Morrison]

(because it has historically been rarer to break Std than Mathlib)

[Mario Carneiro]

so it doesn't matter what branches are created then, except for our own sanity?

[Kim Morrison]

I can turn on such a bot if desirable, of course.

[Kim Morrison]

Yes, this is only for the sake of having uniform names for related things.

[Mario Carneiro]

I would prefer that it is possible for non-trusted things to be done outside the repo

[Mario Carneiro]

maybe you can tell the bot to look at a fork via a comment?