You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
To reduce the load on the CI infrastructure, run pr-merge only nightly (only if either the target branch or the head branch has been updated recently, as is the case today). When a pull request is submitted or updated, only run pr-head.
Until today, and since 21 November 2022, we were only running pr-merge (on PR submission/update and nightly), never pr-head. However the absence of pr-head has some downsides which made it tolerable as a temporary workaround, but not acceptable forever:
When a pull request has merge conflict, no CI runs.
We only get CI results for the merge, which can sometimes be hard to trace to the pre-merge code. This is mostly a problem for CI results that are hard to reproduce locally (non-Linux platforms, non-free compilers).
When a pull request hasn't been updated for a while, the only status visible on GitHub is “did not run”. So when looking for things to review or gatekeep, we can't distinguish “this needs work before it'll pass the CI” from “this passed the CI against a slightly older version of the target branch, so it's probably ok”. Digging in the previous builds on Jenkins might give the information, but it's tedious to figure out if there was a success on the latest head commit, and the history is erased after a while.
Today 20 December 2022, I have re-enabled pr-head. This is necessary for Mbed-TLS/mbedtls#6359, which will happen early in January 2023 and will lead to a temporary increased need for running the CI on pull requests with merge conflicts.
The text was updated successfully, but these errors were encountered:
Enable merge queues on the mbedtls repo #117 restores and improves on testing the pull request merged with its target branch: we now use a merge queue, so the CI runs on the actual merge commit before the merge becomes official. This is an improvement on the old pr-merge situation because that only ran nightly so the result could still be out of date.
To reduce the load on the CI infrastructure, run pr-merge only nightly (only if either the target branch or the head branch has been updated recently, as is the case today). When a pull request is submitted or updated, only run pr-head.
Until today, and since 21 November 2022, we were only running pr-merge (on PR submission/update and nightly), never pr-head. However the absence of pr-head has some downsides which made it tolerable as a temporary workaround, but not acceptable forever:
Today 20 December 2022, I have re-enabled pr-head. This is necessary for Mbed-TLS/mbedtls#6359, which will happen early in January 2023 and will lead to a temporary increased need for running the CI on pull requests with merge conflicts.
The text was updated successfully, but these errors were encountered: