[lsp] Requests input positions are not translated uniformly, and often handled as UTF-8 codepoints instead of UTF-16

[ejgallego]

Title is descriptive, this was laziness on my part, but kinda urgent to fix if we want to be production-ready.

[Alizter]

When does this become a problem? AFAIK it only shows issues on characters with strange East-asian character widths right?

[ejgallego]

Quite a few math unicode characters have different length codepoints in UTF-8 and UTF-16, you can see examples/utf16.v , hover is shifted one position due to \cal{U} being length 1 in UTF-16 and lenght 2 in UTF-8

[Alizter]

Right, but confusingly all unicode characters have a property called East asian width which isn't only specific to east asian characters. https://www.unicode.org/reports/tr11/tr11-8.html Some characters have an ambiguous width which means its not obvious how to handle hover.

I just wanted to share, I'm not particularly sure how to handle this as I had the unfortune to come across it myself for something else.

[ejgallego]

I see what you mean, but that's for the editor to handle right, how would that affect the server?

[Alizter]

Right, but that means we cannot make assumptions on "character count" based on the positions. If the positions are adjusted to account for multiple unicode characters in the same position then there are more characters than the location would indicate. I'm not sure if we do any such logic in the server.

[ejgallego]

I'm afraid I cannot understand what you are talking about. You seem to be talking about display; this issue is not about display, but about code points in a text buffer.

[Alizter]

@ejgallego Nevermind then, I think I must be confused about something.

[ejgallego]

I'll try to explain here what the LSP server needs to do w.r.t. unicode, which by the way is pretty annoying, tho newer versions of the protocol try to get it fixed.

In Coq case, we have 3 versions of positions inside a document, in terms how we understand it: UTF-8 code units, UTF-16 code units; UTF characters. The last one is not used anywhere, except for example to show real "line lenght", etc...

But positions in LSP are measured in terms of "UTF-16 code units", see https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocuments

I'm gonna assume we start counting at 0.

So imagine for example a buffer with:

Definition 𝒰 := 3.

Coq needs to encode this as UTF-8, so in this case, the character at position 17 is a dot, but in utf-8 code units corresponds to and encoding of 0xF0 0x9D 0x92 0xB0, so the dot lives in position 20 for Coq.

c.f. https://www.compart.com/en/unicode/U+1D4B0

However, if we want to report a diagnostic for the dot position, we need to report the code unit in UTF-16, in this case the encoding of \mathcal{U} is 0xD835 0xDCB0, thus the position 18.

However I was sloppy and we are reporting the real position, 17, as we are converting Coq positions to real Unicode position. Thus VSCode thinks the diagnostic is one position back.

You can see this effect if you try examples/utf_16.v.

So instead of converting the Coq positions to true Unicode positions, we need to convert them to UTF-16 code units.

So why is this taking me long to fix? Because we need to be very careful about performance, if we introduce some spurious conversion we will have a hit.

[Alizter]

Thanks for the explanation, that clears it up! If you go for a naive fix and notice the performance is hit, you could add try to memoize conversions to perhaps save some repeated converisons and make it more performant.

[ejgallego]

In some cases you need a cache, but I think if we are careful we can do without it; we just need some discipline with types, but we got most stuff in place already!

Note that things are working now for some characters purely by chance: coq-lsp reports the real unicode position, as in UTF-16 many common characters do indeed take a single two-bytes entry, things coincide, but that's purely by chance.

[ejgallego]

Another problem we have with this conversion UTF-16 / UTF-8 is with #497 , right now the conversions complicate quite a bit having an efficient diff algorithm, so Keep It Simple wins for now.