Zulip Chat Archive

Stream: general

Topic: buggy infoview?


view this post on Zulip 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 :-)

view this post on Zulip Yakov Pechersky (Nov 12 2020 at 21:36):

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

view this post on Zulip Yakov Pechersky (Nov 12 2020 at 21:37):

No congr' here

view this post on Zulip Yakov Pechersky (Nov 12 2020 at 21:39):

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

view this post on Zulip Bryan Gin-ge Chen (Nov 12 2020 at 21:47):

Aha. convert on line 225 uses congr'. source

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 ....

view this post on Zulip Kevin Buzzard (Nov 12 2020 at 21:52):

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

view this post on Zulip Yakov Pechersky (Nov 12 2020 at 21:53):

image.png

view this post on Zulip Yakov Pechersky (Nov 12 2020 at 21:54):

SpoOOoOky action at a distance?

view this post on Zulip Yakov Pechersky (Nov 12 2020 at 21:55):

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

view this post on Zulip 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