git dropped a lemma during merging... why?

Stream: nightly-testing

[Johan Commelin]

Can someone explain to me what happened in the history of nightly-testing?

Specifically, look at https://github.com/leanprover-community/mathlib4/commits/nightly-testing/Mathlib/Data/BitVec.lean

In the past two days, we have had some changes to Mathlib/Data/BitVec.lean on master. But somehow those didn't faithfully end up in nightly-testing, leaving the file in a broken state.

I think the following merge commit just dropped a lemma: https://github.com/leanprover-community/mathlib4/commit/b57c9b7f461c042a5bf8c4d33f7bc6d396a166ff#diff-6775cfd199bc623efa28ab83f50cb425439c6b8e61620229a231e9f8f17a280c

But I don't see that in the github web view. However, when I look at that commit in gitk, I see

@@@ -63,10 -68,17 +68,10 @@@ instance : CommSemiring (BitVec w) :
      (fun _ => rfl) /- toFin_natCast -/
  -- The statement in the new API would be: `n#(k.succ) = ((n / 2)#k).concat (n % 2 != 0)`

 --- Variant of `Fin.intCast_def` for when we are using the `Fin.CommRing` instance.
 -open Fin.CommRing in
 -theorem _root_.Fin.intCast_def' {n : Nat} [NeZero n] (x : Int) :
 -    (x : Fin n) = if 0 ≤ x then Fin.ofNat n x.natAbs else -Fin.ofNat n x.natAbs := by
 -  unfold Fin.instCommRing
 -  dsimp [Int.cast, IntCast.intCast, Int.castDef]
 -  split <;> (simp [Fin.intCast]; omega)
 -
 +-- TODO: move to the Lean4 repository.
  @[simp] theorem _root_.Fin.val_intCast {n : Nat} [NeZero n] (x : Int) :
      (x : Fin n).val = (x % n).toNat := by
