bors changed base branch

Stream: mathlib4

[Rémy Degenne]

On PR #6098, the base branch got changed, apparently by bors. I got the message "bors changed the base branch from master to ScottCarnahan/BinomialRing2" 4 hours ago. Does anyone understand what happened here?
I don't want to merge into that random branch. How do I switch it back to master?

[Rémy Degenne]

It looks like the same happened to all PRs numbered 7078 or below

[Bolton Bailey]

Came here to ask the same thing

[Sebastien Gouezel]

Would this be related to #7215?

[Scott Morrison]

Eek!

[Scott Morrison]

If you click "edit" on the title you can change the base branch baack.

[Thomas Murrills]

Looking at the reference for bors, the only thing that seems related is this:

update_base_for_deletes
If turned on, and if delete_merged_branches is also turned on, then when a pull request is merged and its base branch is about to be deleted, any other pull requests made against the base branch will be fixed up.

And indeed, we have update_base_for_deletes = true in bors.toml. Maybe bors thought that merging master into ScottCarnahan/BinomialRing2 in #7215 meant that master was going to be deleted, and so...updated every PR made against master? Why the cutoff at 7078, though, I wonder... But I don't know anything about bors, so!

[Scott Morrison]

But obviously this shouldn't have happened.

[Thomas Murrills]

Ah, Scott is here, and they know about bors! (Or at least more than I do. I'm not sure exactly who wrangles bors.) I'll leave it to you. :)

[Eric Wieser]

This looks like a bors bug to me

[Eric Wieser]

There are 217 PRs which now have the wrong base

[Eric Wieser]

(which is to say, we should be very careful not to merge any of them until that is fixed)

[Eric Wieser]

I wonder if there's some way we can trick bors into switching them back

[Eric Wieser]

I think our options are:

• Write a script to set all the base branches back again
• Change all 217 by hand
• Delete the branch so that all the PRs are closed, but I don't know it it will be easy to re-open them

[Scott Morrison]

GPT suggests:

#!/bin/bash

# Check if the 'gh' command is available
if ! command -v gh &> /dev/null; then
    echo "'gh' command not found. Please install GitHub CLI."
    exit 1
fi

# Fetch all open PRs with their numbers and base branch
PR_DETAILS=$(gh pr list --state open --limit 100 --json number,baseRefName --jq '[.[] | select(.baseRefName != "master")]')

# Iterate over each PR and update its base branch to 'master' if it's not already
for ROW in $(echo "${PR_DETAILS}" | jq -c '.[]'); do
    PR_NUMBER=$(echo $ROW | jq -r '.number')
    BASE_BRANCH=$(echo $ROW | jq -r '.baseRefName')

    if [ "$BASE_BRANCH" != "master" ]; then
        echo "Changing base branch of PR #$PR_NUMBER from $BASE_BRANCH to 'master'..."
        # gh pr edit $PR_NUMBER --base master
    fi
done

echo "Updated the base branches where needed!"

(I commented out the "live" step.)

[Scott Morrison]

Might run into pagination issues with the --limit 100.

[Scott Morrison]

Happy to test it on a few by hand and then let it rip?

[Eric Wieser]

You should only change PRs that target the bad branch

[Eric Wieser]

Some other PRs might genuinely target non-master

[Scott Morrison]

I'll just do that via checking the dry runs first.

[Scott Morrison]

Rather than writing extra code that may not be necessary.

[Scott Morrison]

The initial dry-run says this is the only non-master target branch.

[Eric Wieser]

The "Extra code" is replacing != "master" with == "ScottCarnahan/BinomialRing2"

[Scott Morrison]

Also -S '-base:master'

[Eric Wieser]

I think the last one alone is enough

[Scott Morrison]

nope

[Eric Wieser]

Aren't you filtering twice?

[Scott Morrison]

That doesn't filter the results before the 100 result limit, only after.

[Eric Wieser]

Well, that doens't really matter

[Scott Morrison]

Well, it does, because then you get 0 results, even though there are more to do.

[Scott Morrison]

