[Merged by Bors] - ci: automated nightly-testing branch
#6823
Conversation
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
semorrison
added
awaiting-review
RFC
Since the CI runs only once a day, I think a daily nag is actually quite good. So I think the repeated messages are a feature, not a bug. |
|
Thanks 🎉 bors merge |
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Sep 1, 2023
This PR adds three workflows that manage a `nightly-testing` branch. * Every commit to `master` is merged to `nightly-testing`, resolving conflicts in favour of `nightly-testing`. * Once a day the `lean-toolchain` is bumped to the newest Lean nightly release. * If CI fails, a bot posts in the mathlib reviewers stream. The aim is to get quick notification that a nightly release of Lean is incompatible with Mathlib. The `nightly-testing` branch is not intended to ever contain human contributions, and in particular it is always okay to delete it and recreate it from `master`. If there are breaking changes: * If it could be fixed by a change to Mathlib that would work both on the current `lean-toolchain` used by `master`, and the latest nightlies, please make the PR to Mathlib `master`. * If it requires a fix that doesn't make sense on the current `lean-toolchain` used by `master`, please make a PR with a new `lean-toolchain`, mark that PR as `blocked-by-core-release`, but also **merge** your PR into `nightly-testing` (once you've verified it works!) There is no attempt to avoid repeated messages if we've already notified zulip about the failure, and subsequent commits continue to fail. Suggestions for dealing with that welcome. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
|
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. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
nightly-testing branchnightly-testing branch
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds three workflows that manage a
nightly-testingbranch.masteris merged tonightly-testing, resolving conflicts in favour ofnightly-testing.lean-toolchainis bumped to the newest Lean nightly release.The aim is to get quick notification that a nightly release of Lean is incompatible with Mathlib.
The
nightly-testingbranch is not intended to ever contain human contributions, and in particular it is always okay to delete it and recreate it frommaster.If there are breaking changes:
lean-toolchainused bymaster, and the latest nightlies, please make the PR to Mathlibmaster.lean-toolchainused bymaster, please make a PR with a newlean-toolchain, mark that PR asblocked-by-core-release, but also merge your PR intonightly-testing(once you've verified it works!)There is no attempt to avoid repeated messages if we've already notified zulip about the failure, and subsequent commits continue to fail. Suggestions for dealing with that welcome.