## Stream: general

### Topic: buggy infoview?

#### Kevin Buzzard (Nov 12 2020 at 21:28):

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 (Nov 12 2020 at 21:36):

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

#### Yakov Pechersky (Nov 12 2020 at 21:37):

No congr' here

#### Yakov Pechersky (Nov 12 2020 at 21:39):

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

#### Bryan Gin-ge Chen (Nov 12 2020 at 21:47):

Aha. convert on line 225 uses congr'. source

#### Yakov Pechersky (Nov 12 2020 at 21:50):

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 (Nov 12 2020 at 21:52):

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 (Nov 12 2020 at 21:52):

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 (Nov 12 2020 at 21:52):

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

image.png

#### Yakov Pechersky (Nov 12 2020 at 21:54):

SpoOOoOky action at a distance?

#### Yakov Pechersky (Nov 12 2020 at 21:55):

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

#### Kevin Buzzard (Nov 12 2020 at 21:59):

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

Last updated: May 13 2021 at 21:12 UTC