Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(ci): switch from mergify to bors (#2322)
This PR (joint work with @gebner) changes the automation that merges our PRs from mergify to a service called [bors](https://bors.tech/). Currently, the "time-to-master" of an approved PR grows linearly with the number of currently queued PRs, since mergify builds PRs against master one at a time. bors batches approved PRs together before building them against master so that most PRs should merge within 2*(current build time). As far as day-to-day use goes, the main difference is that maintainers will approve PRs by commenting with the magic words "`bors r+`" instead of "approving" on Github and adding the "ready-to-merge" label. Contributors should be aware that pushing additional commits to an approved PR will now require a new approval. Some longer notes on bors and mathlib can be found [here](https://github.com/leanprover-community/mathlib/blob/2ea15d65c32574aaf513e27feb24424354340eea/docs/contribute/bors.md). Co-authored-by: Gabriel Ebner <gebner@gebner.org>
- Loading branch information
1 parent
495deb9
commit f723f37
Showing
12 changed files
with
269 additions
and
89 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,63 @@ | ||
| name: Add "ready-to-merge" label | ||
|
|
||
| on: | ||
| issue_comment: | ||
| types: [created] | ||
|
|
||
| jobs: | ||
| add_label: | ||
| name: Add label | ||
| if: (toJSON(github.event.issue.pull_request) != 'null') && (startsWith(github.event.comment.body, 'bors r+') || contains(toJSON(github.event.comment.body), '\r\nbors r+') || startsWith(github.event.comment.body, 'bors merge') || contains(toJSON(github.event.comment.body), '\r\nbors merge')) | ||
| runs-on: ubuntu-latest | ||
| steps: | ||
| - uses: octokit/request-action@v2.x | ||
| name: Get PR head | ||
| id: get_pr_head | ||
| with: | ||
| route: GET /repos/:repository/pulls/:pull_number | ||
| repository: ${{ github.repository }} | ||
| pull_number: ${{ github.event.issue.number }} | ||
| env: | ||
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | ||
|
|
||
| # Parse steps.get_pr_head.outputs.data, since it is a string | ||
| - id: parse_pr_head | ||
| name: Parse PR head | ||
| uses: gr2m/get-json-paths-action@v1.x | ||
| with: | ||
| json: ${{ steps.get_pr_head.outputs.data }} | ||
| head_user: 'head.user.login' | ||
|
|
||
| # we skip the rest if this PR is from a fork, | ||
| # since the GITHUB_TOKEN doesn't have write perms | ||
| - if: steps.parse_pr_head.head_user == 'leanprover-community' | ||
| uses: octokit/request-action@v2.x | ||
| name: Get comment author | ||
| id: get_user | ||
| with: | ||
| route: GET /repos/:repository/collaborators/:username/permission | ||
| repository: ${{ github.repository }} | ||
| username: ${{ github.event.comment.user.login }} | ||
| env: | ||
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | ||
|
|
||
| # Parse steps.get_user.outputs.data, since it is a string | ||
| - if: steps.parse_pr_head.head_user == 'leanprover-community' | ||
| id: parse_user | ||
| name: Parse comment author permission | ||
| uses: gr2m/get-json-paths-action@v1.x | ||
| with: | ||
| json: ${{ steps.get_user.outputs.data }} | ||
| permission: 'permission' | ||
|
|
||
| - if: (steps.parse_pr_head.head_user == 'leanprover-community') && (steps.parse_user.outputs.permission == 'admin') | ||
| uses: octokit/request-action@v2.x | ||
| id: add_label | ||
| name: Add label | ||
| with: | ||
| route: POST /repos/:repository/issues/:issue_number/labels | ||
| repository: ${{ github.repository }} | ||
| issue_number: ${{ github.event.issue.number }} | ||
| labels: '["ready-to-merge"]' | ||
| env: | ||
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,6 @@ | ||
| status = ["Build mathlib"] | ||
| use_squash_merge = true | ||
| timeout_sec = 21600 | ||
| block_labels = ["not-ready-to-merge", "WIP", "changes-requested", "blocked-by-other-PR"] | ||
| delete_merged_branches = true | ||
| cut_body_after = "TO CONTRIBUTORS:" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,125 @@ | ||
| # bors for mathlib! | ||
|
|
||
| [](https://app.bors.tech/repositories/24316) | ||
|
|
||
| In early April 2020, we had a stretch where the mergify queue was constantly 4-5 PRs deep, which | ||
| meant that the time between setting a PR as "ready-to-merge" and its landing in `master` was 12+ | ||
| hours. With mergify, the amount of time it takes to finish merging `N` "ready-to-merge" PRs is | ||
| `O(N)`, since every PR is tested against the current master in a serial fashion. This will only get | ||
| worse as both build times and the rate of contributions increase. | ||
|
|
||
| To address this, we decided to switch from our previous mergify-based workflow to one using | ||
| [bors-ng](https://bors.tech/). `bors` is a free service that is able to batch multiple PRs together | ||
| in a "`staging`" branch, run the CI scripts on that branch, and then fast-forward `master` if CI | ||
| passes. | ||
|
|
||
| For PRs with no CI failures, the time from approval to merging should be at most 2*`T`, where `T` is | ||
| the amount of time to run CI on a commit. One `T` is for the `staging` build already in progress | ||
| when the PR is approved (if any), and one `T` is needed for the batch that the PR is added to. | ||
|
|
||
| If CI on `staging` fails (e.g. due to a merge conflict), bors will split the batch in two and try to | ||
| merge each of those separately, so that the time to merge is `O(E log N)` where `E` is the error | ||
| rate. (See [here](https://github.com/bors-ng/bors-ng/blob/master/README.md#how-it-works) for a few | ||
| more details.) | ||
|
|
||
| ## What has changed? | ||
|
|
||
| *[See also bors-ng "Getting Started"](https://bors.tech/documentation/getting-started/) and | ||
| ["Reference"](https://bors.tech/documentation/)*. | ||
|
|
||
| - Using bors is very similar to the previous mergify-based workflow, except that instead of | ||
| approving and adding the "ready-to-merge" label, maintainers just need to remove any "blocked | ||
| labels" ("WIP", "changes-requested", "not-ready-to-merge", "blocked-by-other-PR") and then add a | ||
| comment to the PR containing "`bors r+`" (or "`bors merge`") on its own line. This will add the PR | ||
| to the last batch in the bors queue. This can be cancelled by commenting with "`bors r-`" / | ||
| "`bors merge-`". | ||
|
|
||
| - We have a Github Actions workflow which will try to label approved PRs with | ||
| "ready-to-merge" so that we can see at a glance which open PRs are in the queue. It's not perfect, | ||
| so if you notice a PR that's approved but missing the label, feel free to add the label manually. | ||
|
|
||
| - Usually the queue will consist of at most two batches, the batch whose build is in progress and | ||
| one batch that is "Waiting to run", but if errors have occurred, the queue may get longer. | ||
| (Compare this to the mergify queue, whose length is equal to the number of approved PRs.) | ||
|
|
||
| - One significant change is that pushing new commits to a PR branch after it's marked "`bors r+`" | ||
| will cancel it (remove it from its queue), and a maintainer will have to write "`bors r+`" again. | ||
|
|
||
| - Maintainers can also write "`bors d+`" (short for "`bors delegate+`") to allow the PR author to | ||
| add "`bors r+`". This can be customized with a list of users, see the bors-ng Reference. | ||
|
|
||
| - While we still get a nice linear git history like we're used to (see below), PRs squashed and | ||
| merged by bors will no longer display as "Merged" on Github with the purple icon. Instead, bors | ||
| will Close the PR (red icon) and prepend "**[Merged By Bors] -**" to the title. This is a Github | ||
| API limitation, [see the discussion in this thread](https://forum.bors.tech/t/use-a-squash-merge-in-bors/349/19). | ||
|
|
||
| - Pushing commits directly to `master` will cause any currently running bors batch to fail and get | ||
| (automatically) retried (see [the notes here](https://github.com/bors-ng/bors-ng/pull/859)). We've | ||
| changed leanprover-community-bot so that it will create its own "update nolints.txt" PRs and also | ||
| add `bors r+` to them. | ||
|
|
||
| - Commit messages are taken from the first post of the PR. This is much nicer than mergify / | ||
| Github's default which just combines all commit subject lines into one. We have set things | ||
| up so that the text after "TO CONTRIBUTORS" is automatically ignored. Note that | ||
| contributions from other users will have to be added explicitly to the first post with | ||
| ["Co-authored-by:" trailers](https://github.blog/2018-01-29-commit-together-with-co-authors/); | ||
| they aren't automatically added like how mergify and Github previously did. | ||
|
|
||
| - Even if the usual "push" build succeeds on a PR branch that is up-to-date with master, `bors r+` | ||
| will not instantly merge it into `master` the way mergify used to; instead, bors will run the CI | ||
| again on the staging branch. [See related issue](https://github.com/bors-ng/bors-ng/issues/852). | ||
|
|
||
| - `bors r+` on a PR from an external fork will crash if there are any changes to the Github Actions | ||
| config; [see here](https://github.com/bors-ng/bors-ng/issues/806). PRs that propose such changes | ||
| will have to be merged manually or transferred to the community repo. | ||
|
|
||
| Note that approving PRs from external forks which *don't* propose changes to Github Actions can | ||
| still cause bors to crash if the Github Actions config in `master` is changed before the PR is | ||
| merged. Presumably asking the PR author to merge `master` into their branch should work. | ||
|
|
||
| - There is a `bors try` option which might be useful for running CI and getting oleans for PRs from | ||
| external forks. I don't think we've tested this yet. | ||
|
|
||
| - Github Actions has a UI bug which shows pushed commits as being built from the `staging` branch. | ||
| However, if we check the actual head refs, the commits are actually pushed to `staging`, then | ||
| `master`, then `staging.tmp*` (and we've set things up so only the first two are run). | ||
|
|
||
| ## Git history | ||
|
|
||
| We're using an option `with_squash_merge = true` which makes the git history look the same as it did | ||
| with mergify. | ||
|
|
||
| Here is a pretty ASCII diagram ([source](https://github.com/bors-ng/bors-ng/issues/194#issuecomment-361011427)): | ||
|
|
||
| **6. squash and rebase, fast-forward merge** | ||
|
|
||
| Rough git command equivalent: | ||
|
|
||
| ``` | ||
| for pr in pr1 pr2 pr3; do | ||
| git checkout $pr | ||
| git rebase --interactive staging.tmp | ||
| git checkout staging.tmp | ||
| git merge --ff-only $pr | ||
| done | ||
| ``` | ||
|
|
||
| What it looks like: | ||
|
|
||
| ``` | ||
| --E---F---G PR1 | ||
| / | ||
| / | ||
| / H---I---J PR2 | ||
| / / | ||
| / | | ||
| / | K---L---M PR3 | ||
| / |/ | ||
| A---B---C---D master | ||
| | | ||
| | | ||
| v | ||
| A---B---C---D---[EFG]---[HIJ]---[KLM] master | ||
| ``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file was deleted.
Oops, something went wrong.
Oops, something went wrong.