TuringLang
Require branches to be up to date before merging
Bors currently ensures that branches are up to date before merging. This results in a lot of comments because the integration isn't really integrated well into GitHub (nothing against Bors here, comments are the only way for such systems to send info to the user). Nowadays, GitHub has a setting for this:
which can also be combined with
Related discussion from another project at https://github.com/jazzband/pip-tools/issues/1085.
I know this Github feature, we use(d) it over at JuliaGaussianProcesses :slightly_smiling_face:
When we started using bors, it didn't exist. At that time there were often many PRs at the same time, and it happened multiple times that even though tests passed in PRs merging them broke the master branch.
There is still an advantage of bors over the Github settings, as far as I can see: You can just run bors in multiple PRs and bors will build a merge queue and make sure that one PR is merged after the other, given that tests pass, whereas otherwise you have to manually (or automatically) merge a PR and then manually update the next PR etc.
Another nice thing about bors is that one can specify explicitly when a PR should be tested and CI tests be run.
There is still an advantage of bors over the Github settings, as far as I can see: You can just run bors in multiple PRs and bors will build a merge queue and make sure that one PR is merged after the other, given that tests pass, whereas otherwise you have to manually (or automatically) merge a PR and then manually update the next PR etc.
Yes. You are right there. As it happens, there was a related discussion on Slack # infrastructure yesterday where Dilum Aluthge pointed out that GitHub is working on fixing that problem too with the Pull Request Merge Queue beta (https://github.blog/changelog/2021-10-27-pull-request-merge-queue-limited-beta/).
Another nice thing about bors is that one can specify explicitly when a PR should be tested and CI tests be run.
This can be done via GitHub too, right? Either via git commit --allow-empty -m 'Trigger CI' or via the web interface.
I get your points about the merge queue, but I do wonder whether the tradeoff is worth it. PRs serve as a point of reference for years to come and all the bot comments make finding information more difficult.
This can be done via GitHub too, right? Either via git commit --allow-empty -m 'Trigger CI' or via the web interface.
How can this be done in the web interface? This would not result in a pull_request trigger but eg a workflow_dispatch, so it's not necessarily the same since not all actions and packages support them the in the same way (eg Documenter, maybe it changed recently though). I'd also argue that both approaches are signficantly worse from an UX perspective.
Generally, I don't think the comments are a big issue. One could even delete them, manually or automatically. Many repos (also eg Julia base) use the same approach, eg for benchmarks. IMO comments could also be reduced if bors would be run only when a PR is discussed and approved. But yeah, my personal opinion is that diverging and (seemingly) unrelated discussion are much more confusing than bors comments.
(Maybe I should add that I'm not strictly against GH actions and features, I just think the current state is not too bad and still has advantages.)
