Zulip Chat Archive
Stream: general
Topic: comments highlighted in VSCode
Rob Lewis (Jul 12 2022 at 13:17):
I don't know how long this has been happening, but I don't think it's been forever (or maybe it has and I just blindly looked past it). I've been seeing messages in VSCode bleed into later lines if the noisy commands are follwed by comments.
image.png
This is on Ubuntu, VSCode extension 0.16.53, but I also see it on GitPod. Is this new(ish) or a figment of my imagination? Is there an easy fix?
Thomas Browning (Jul 12 2022 at 13:22):
I also only noticed this recently
Gabriel Ebner (Jul 12 2022 at 13:23):
I am 200% sure this issue is on the Lean side. What happens is that every token consumes the whitespace after it as well (and comments are white space). Check and print are the only commands that produce a message with an end position, so you won't see this issue anywhere else.
Eric Wieser (Jul 12 2022 at 13:24):
I think I recently taught the extension to respect end positions
Eric Wieser (Jul 12 2022 at 13:25):
I hadn't considered they might be useless
Eric Wieser (Jul 12 2022 at 13:26):
Probably the best fix is for lean to strip "whitespace" tokens when giving end positions?
Eric Wieser (Jul 12 2022 at 13:27):
The quick hack is to stop sending them at all if they're worse than the heuristic end position
Gabriel Ebner (Jul 12 2022 at 13:27):
Easy and done that way in :four_leaf_clover:, but not sure if worth the effort in :three:.
Patrick Massot (Jul 12 2022 at 13:29):
I confirm this rather new and very annoying.
Rob Lewis (Jul 12 2022 at 13:29):
Was there a recent change that caused this?
Eric Wieser (Jul 12 2022 at 13:30):
It came in with the Unicode codepoint counting change to vscode-lean I made (leanprover/vscode-lean#301)
Eric Wieser (Jul 12 2022 at 13:30):
There was no comment warning against listening to the end_pos field from the server, so I figured I'd just use the field whenever it was present
Eric Wieser (Jul 12 2022 at 13:33):
The relevant diff line is
https://github.com/leanprover/vscode-lean/pull/301/files#diff-da8cc70370d67b4c482d5cf755fb7f45697844107dd73ccf7f5b54162703f63cL68-R75
Jeremy Avigad (Jul 12 2022 at 15:44):
I also noticed this a couple of days ago, while preparing lectures of LFTCM. A workaround is to put all the #check commands in section ... end blocks.
Rob Lewis (Jul 12 2022 at 16:00):
Or . after the #check command, but this can be a little confusing for beginners.
Gabriel Ebner (Jul 12 2022 at 17:36):
If we have a consensus, it's fine to revert to positions instead of ranges. We could also truncate ranges to the first line (like :four_leaf_clover:). PRs welcome!
Eric Wieser (Jul 12 2022 at 21:16):
I was also thinking truncating to the first line was a good compromise too
Eric Wieser (Jul 12 2022 at 21:31):
Does anything actually use the end positions?
Eric Wieser (Jul 12 2022 at 21:35):
Claims to have been added for some "message box" feature: https://github.com/leanprover-community/lean/commit/bf0d78588803657389891aa756f377122d70f8a7
Eric Wieser (Jul 12 2022 at 21:37):
The line that populates it unhelpfully for check is https://github.com/leanprover-community/lean/blob/9dc6b1ea9d64cb163b0a0c371622887d32e6792f/src/frontends/lean/builtin_cmds.cpp#L210
Mario Carneiro (Jul 13 2022 at 04:13):
The --ast output does make use of end positions, although they might not be computed/extracted in all the same places as the server messages
Mario Carneiro (Jul 13 2022 at 04:16):
We already have to handle proper end pos calculation for tactic spans after by so it's likely there is a simple fix
Mario Carneiro (Jul 13 2022 at 04:34):
Patrick Massot (Jul 13 2022 at 13:18):
Could we have a Lean release including that really soon? This issue is really super painful for Lftcm2022 because #check is used a lot in tutorials.
Eric Rodriguez (Jul 13 2022 at 13:36):
it should be a painless bump, too
Eric Rodriguez (Jul 13 2022 at 13:36):
have we confirmed that this fix actually fixes the issue?
Eric Wieser (Jul 13 2022 at 15:50):
Yes, I tested it
Eric Rodriguez (Jul 13 2022 at 15:50):
cc @Gabriel Ebner
Eric Wieser (Jul 13 2022 at 15:51):
I was hoping that https://github.com/leanprover-community/lean/pull/743 would make it into the same lean release to fix the problem in this thread (json.parse "-1" = some (json.of_int 4294967295))
Eric Rodriguez (Jul 13 2022 at 15:51):
Eric Rodriguez (Jul 13 2022 at 15:51):
putting a full stop at the end of each #check/#print is a nice quick workaround
Eric Wieser (Jul 13 2022 at 15:51):
But I guess that's not necessary for LFTCM
Eric Wieser (Jul 13 2022 at 15:54):
Eric Rodriguez said:
it should be a painless bump, too
Indeed, all that changed is the end_pos fix we need here, a bug in meta code for empty structures, and floats/integer conversions being better behaved
Gabriel Ebner (Jul 13 2022 at 16:00):
Can you make the PR? I'm currently on vacation.
Eric Wieser (Jul 13 2022 at 16:02):
We just copy https://github.com/leanprover-community/lean/pull/737, right?
Eric Wieser (Jul 13 2022 at 16:14):
https://github.com/leanprover-community/lean/pull/745, but we should wait for the previous build to finish first
Eric Wieser (Jul 13 2022 at 22:16):
Eric Wieser (Jul 14 2022 at 08:08):
#15325 is now passing CI; As Eric Rodriguez said, the bump was trivial
Last updated: Dec 20 2023 at 11:08 UTC