bors going away?

Stream: general

[Mario Carneiro]

@bors said:

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Lint style

[Bryan Gin-ge Chen]

GitHub's merge queue feature looks promising. Has anyone tried it out?

[Ruben Van de Velde]

See https://bors.tech/newsletter/2023/05/01/tmib-76/

[Yaël Dillies]

:sad:

[Mauricio Collares]

Bryan Gin-ge Chen said:

GitHub's merge queue feature looks promising. Has anyone tried it out?

I think this is the natural option, but I don't know if it does batching (and binary searching to resolve build conflicts) or if it just serializes the merging/CI steps.

[Ruben Van de Velde]

It doesn't seem to support batching or prioritization

[Yaël Dillies]

That's pretty poor...

[Mauricio Collares]

I searched some more and I found https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/configuring-pull-request-merges/managing-a-merge-queue, which says stuff like "Merge limits: Select the minimum and maximum number of pull requests to merge in a single group (between 1 and 100), and a timeout after which the queue should stop waiting for more entries and merge with fewer than the minimum number of pull requests."

[Mauricio Collares]

And this implies a "Jump queue" (i.e., move to front) exists too, which is good.

[Scott Morrison]

It seems pretty hard to work out from their documentation how it actually works. (e.g. what it does about batching, what happens when something fails mid-queue).

[Scott Morrison]

We could just turn it on for the mathlib4 repository for a bit, see how it goes, and if it doesn't work out fall back to hosting our own bors.

[Eric Wieser]

Or make a mathlib-test fork and ask people to create some garbage PRs (that modify comments in early files to make builds slow) just to see what happens

[Matthew Ballard]

Ruben Van de Velde said:

See https://bors.tech/newsletter/2023/05/01/tmib-76/

So bors itself is deprecated?

[Scott Morrison]

Yes. :-(

[James Gallicchio]

can a majority of mathlib PRs be grouped in some reasonable fashion based on which part of the library they mainly touch? e.g. lots of PRs only touch stuff in Algebra or only touch stuff in CategoryTheory?

a technique I've seen before to reduce merge queue pressure on master in mono-repos is to have non-master branches that accumulate multiple PRs before being merged into master all together. e.g. you have an algebra branch that all mostly-algebra PRs target, and then once a day (maybe more often) you merge that branch into master.

it's somewhat better than trying to automatically batch PRs, because you can work out all the merge conflicts in all the algebra PRs before the changes even reach master.

[Ruben Van de Velde]

Personally, I'm not sure that that is something that would be helpful at this point

[Mauricio Collares]

https://github.blog/2023-07-12-github-merge-queue-is-generally-available/

[Yury G. Kudryashov]

Should we try it?

[Eric Wieser]

Should we try it on something with lower traffic like Std4 first? I think using it on mathlib3 just before the freeze would be needless pain, and there are probably more people working on Mathlib4 than Std4 [citation needed]

[Yury G. Kudryashov]

@Mario Carneiro :up:?

[Alex J. Best]

Trying it on something low traffic seems to defeat the purpose really though, testing it a bit on a fork might be good though so maintainers can learn how it works

[Yury G. Kudryashov]

Anyway, it's up to the CI team to decide. @Bryan Gin-ge Chen @Gabriel Ebner @Eric Wieser @Johan Commelin @Wojciech Nawrocki :up:

[Eric Wieser]

Note that Std4 is not in the leanprover-community organization, so I suspect only @Gabriel Ebner from that list has the power to enact such a decision.

[Yury G. Kudryashov]

CI team can decide to try it on some other repo (website, docs).
P.S.: I stop replying in this thread because I feel like I'm trespassing into the CI team territory.

[Johan Commelin]

Yury, I don't think you have to worry about that. Everybody can offer suggestions.

[Scott Morrison]

Test in production on Mathlib! :-)

[Yury G. Kudryashov]

That's an option too (at least if it's easy to reverse the decision).

[Scott Morrison]

I think the biggest problem is:

Once a pull request has passed all required branch protection checks, a user with write access to the repository can add the pull request to the queue.

This seems incompatible with our setup in which we give write access to all contributors.

[Scott Morrison]

We could try to just establish the social expectation that only maintainers actually merge, but I think we will see too many mistakes to be comfortable with this.

[Scott Morrison]

I think we should assume that this situation (anyone with write access can add to the merge queue) is here to stay. That means our options are:

• remove write access from non-maintainers, by working out how to do CI from forks (like everyone else in the universe)
• not use github's merge queue (which will mean running our own bors instance)

[Scott Morrison]

The obstacles for CI from forks seem to be:

