buggy infoview?

Stream: general

[Kevin Buzzard]

In this gist (discovered by someone at Xena this evening) the infoview output just after the comma on line 66 is completely unrelated to the tactic state: it randomly seems to be the goal state on line 225. Moving to the beginning of line 67, sanity is restored. The first year student who discovered it apologises for their lousy lean by the way :-)

[Yakov Pechersky]

We saw this previously due to a buggy congr' _ with _

[Yakov Pechersky]

No congr' here

[Yakov Pechersky]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Extension.20showing.20goal.20for.20a.20separate.20lemma

[Bryan Gin-ge Chen]

Aha. convert on line 225 uses congr'. source

[Yakov Pechersky]

On my machine, I do not see the buggy when just pasting the gist into VSCode. That's because on pasting, the extra space after the comma on the push_neg line (66) is stripped. Bringing it back and holding the line cursor there shows the wrong goal state. Adding and moving to another space on that line goes back to what is expected.

[Kevin Buzzard]

Yeah so this is the "line 66 column 16 bug", because if you hit enter a few times before line 66 to make line 66 be the linarith a few lines before, and then slowly move the cursor to the right, the infoview randomly changes on column 16.
line66.gif

[Yakov Pechersky]

A "workaround", transpose the set ... and push_neg ... lines. Then the tactic state at any point in the set ... line is as expected, similarly push_neg ....

[Kevin Buzzard]

I don't need a workaround, I'm loving it :-)

[Yakov Pechersky]

image.png

[Yakov Pechersky]

SpoOOoOky action at a distance?

[Yakov Pechersky]

And of course, line 65 col 33 has the same issue.

[Kevin Buzzard]

Shing is telling me that I'm one out because the infoview is one column out.