what to do?

Stream: nightly-testing

[Jon Eugster]

I've tried to read the documentation about lean-pr-testing-... branches, and I'm massively confused. Could I please get some instructions on whether I'm doing this right?

So there is Lean PR lean4#5173 and I've pushed a commit with fixes to the mathlib branch lean-pr-testing-5173.. and now what?

Is it correct that I've created mathlib PR #16157 which goes bump/v4.12.0 <-- lean-pr-testing-5173?

[Ruben Van de Velde]

I think we need to merge lean-pr-testing-#### into nightly-testing first

[Ruben Van de Velde]

I think you can change the target branch of your pr

[Jon Eugster]

ok. and do I do that now or after the PR is merged in core?
What confused me is that it says nightly-testing <-- lean-pr-testing-5173 "can be done anytime", but I guess I'll just make the PR and then wait for somebody of yous to use that when the time is right.

[Ruben Van de Velde]

Yeah, make the PR to nightly-testing, and then when the nightly with your changes is released, a bot will bump the version on the nightly-testing branch, which will fail - at that point, we can merge your PR

[Kim Morrison]

The essential step for contributors is to get a builds-mathlib label on their lean PR.

[Kim Morrison]

The steps for that are:

• Make sure your lean PR is branched of nightly-with-mathlib (rebase it if not).
• If you get a breaks-mathlib, then you'll need to push changes to the Mathlib branch lean-pr-testing-NNNN branch until it's fixed
• If the breakage is in Batteries, then PR to that same name branch there (and ping me so I can merge quickly), but then also on the Mathlib branch update the lakefiles to point Batteries at that branch, and run lake update batteries