Once the top 100 PRs are all pointing at master

[Eric Wieser]

Ah, because you're not iterating the API within the script, just re-running it

[Eric Wieser]

Scott Morrison said:

The initial dry-run says this is the only non-master target branch.

This is only for the first 100, right?

[Scott Morrison]

The gh cli doesn't have pagination controls. You just get the first --limit.

[Scott Morrison]

All done. For reference, two (three?) runs of:

#!/bin/bash

# Check if the 'gh' command is available
if ! command -v gh &> /dev/null; then
    echo "'gh' command not found. Please install GitHub CLI."
    exit 1
fi

# Fetch all open PRs with their numbers and base branch
PR_DETAILS=$(gh pr list -S '-base:master' --state open --limit 100 --json number,baseRefName --jq '[.[] | select(.baseRefName == "ScottCarnahan/BinomialRing2" )]')

# Iterate over each PR and update its base branch to 'master' if it's not already
for ROW in $(echo "${PR_DETAILS}" | jq -c '.[]'); do
    PR_NUMBER=$(echo $ROW | jq -r '.number')
    BASE_BRANCH=$(echo $ROW | jq -r '.baseRefName')

    if [ "$BASE_BRANCH" == "ScottCarnahan/BinomialRing2" ]; then
        echo "Changing base branch of PR #$PR_NUMBER from $BASE_BRANCH to 'master'..."
        gh pr edit $PR_NUMBER --base master
    fi
done

echo "Updated the base branches where needed!"

[Scott Morrison]

Your 217 PRs links above now returns 2!

[Eric Wieser]

Great, thanks!

[Eric Wieser]

I made a patch to bors at https://github.com/bors-ng/bors-ng/pull/1715 that should hopefully stop this happening again, but I doubt it will be merged

[Eric Wieser]

I guess it's not a big deal if it happens again now that we have this script to hand; thanks!

[Sky Wilshaw]

Does mathlib plan to migrate to the GitHub merge queue?

[Scott Morrison]

Yes, we've talked about it. The biggest problem is just setting up the constraints so that only maintainers can give final approval for merging.

[Scott Morrison]

When I looked at it I couldn't work out how to do that.

[Scott Morrison]

Well, I could, but it required additional CI automation.

[Scott Morrison]

A step that checks for a comment written by someone on a whitelist.

[Eric Wieser]

I thought the problem was the opposite, and we couldn't work out how to delegate so that non-maintainers could trigger the final merge?

[Scott Morrison]

But as far as I could see the absence of that step was going to put a red x on the status of the PR, which I'd really prefer to avoid!

[Scott Morrison]

Oh, I hadn't even got as far as thinking about delegating.

[Eric Wieser]

I don't see why we need anything special for a delegation-free workflow

[Eric Wieser]

Surely only maintainers can hit the merge button anyway?

[Scott Morrison]

The documentation leaves something to be desired, so I think we need to set up a practice repo. My reading of the docs was that maintainers were not special.

[Scott Morrison]

The only criteria for merging were "passes CI checks" and "has at least k approvals" (and possibly something about approvals from a CODEOWNER).

[Mauricio Collares]

What about the alternate proposal to switch back to Mergify? It has improved a lot since Mathlib migrated away from it in 2021.

[Sky Wilshaw]

Their free tier seems limited to 100 PRs per month - I haven't checked but I feel like it'd be easy to hit that on a repo as big as mathlib.

[Joachim Breitner]

We could ask them if they would be interested in having us as a non-payment customer. I found them quite responsive usually when I managed the mergify setup for another project. Also happy to lend a hand setting it up if there is need for that.

[Eric Wieser]

Eric Wieser said:

I made a patch to bors at https://github.com/bors-ng/bors-ng/pull/1715 that should hopefully stop this happening again, but I doubt it will be merged

This was merged!

[Joachim Breitner]

The bors repo is using Github’s merge queue feature :shocked:

[Scott Morrison]

Eating their own dog food: https://bors.tech/newsletter/2023/05/01/tmib-76/

[Scott Carnahan]

Sorry about blowing everything up!