Zulip Chat Archive

Stream: general

Topic: VSCode puts error lines in the wrong place


Eric Wieser (May 18 2022 at 20:55):

This code:

example (𝒜𝒜𝒜𝒜𝒜𝒜𝒜𝒜𝒜𝒜𝒜𝒜 : nat) : ℕ := _

results in the error line going under nat when it should instead be under _:
image.png

Eric Wieser (May 18 2022 at 20:59):

This example:

example (𝒜𝒜𝒜𝒜𝒜𝒜𝒜𝒜𝒜𝒜𝒜𝒜 : nat) : ℕ := _

example (AAAAAAAAAAAA : nat) : ℕ := _

Reports the same column number with lean --make, so the bug must lie in the server or extension

Reid Barton (May 18 2022 at 21:01):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/VSCode.20squiggle.20off/near/269407218

Mario Carneiro (May 18 2022 at 21:07):

interestingly, https://github.com/microsoft/language-server-protocol/issues/376 recently got fixed, so maybe there is a way to fix this now

Eric Wieser (May 18 2022 at 21:19):

I thought Lean 3 didn't use LSP?

Eric Wieser (May 18 2022 at 21:19):

Or rather, that the L in Lean 3's LSP stood for Lean

Mario Carneiro (May 18 2022 at 21:30):

ah, fair point

Eric Wieser (May 18 2022 at 21:34):

I'll have a go at fixing the lean3 extension, I think the server is well-behaved

Arthur Paulino (May 18 2022 at 21:37):

Out of curiosity, how did you come up with that testing case? :open_mouth:

Mario Carneiro (May 18 2022 at 21:38):

it's easy enough to notice when you use one script letter

Mario Carneiro (May 18 2022 at 21:38):

using more script letters just makes the problem worse

Eric Wieser (May 18 2022 at 21:38):

Arthur Paulino said:

Out of curiosity, how did you come up with that testing case? :open_mouth:

The same input causes Overleaf to completely reject a tex file

Eric Wieser (May 18 2022 at 21:39):

This rabbit hole started with a spike trap

Eric Wieser (May 18 2022 at 21:39):

Apparently its editor, CodeMirror, doesn't handle things that use two UTF-16 code units

Mario Carneiro (May 18 2022 at 21:39):

the general problem happens if you use any characters above 0xFFFF

Eric Wieser (May 18 2022 at 21:39):

UTF-16 is the worst

Eric Wieser (May 18 2022 at 21:40):

UTF-8 forces people to actually solve these problems, UTF-32/UCS-4 makes them not exist.

Mario Carneiro (May 18 2022 at 21:41):

Most uses of UTF-16 are actually WTF-16 (UTF-16 with unpaired surrogates)

Eric Wieser (May 18 2022 at 21:41):

Mario Carneiro said:

interestingly, https://github.com/microsoft/language-server-protocol/issues/376 recently got fixed, so maybe there is a way to fix this now

VSCode just throws an error if it recieves this field with any value other than utf8

Mario Carneiro (May 18 2022 at 21:41):

...and yes, the acronym is intentional

Mario Carneiro (May 18 2022 at 21:42):

utf8 is fine, the hard part was getting it to recognize anything other than utf16

Mario Carneiro (May 18 2022 at 21:44):

is that for the server or the client?

Eric Wieser (May 18 2022 at 21:45):

I can't work out where the vscode client is

Eric Wieser (May 18 2022 at 21:45):

My best guess was https://github.com/microsoft/vscode-languageserver-node/blob/8b3c375adc4fa69f63726ef58d911c8e27b261c5/client/src/common/client.ts#L1120-L1122

Mario Carneiro (May 18 2022 at 21:47):

The protocol is that the client says a bunch of encodings it supports, and then the server replies with the encoding it wants to use. It makes sense for the template for typescript servers to reply utf-16 since javascript is utf-16 native

Mario Carneiro (May 18 2022 at 21:49):

in particular you can tell that is a server response and not the client list because the client's version is positionEncodings (note the plural)

Mario Carneiro (May 18 2022 at 21:50):

actually that's not right, that is the code on the client to reject the server's response if it is not utf-16. The client's original request of supported encodings is https://github.com/microsoft/vscode-languageserver-node/blob/8b3c375adc4fa69f63726ef58d911c8e27b261c5/client/src/common/client.ts#L1690

Mario Carneiro (May 18 2022 at 21:51):

so I think you are right that vscode does not yet actually support any other encodings

Eric Wieser (May 18 2022 at 21:55):

I was hoping I'd be able to look at how the server client handles these other encodings so as to implement it in our server

Eric Wieser (May 18 2022 at 21:55):

So much for that approach

Eric Wieser (May 18 2022 at 22:11):

Tried a patch at https://github.com/leanprover/vscode-lean/pull/301, but can't work out how to test it in gitpod

Eric Wieser (May 18 2022 at 22:15):

It works :tada:

image.png

Yaël Dillies (May 18 2022 at 22:17):

You know we've had this problem for literal months, right? :grinning:

Mario Carneiro (May 18 2022 at 22:22):

I think there are other places the issue arises in the server:

Eric Wieser (May 18 2022 at 22:29):

Yeah, I just found those

Eric Wieser (May 18 2022 at 23:22):

Ok, hopefully fixed

Julian Berman (May 18 2022 at 23:55):

@Rish Vaishnav fixed this sort of thing in lean.nvim awhile back -- https://github.com/Julian/lean.nvim/pull/208

Julian Berman (May 18 2022 at 23:56):

I guess yet another reason Lean 4 can't come soon enough, will be nice if we can share a bit more between all of the plugins.

Eric Wieser (May 19 2022 at 06:03):

Personally I think the lean 3 behavior of counting codepoints is correct, and the fault lies entirely with vscode; but perhaps that's the python user within me talking.

Eric Wieser (May 19 2022 at 07:14):

Turns out that Try this was also broken:

/-𝒜𝒜𝒜𝒜𝒜𝒜𝒜𝒜𝒜𝒜𝒜𝒜𝒜𝒜𝒜𝒜𝒜𝒜𝒜 don't replace me -/ #eval
  tactic.trace "Try this: foo"

This replaces the word don't with foo


Last updated: Aug 03 2023 at 10:10 UTC