Skip to content

Commit

Permalink
sagemathgh-35062: Enable merge_group trigger for merge queues
Browse files Browse the repository at this point in the history
    
### 📚 Description

Two days ago [github announced the public beta of merge
queues](https://github.blog/changelog/2023-02-08-pull-request-merge-
queue-public-beta/). The idea is pretty similar the current
release/merge process (as far as I understand it): Given you want to
merge three PRs into `develop`, you add them to the merge queue and
github will create three temporary branches:
- PR1
- PR1 + PR2 merged
- PR1 + PR2 + PR3 merged

It then runs all checks with the `merge_group` trigger on each branch.
Once all checks for all these temporary branches are successful, the
whole group is merged into `develop`. If there are merge conflicts, say
between PR3 and PR1, or the build for the PR1+2+3 branch fails, then PR3
is removed from the merge queue and only the first two PRs are merged
into `develop`.

In this way, one could never end up in a situation where the checks are
not passing in the develop branch, without requiring devs to always
merge the latest develop branch themselves. (E.g., we will no longer hit
the situation that PR2 introduces new linter rules which are not
fullfiled by PR3 but both PRs are merged into develop).

References:
- https://docs.github.com/en/repositories/configuring-branches-and-
merges-in-your-repository/configuring-pull-request-merges/managing-a-
merge-queue
- https://docs.github.com/en/actions/using-workflows/events-that-
trigger-workflows#merge_group

---

In this PR we add the merge_group trigger on the current PR-workflows,
which enables to run these in the merge queue as well.

---

Since this effectively implements the current version of "Volker's
temporary private develop branch", I was wondering if this would be
eneough to give more people rights to merge PRs. What else would be
necessary for such a step? @vbraun

<!-- Describe your changes in detail -->
<!-- Why is this change required? What problem does it solve? -->
<!-- If it resolves an open issue, please link to the issue here. For
example "Closes sagemath#1337" -->

### 📝 Checklist

<!-- Put an `x` in all the boxes that apply. -->
<!-- If your change requires a documentation PR, please link it
appropriately -->
<!-- If you're unsure about any of these, don't hesitate to ask. We're
here to help! -->

- [ ] I have linked an issue or discussion.
- [ ] I have created tests covering the changes.
- [ ] I have updated the documentation accordingly.

### ⌛ Dependencies
<!-- List all open pull requests that this PR logically depends on -->
<!--
- #xyz: short description why this is a dependency
- #abc: ...
-->
    
URL: sagemath#35062
Reported by: Tobias Diez
Reviewer(s): Dima Pasechnik, Matthias Köppe, Tobias Diez
  • Loading branch information
Release Manager committed Oct 1, 2023
2 parents 1cf0c13 + 043e76a commit c7b19b2
Show file tree
Hide file tree
Showing 3 changed files with 15 additions and 2 deletions.
5 changes: 4 additions & 1 deletion .github/workflows/build.yml
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,11 @@ name: Build & Test

on:
pull_request:
merge_group:
push:
branches: ['**']
branches:
- master
- develop
# Ignore pushes on tags to prevent two uploads of codecov reports
tags-ignore: ['**']
workflow_dispatch:
Expand Down
4 changes: 4 additions & 0 deletions .github/workflows/doc-build.yml
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,11 @@ name: Build documentation

on:
pull_request:
merge_group:
push:
branches:
- master
- develop
workflow_dispatch:
# Allow to run manually

Expand Down
8 changes: 7 additions & 1 deletion .github/workflows/lint.yml
Original file line number Diff line number Diff line change
@@ -1,6 +1,12 @@
name: Lint

on: [push, pull_request]
on:
push:
branches:
- master
- develop
pull_request:
merge_group:

concurrency:
# Cancel previous runs of this workflow for the same branch
Expand Down

0 comments on commit c7b19b2

Please sign in to comment.