Skip to content

Commit 4ba2c37

Browse files
GarmelonReemMelamed
authored andcommitted
chore(CI): fix merge conflict resolution for nightly-testing (leanprover-community#40257)
Resolving merge conflicts in favor of `nightly-testing` when merging `master` may be convenient for nightly maintainers, but it can lead to changes made on `master` accidentally being dropped again later in the bump PR. For an example case, see leanprover-community#40189 (see [#PR reviews > leanprover-community#39443 &leanprover-community#96;nonempty_preimage_iff&leanprover-community#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2339443.20.60nonempty_preimage_iff.60/near/599885755) for an explanation of what happened). Resolving conflicts in favor of `master` means that `nightly-testing` will rather break than silently undoing changes made on `master`. Co-authored-by: Joscha <joscha@plugh.de>
1 parent 2958d52 commit 4ba2c37

1 file changed

Lines changed: 6 additions & 4 deletions

File tree

.github/workflows/nightly_merge_master.yml

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
# This job merges every commit to `master` into `nightly-testing`, resolving merge conflicts in favor of `nightly-testing`.
1+
# This job merges every commit to `master` into `nightly-testing`, resolving merge conflicts in favor of `master`.
22

33
name: Merge master to nightly
44

@@ -49,15 +49,17 @@ jobs:
4949
git config user.name "mathlib-nightly-testing[bot]"
5050
git config user.email "mathlib-nightly-testing[bot]@users.noreply.github.com"
5151
52-
- name: Merge master to nightly favoring nightly changes
52+
- name: Merge master to nightly favoring master changes
5353
run: |
5454
cd nightly-testing
5555
git remote add upstream https://github.com/leanprover-community/mathlib4.git
5656
git fetch upstream master
57-
# Merge master into nightly-testing, resolving conflicts in favor of nightly-testing
57+
# Merge master into nightly-testing, resolving conflicts in favor of master.
58+
# In the past, we've silently dropped changes made on master because
59+
# conflicts were resolved in favor of nightly-testing, which is bad.
5860
# If the merge goes badly, we proceed anyway via '|| true'.
5961
# CI will report failures on the 'nightly-testing' branch direct to Zulip.
60-
git merge upstream/master --strategy-option ours --no-commit --allow-unrelated-histories || true
62+
git merge upstream/master --strategy-option theirs --no-commit --allow-unrelated-histories || true
6163
# We aggressively run `lake update`, to avoid having to do this by hand.
6264
# When Batteries changes break Mathlib, this will likely show up on nightly-testing first.
6365
lake update -v

0 commit comments

Comments
 (0)