Possible bug in diff highlighting

Stream: lean4

[Damiano Testa]

Dear All,

in the code below, I was expecting 4 and 5 to be highlighted as being "ready to change", but they are not. I imagine that the issue is that the "diff'er" sees literals and decides that they have not changed, instead of inspecting what the actual literal is.

example {a b : Nat} (h : b + a = 0): a + b = 0 := by
  rw [Nat.add_comm] -- place the cursor at the beginning of this line: `a` and `b` are diff'ed
  assumption

example (h : 5 + 4 = 0) : 4 + 5 = 0 := by
  rw [Nat.add_comm] -- place the cursor at the beginning of this line: `4` and `5` are *not* diff'ed
  assumption

Of course, this has little consequence. However, if I wanted to find the place in the code where the diff'ing happens, how would I go about it?

Thanks!

[Mario Carneiro]

cc: @Edward Ayers

[Damiano Testa]

I think that I found a relevant thread.

[Damiano Testa]

Possibly, at this line a further case could be added for Expr.lit atoms?

[Mario Carneiro]

I don't think that's the issue; without a .lit case it would just treat every pair of literals as differing

[Mario Carneiro]

I think what is happening is that the diff is traversing partially inside the term 4, so there is no place to show the highlight

[Damiano Testa]

Ah, a case of "I found a beautiful diff for your tactic, but this expression is too small to contain it"?

[Mario Carneiro]

I'm not sure exactly how to make it work but the diff should be "rounded up" somehow to the nearest displayable subexpression; it should never be the case that a diff is hidden because there isn't a syntax for that subexpression

[Damiano Testa]

But why does the diff on a and b work then?

[Mario Carneiro]

because a is what changed in that case

[Damiano Testa]

and isn't 4 what changed in the second case?

[Mario Carneiro]

with 4 what changed is actually the two occurrences of 4 in OfNat Nat 4 (instOfNat 4)

[Mario Carneiro]

which are .lit

[Damiano Testa]

Ah, I see and I understand you comment now: the change is embedded further inside.

[Damiano Testa]

It is "shielded" by the OfNat application, right?

[Mario Carneiro]

we want to show a diff that is more fine-grained than we can display

[Mario Carneiro]

it would be extra cool if you could see the fine grained diff if you hover over the 4

[Damiano Testa]

So now the marker for the beginning and end of changes get updated to the (two) 4s inside the OfNat application, but then the infoview does not show this, right?

[Damiano Testa]

whereas the diff should only update the begin/end position once it reaches a displayable location, not any location.

[Damiano Testa]

And you are saying that the infoview could highlight 4 in the case above, but then, on hover, highlight the 4's inside the OfNat application?

[Damiano Testa]

Am I understanding what is happening?

[Damiano Testa]

Something like duplicating the begin/end markers, one for displayble change, one for actual change. Possibly, the current one with the actual change determines the "next-up" available displayable one, though...

[Damiano Testa]

In this case,

example : 4 + a = 0 := by
  rw [add_comm]

4 also gets highlighted.

[Mario Carneiro]

which validates my diagnosis

[Damiano Testa]

In this case, 4 is highlighted because the diff does not enter it? The diff does not enter 4 since the arguments of HAdd.hadd have already different heads?

[Damiano Testa]

Ok:

example : Nat.cast 4 + Nat.cast 3 = 0 := by
  rw [add_comm]  -- no, no highlighting here

example : Nat.cast 4 + 3 = 0 := by
  rw [add_comm]  -- yes, highlighting here

[Damiano Testa]

So, I think that I now understand better what you said from the very beginning!

[Damiano Testa]

Indeed, this highlights the "inner-most" change:

example : @OfNat.ofNat ℕ (Nat.succ Nat.zero) _ + @OfNat.ofNat ℕ (Nat.succ $ Nat.succ Nat.zero) _ = 0 := by
  rw [add_comm]  -- `Nat.zero` vs `Nat.succ Nat.zero`

This is very cool!

[Mario Carneiro]

here's another way to see the highlight:

set_option pp.all true
example : 4 + 3 = 0 := by
  rw [Nat.add_comm]

[Damiano Testa]

Ah, great! I was doing my own pp.almost_all implementation by hand...

[Damiano Testa]

So, when the information about the diff reaches the stage where it should be printed, then either

• the diff stained a whole node that gets printed with the current settings and thus gets displayed, or
• the stain is inside something that is displayed and gets ignored, rather than expanding.

I know that this is probably the content of your first comment, Mario, but I am very unaware of how these things happen!

[Mario Carneiro]

so the question is then, where is the logic that actually does the rendering and how should it be changed to not ignore changes in subterms

[Damiano Testa]

Yes, suddenly I feel like I understand what you say, Mario!

[Damiano Testa]

Is the idea that whatever takes care of printing should remember whether a subpart was stained and propagate the stain to the whole?

[Sebastian Ullrich]

The answer to the first part is Lean.Widget.Diff