VSCode puts error lines in the wrong place

Stream: general

[Eric Wieser]

This code:

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

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

[Eric Wieser]

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]

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

[Mario Carneiro]

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]

I thought Lean 3 didn't use LSP?

[Eric Wieser]

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

[Mario Carneiro]

ah, fair point

[Eric Wieser]

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

[Arthur Paulino]

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

[Mario Carneiro]

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

[Mario Carneiro]

using more script letters just makes the problem worse

[Eric Wieser]

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]

This rabbit hole started with a spike trap

[Eric Wieser]

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

[Mario Carneiro]

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

[Eric Wieser]

UTF-16 is the worst

[Eric Wieser]

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

[Mario Carneiro]

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

[Eric Wieser]

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]

...and yes, the acronym is intentional

[Mario Carneiro]

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

[Mario Carneiro]

is that for the server or the client?

[Eric Wieser]

I can't work out where the vscode client is

[Eric Wieser]

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

[Mario Carneiro]

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]

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]

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]

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

[Eric Wieser]

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]

So much for that approach

[Eric Wieser]

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]

It works :tada:

image.png

[Yaël Dillies]

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

[Mario Carneiro]

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

• https://github.com/leanprover/vscode-lean/blob/8ad0609f560f279512ff792589f06d18aa92fb3f/src/hover.ts#L12
• https://github.com/leanprover/vscode-lean/blob/8ad0609f560f279512ff792589f06d18aa92fb3f/src/definition.ts#L12
• https://github.com/leanprover/vscode-lean/blob/8ad0609f560f279512ff792589f06d18aa92fb3f/src/completion.ts#L45
• https://github.com/leanprover/vscode-lean/blob/8ad0609f560f279512ff792589f06d18aa92fb3f/src/tacticsuggestions.ts#L57
• https://github.com/leanprover/vscode-lean/blob/8ad0609f560f279512ff792589f06d18aa92fb3f/src/diagnostics.ts#L60

[Eric Wieser]

Yeah, I just found those

[Eric Wieser]

Ok, hopefully fixed

[Julian Berman]

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

[Julian Berman]

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]

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]

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