• inability to push oleans into the shared cache
• inability to use Hoskinson Center CI runners (although I'm not sure these are even running mathlib4 actions at present!)

[Yury G. Kudryashov]

I think that each user won't run out of their amount of free hours of CI, so the latter is not a problem.

[Yury G. Kudryashov]

But we need some solution for oleans.

[Scott Morrison]

The Hoskinson runners are faster than github, and it would be nice to take advantage of this.

[Yury G. Kudryashov]

It only matters if someone makes a big refactor or modifies a file deep in the import heirarchy.

[Yury G. Kudryashov]

But I can't think of a way to deal with oleans.

[Yury G. Kudryashov]

We can have a central storage for the main branch, then each clone oleans as github artifacts. Can we?

[Yury G. Kudryashov]

And how can we help users not run out of space?

[Yury G. Kudryashov]

(lake exe cache get can try the central storage and user-specific storages)

[Yury G. Kudryashov]

Another option: each contributor gets a login+password for the storage. oleans from each user are stored in login/shasum.extension. lake exe cache get has a configurable list of users that one trusts.

[Yury G. Kudryashov]

BTW, what are the current monthly stats for the storage?

[James Gallicchio]

what is the shared cache used for currently? if it's just for speeding up subsequent CI runs, I think GH has a way for CI to cache files directly, which could be set up in each contributor's fork

[Yury G. Kudryashov]

I can git checkout some-branch; lake exe cache get and have oleans for that branch.

[James Gallicchio]

ahh. yeah. maybe this is the incentive to build a centralized package repository with olean caching. but that's a lot of work compared to hosting a bors instance :big_smile:

[Sebastian Ullrich]

Also relevant: https://matklad.github.io/2023/06/18/GitHub-merge-queue.html

[Johan Commelin]

Wow, if those criticisms are right, then I really think we should self-host bors

[Anne Baanen]

Delegation is such an important feature for how I use bors that its absence is sufficient reason for me to self-host bors.

[Johan Commelin]

Yes, and the latency aspect as well

[Johan Commelin]

human time >> machine time

[Sebastian Ullrich]

Even Bors the software being frozen is not a great sign but I agree that self-hosting it while watching for improvements to GH's implementation sounds like a reasonable strategy.
Relevant GH feature requests: https://github.com/orgs/community/discussions/14699 and (I think?) https://github.com/orgs/community/discussions/6865

[Jireh Loreaux]

Yeah, without delegation I think we should self-host Bors, not to mention some of the other headaches above.

[Matthew Ballard]

What happens when something breaks Bors? My understanding is that it is on the user to fix since the repo itself being archived.

[Matthew Ballard]

Scott Morrison said:

The obstacles for CI from forks seem to be:

• inability to push oleans into the shared cache
• inability to use Hoskinson Center CI runners (although I'm not sure these are even running mathlib4 actions at present!)

What makes it able to do these currently?

[Eric Wieser]

From forks, it's not able to do those currently

[Eric Wieser]

Unfortunately there is an element of security by obscurity here, which public discussion erodes

[Matthew Ballard]

Auth issues?

[Matthew Ballard]

Ah ok.

[Eric Wieser]

Github recommends that you do not allow private CI runners to be used on forks, which somewhat answers question 2.

[Eric Wieser]

Though it is technically possible

[Matthew Ballard]

Can't the current workflow be triggered on a pull request to master, the fork get pulled in, and everything run as it is now?

[Yury G. Kudryashov]

So that the runner ignores workflow setup in the fork?

[Joachim Breitner]

Is the question whether to replace bors, and with what?
I have used mergify in the past, and found it very nice, also compared to bors. They are also quite responsive, so if GitHub's built in features don't cut it, I expect they'll listen to our needs.

[Eric Wieser]

I think we used to use mergify; it's in some old mathlib3 PRs

[Mauricio Collares]

!3#2322

[Mauricio Collares]

Apparently mergify didn't do batching at the time (it got implemented in Q3 2021)

[Joachim Breitner]

Ah, I see :-). Yes, they have that feature now, including a refinement that they call merge trains (although I haven’t used that myself yet)

[Johan Commelin]

Does mergify have delegation? I think it didn't back in the day when mathlib used it.

[Joachim Breitner]

Not in the exact from that bors has it, I believe. Most of the time when something was delegated to me it was “merge once CI turned green”, which I found strange anyways (why tell a human to watch it when borgs/mergify/whatever can do that).
In other words, I wonder if “delegation” is really more useful than “merge when ready” where ready means something like “has approving reviews and the label automerge”. But likely I haven’t seen all the use-cases for delegation, and when it would mean something else than “I approve this PR”

[Matthew Ballard]

It looks like it can do label-based triggers. So you have some combination of maintainer approval and this to allow simulated delegation

[Eric Wieser]

Often delegation is used for "make some trivial docstring change, wait for CI, then merge"

[Johan Commelin]

delegation in the form of "merge when CI is green" is indeed pointing at failing tech, but the form of "please fix these minor issues, and kick it on some queue afterwards" seems like an excellent form of delegation

[Joachim Breitner]

In the project I used it with the rules was:

Merge when it has an approving review by a commiter, CI is green, and merge label is there.

So the action to indicate

"make some trivial docstring change, wait for CI, then merge"

would be to remove the merge label (if present) and approve.
Then the author can fix typo, add label, and is done. As soon as CI is green, it is merged.
In particular (and very crucial, I believe), noone has to manually wait for CI to finish

[Joachim Breitner]

It requires maintainers to remove the label if they want the author to give a chance to act again, but otherwise that use-case was covered nicely .

[Joachim Breitner]

Is it important that the delegation can be scoped to one particular user? Or is it ok if anybody can do the next step?

[Johan Commelin]

"approving review by a commiter", does that mean "maintainer"?

[Johan Commelin]

Note that on github, almost anyone can add labels. So the presence of the label should be thought of as a social flag, not a security flag.

[Joachim Breitner]

Yes, approving review by a maintainer. Or by an explicit github group.

[Joachim Breitner]

A few times there was some small annoyance because the delegation allowed the original PR author to merge, but someone else had taken over the PR since then. And almost anyone can sneak in a commit to someone else's branch …
Are we worried about people who have been added to the repo (only those can add labels, I think) playing not nice?
(If so, then label-based “merge if ready” indications don’t work well.)

[Johan Commelin]

I don't think we are too worried about that. If someone abuses trust, then we revert the commit too master and revoke write access for that person.

[Matthew Ballard]

Here are all the conditions available to use

[Joachim Breitner]

So so far it sounds as if mergify would be a viable option, should bors have to be shut down and should nothing better (e.g. github native) work for us.

[Joachim Breitner]

This is the config that I set up at a previous project. It worked well from a developer happiness point of view, but it was obviously a very differently sized project, and less open: https://github.com/dfinity/motoko/blob/master/.mergify.yml

[Joachim Breitner]

Now that a PR of mine just got merged, I am reminded of one thing that mergify might do better: merged PRs would actually appear as merged in GitHub, not closed

[Ruben Van de Velde]

Since we seem to be using the merge queue now, we should probably try to make it produce better commit messages

[Mauricio Collares]

I think the merge queue won't be used. Probably we will hear about the chosen alternative soon.

[Johan Commelin]

Yes, there has been a lot of experimenting and debugging yesterday. We hope to post an update soon!

[Eric Wieser]

The merge queue was unsuitable because it runs a build for every single commit, rather than just the latest commit in the batch

[Scott Morrison]

(It's not totally clear to me that this is actually a showstopper. It will certainly consume more CI than bors. But we do a lot of non-bors CI, and there may still be slack in the system.)

[Joachim Breitner]

If it’s just the squash merge commit message, Github now supports the sensible setting of using Github title + description. Probably it can’t stop at --- though. Mergify supports something along these lines (a ### commit message section).

[Eric Wieser]

If you look at #rss > Recent Commits to mathlib4:master , you can see we already used the title+description option for the last few messages

[Joachim Breitner]

Ok, sorry for the noise :-)

[Mauricio Collares]

Eric Wieser said:

The merge queue was unsuitable because it runs a build for every single commit, rather than just the latest commit in the batch

Wait, what? That would make it useless for everyone, not just mathlib. Could this be a problem with mathlib's ci setup?

[Eric Wieser]

The purpose of the github merge queue seems to be to ensure master never breaks, not to reduce CI load

[Mauricio Collares]

Mauricio Collares said:

I searched some more and I found https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/configuring-pull-request-merges/managing-a-merge-queue, which says stuff like "Merge limits: Select the minimum and maximum number of pull requests to merge in a single group (between 1 and 100), and a timeout after which the queue should stop waiting for more entries and merge with fewer than the minimum number of pull requests."

Is this relevant?

[Ruben Van de Velde]

https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/configuring-pull-request-merges/managing-a-merge-queue#successful-ci suggests that it waits for result from both [master, PR1] and [master, PR1, PR2] before merging PR1 and PR2 into master

[Eric Rodriguez]

Indeed, merge queue does not do batches + binary search like Bors

[Mauricio Collares]

It does not do binary search, but given that merge groups are a thing I'd be very surprised if (in a properly configured environment, which might be hard because documentation is basically non-existent) every commit of a group got tested separately.

[Eric Wieser]

It looks pretty clear from the GitHub documentation that CI runs on every commit in the group (after the history is merged / rebased to be linear)

[Mario Carneiro]

It sounds like you can set "Minimum pull requests to merge" and "Wait time" so that PRs queue up without CI running until either N PRs are ready or T time has passed. It says

You can specify a minimum group size, which is useful if merges to your base branch trigger a lengthy CI build or deploy process, and you don’t want to hold up the following entries in the queue.

which suggests that it is intended for our general use case

[Mario Carneiro]

also "Build concurrency" can be used to prevent it from eating all our runners

[Matthew Ballard]

Does it bisect at all?

[Mario Carneiro]

I see no evidence of bisection

[Mario Carneiro]

I think it just makes the queue go slower if you use the aforementioned throttling options

[Eric Wieser]

is useful if merges to your base branch trigger a lengthy CI build

this is merges to the base branch, not CI on the staging branch

[Eric Wieser]

This is too late to be useful; if we move our CI to only be on the base branch, then we can't guarantee master stays green any more

[Mauricio Collares]

Eric Wieser said:

It looks pretty clear from the GitHub documentation that CI runs on every commit in the group (after the history is merged / rebased to be linear)

I agree that the docs are very weird, and I am not claiming that the feature is helpful for us any longer. I'm just surprised someone at GitHub would think this version of merge_group is useful to anyone.

[Mario Carneiro]

it's not rocket science, why does everyone mess this up?

[Eric Wieser]

There's some discussion here, but I doubt it has much visibility

[Eric Wieser]

To be fair, github have succeeding in meeting the not-rocket-science rule

[Eric Wieser]

They've just done it in a way that costs more CI machines

[Ruben Van de Velde]

Arguably, running CI only on the batch is what breaks the not rocket science rule

[Eric Wieser]

Yes, depending on whether you split the hair of "repository of code" as "every commit" or "the HEAD at any point in time"

[Mario Carneiro]

I don't see how you could make every commit green unless you prevent people from pushing to the repo at all

[Eric Wieser]

Ok, I should have split that as "every commit accessible by following the first parents of HEAD"

[Mario Carneiro]

which is possible, if like graydon you keep a separate repository which is entirely maintained by robots and pulls stuff from the repo that people actually work on

[Eric Wieser]

It's also exactly what github merge queues achieve

[Mario Carneiro]

oh I see what you mean now, bors can merge commits which have not been tested but are ancestors of a tested commit

[Eric Wieser]

Yes exactly, and conceivably that could be a problem for some people; but it's not something we care about or are willing to increase our CI usage for

[Julian Berman]

"Every commit needs to work" may also be Gerrit-inspired.

[Eric Rodriguez]

Our current setup makes it harder to bisect bugs that get introduced in one big bors batch if it so happens that two PRs in that batch "interfere constructively"

[Eric Rodriguez]

But I feel like this is far less of an issue for our specific use than anyone elses' because it is very hard to write theorems that are genuinely bad/buggy; as opposed to code.

[Eric Rodriguez]

Eric Rodriguez said:

Our current setup makes it harder to bisect bugs that get introduced in one big bors batch if it so happens that two PRs in that batch "interfere constructively"

e.g. one changes a meta thing and the other one removes the tests for that meta thing

[Matthew Ballard]

Akin to Zeus who summoned two mighty warriors from their grave, @Rob Lewis has asked to rise from its grave to rescue mathlib. Congratulations and thanks!

[Mac Malone]

Julian Berman said:

"Every commit needs to work" may also be Gerrit-inspired.

It is also very useful for end-users who may wish to cherry-pick some subset of changes for there use-case (e.g., patching old software with newer security patches but without a full update to the newest release due to other restrictions). Being able to bisect effectively without false positive breakages is very valuable. Thus, I think what GitHub is doing here is a proper implementation of the "Not Rocket Science" rule. The fact that bors did not do this is actually surprising, as it violates the principle of monotonically increasing test coverage expressed in the article by Graydon (i.e., by an x-axis of commit # in the default branch, test coverage is not necessarily monotonically increasing).

[Eric Wieser]

That property is only true with the github merge queue if you squash merge though. If you create real merge commits, then it only enforces "the chain of first parents is always green"

[Eric Wieser]

Note that it's easy enough to bisect mathlib despite not every commit being tested; you just return the special exit code 125 from your bisection script if no cache is available

[Eric Rodriguez]

Sure, but that won't tell you what exact commit has issues, just the bors group - that is likely easy to figure out anyways, though.

[Mac Malone]

Eric Wieser said:

That property is only true with the github merge queue if you squash merge though. If you create real merge commits, then it only enforces "the chain of first parents is always green"

Yeah, I guess I was subconsciously assuming a linear history here as merge commits have nearly always been discouraged in the software projects I've dealt with heavily (outside of a few cases of semi-linear histories).

[Eric Wieser]

I guess you could argue that the bors batching ought to be reflected in the git history itself, which would restore the "every first parent is tested" property (maybe that counts as semilinear?).

[Mauricio Collares]

git bisect works perfectly with many merge commits since that's how Linux is developed

[Jireh Loreaux]

I think the actual performance gains of batching on busy days likley outweigh the potential drawbacks of failed bisection. I think the probability of the former occurring is rather low, especially if one follows Eric's regime first of only bisecting commits with a cache to winnow down the search. Then you can do normal bisection between the failing cached commit and the most recently cached commit.

In this way the probability of encountering a false positive bisection is limited to the probability of error in an individual commit in a bors batch of size at most n, where n is the max batch size between the working and failing commits.

[Joachim Breitner]

The performance gains are overall compute cost, but not actually merge latency, because the batch’s prefixes are tested in parallel, right?
(I’m wary of a workflow that does not test every first-parent commit on master for the reasons mentioned above already, but I understand that resources may be limited)

[Eric Wieser]

Merge latency is only unaffected if we never run out of compute

[Eric Wieser]

But we're very frequently using all the runners at busy times of day, so that's a bad assumption.

[Jireh Loreaux]

Moreover, we've had bors batches whose size exceeds the number of runners.

[Jireh Loreaux]

In addition, bors is relatively feature rich. If there were some commit against which we really wanted to ensure Mathlib builds, we could send it to bors with high priority to make sure it gets its own batch. Maybe this is worth doing for core or std bumps, but for many commits I think it really isn't that important.

[Ruben Van de Velde]

My understanding is that bors initially didn't have batching, but resource constraints made people do "rollup merges" manually until the feature was added to bors

[Joachim Breitner]

If you are looking for a feature rich replacement for bors, mergify might be an option. It does merge queues like GitHub, but is much more configurable (e.g. extracting commit messages from PR descriptions, and plenty of other PR-related automation, e.g. reacting to labels etc.)

[Jireh Loreaux]

but mergify has a cap for their free version of 100 / month. At this point, it doesn't seem we need a replacement for bors.

[Rob Lewis]

Mergify would cost $12/mo/seat, but I'm not sure what "seat" means. If it's active users, or even active mergers, it's prohibitively expensive. If it's repo, then $12/mo for Mergify on mathlib4 might be worth it if/when bors returns to its grave

[Eric Rodriguez]

Has anyone contacted mergify directly?

[Joachim Breitner]

Just did :-)

[Julien Danjou]

Joachim Breitner said:

Just did :-)

:wave: Julien from Mergify here! Thanks @Joachim Breitner for the invitation :)
If you think we'd be a good solution for you, I'd be happy to have a chat. We (have to) announce limitations on the open source plan to avoid abuse, but we can raise those on a case-by-case basis.