-   rw [Fin.intCast_def]
+   rw [Fin.intCast_def']
    split <;> rename_i h
    · simp [Int.emod_natAbs_of_nonneg h]
    · simp only [Fin.ofNat_eq_cast, Fin.val_neg, Fin.natCast_eq_zero, Fin.val_natCast]

which shows _root_.Fin.intCast_def' being dropped.

The command line git client also shows me

$ git show b57c9b7f461c042a5bf8c4d33f7bc6d396a166ff
commit b57c9b7f461c042a5bf8c4d33f7bc6d396a166ff
Merge: 66d7396a6dd 4d464b72a4f
Author: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Date:   Fri Jun 6 06:41:05 2025 +0000

    Merge master into nightly-testing

diff --cc Mathlib/Data/BitVec.lean
index b2b8c989a2e,3990ce5c0a8..8a79b51af8c
--- a/Mathlib/Data/BitVec.lean
+++ b/Mathlib/Data/BitVec.lean
@@@ -63,10 -68,17 +68,10 @@@ instance : CommSemiring (BitVec w) :
      (fun _ => rfl) /- toFin_natCast -/
  -- The statement in the new API would be: `n#(k.succ) = ((n / 2)#k).concat (n % 2 != 0)`

 --- Variant of `Fin.intCast_def` for when we are using the `Fin.CommRing` instance.
 -open Fin.CommRing in
 -theorem _root_.Fin.intCast_def' {n : Nat} [NeZero n] (x : Int) :
 -    (x : Fin n) = if 0 ≤ x then Fin.ofNat n x.natAbs else -Fin.ofNat n x.natAbs := by
 -  unfold Fin.instCommRing
 -  dsimp [Int.cast, IntCast.intCast, Int.castDef]
 -  split <;> (simp [Fin.intCast]; omega)
 -
 +-- TODO: move to the Lean4 repository.
  @[simp] theorem _root_.Fin.val_intCast {n : Nat} [NeZero n] (x : Int) :
      (x : Fin n).val = (x % n).toNat := by
-   rw [Fin.intCast_def]
+   rw [Fin.intCast_def']
    split <;> rename_i h
    · simp [Int.emod_natAbs_of_nonneg h]
    · simp only [Fin.ofNat_eq_cast, Fin.val_neg, Fin.natCast_eq_zero, Fin.val_natCast]

which is much more concise (AND much more revealing!!) then the github webview.

I'm very confused, and suddenly don't really trust what github is showing me :explode:

[Johan Commelin]

So really, there are two questions:

1. Why did this bad merge happen in the first place?
2. Why couldn't we spot it on github in the second place?

[Joscha Mennicken]

Regarding 2.: Since each commit describes a full snapshot of the repo, there isn't an obvious answer as to what the diff of a merge commit should be - what should it be diffed against? Github seems to show the diff between the first parent and the merge commit itself (though it may actually be some sort of combined diff, I'm not sure), while git show seems to be smarter. According to the man page, "It also presents the merge commit in a special format as produced by git diff-tree --cc", which (as far as I understand) combines the diffs against each parent and also tries to only show the places where merge conflicts had to be resolved.

[Joscha Mennicken]

After some more testing, GitHub seems to show exactly the diff against the first parent, no special sauce.

[Johan Commelin]

Thanks for explaining! It's sad that github is not using the smarter git show.

[Joscha Mennicken]

Regarding 1.: The lemma was added in commit fc52fd8bbdcc3675a7344743f7a46a3f59ad2be6 as part of PR #25476. The bot seems to use the ours option to the ort merge strategy to resolve conflicts. When the bot created its merge commit, there was probably a merge conflict involving the newly added lemma and some change on the nightly branch, and since the bot prefers the nightly changes in case of conflict, it threw away the lemma.

Automatic merge conflict resolution will get things wrong from time to time. While git's heuristics are (mostly) correct for simple changes, when they fail to decide on a solution, semantic information tends to be required. Merge conflicts occur when Git's heuristics can't find an obvious solution, which is usually when two changes touch or overlap (the diff algorithm's heuristics decide where the change actually occurs in the first place).

[Joscha Mennicken]

You can reproduce it by:

$ git switch 66d7396a6dd --detach
$ git merge 4d464b72a4f
Auto-merging Mathlib/Data/BitVec.lean
CONFLICT (content): Merge conflict in Mathlib/Data/BitVec.lean
Automatic merge failed; fix conflicts and then commit the result.

The merge conflict looks like this:

<<<<<<< HEAD
-- TODO: move to the Lean4 repository.
||||||| e32a1c5b1f1
open Fin.IntCast

-- TODO: move to the Lean4 repository.
=======
-- Variant of `Fin.intCast_def` for when we are using the `Fin.CommRing` instance.
open Fin.CommRing in
theorem _root_.Fin.intCast_def' {n : Nat} [NeZero n] (x : Int) :
    (x : Fin n) = if 0 ≤ x then Fin.ofNat n x.natAbs else -Fin.ofNat n x.natAbs := by
  unfold Fin.instCommRing
  dsimp [Int.cast, IntCast.intCast, Int.castDef]
  split <;> (simp [Fin.intCast]; omega)

>>>>>>> 4d464b72a4f

[Joscha Mennicken]

ours (nightly) is the section between <<< and |||, the merge base is the section between ||| and ===, and theirs (master) is the section between === and >>>.

In other words, on nightly the open Fin.IntCast was removed while on master open Fin.IntCast as well as the -- TODO: ... were replaced by the lemma.

[Johan Commelin]

@Joscha Mennicken Thanks a lot for all the details!

[Joscha Mennicken]

The only way to reliably prevent this I can think of is to abort on merge conflicts and merge manually in those cases

[Johan Commelin]

Yeah, but before nightly-testing ends up in master, it goes through a PR review anyways. So I think the current opportunistic approach is probably the best overall