[Johan Commelin]

@Julien Danjou Hi! Thanks for taking the time to hop on this zulip!

I don't know how much details Joachim already gave you, but here is a short summary: https://leanprover-community.github.io/mathlib_stats.html shows that we have ~500 commits per month on our master branch, on busy days this means merging > 20 PRs per day. Since CI runs can take over 1 hour in worst-case scenarios this would mean that a linear merging strategy leads to a traffic jam.

We used bors to batch CI runs and merge batches of PRs in one go. But bors is EOL, so now we are looking at alternatives. Over the weekend we managed to set up a self-hosted bors instance. I'm not up to speed on the final details, but my impression is that "it works mostly fine" TM, and "there are still a few glitches" TM.

We also used mergify several years ago. Back then it didn't have the feature to merge PRs in batches. But that seems to have changed...

[Julien Danjou]

Hi @Johan Commelin !

Yes, we're far more feature-complete than Bors at this point, if one can say — but it's not a competition; it's about finding the right tool for you.

We do support batches, indeed, and even multiple concurrent batches. Details here: https://docs.mergify.com/merge-queue/batches/

Merging 20 PRs per day won't be a problem as far as we're concerned. I've tagged your organization as being authorized to go above limits on our open-source plan, so feel free to give it a try.

[Joachim Breitner]

That’s at least a proactive customer service that (I assume) we won’t get at Github :-)