Follow LSP and treat positions as UTF16 code units

[ineol]

Fixes #531

This is probably only a partial as it only affects completion requests.

The translation should probably be done in lsp_core.ml, in do_position_request for example. But then, what should we do when the position is out of bound? pass None to the implementation? or terminate directly the request?

[ejgallego]

Thanks a lot @ineol , indeed we need to fix this at the core, I have a branch but didn't get enough time to finish it.

The changes needed are a bit deep, actually.

The convention is that Lang.Point.t positions are unicode chars, and Coq.Pos.t positions are Coq byte offsets.

Turns out this is wrong, Lang.Point.t should be protocol-level positions, in this case, not unicode points, but UTF-16 points. That's not hard to do, however it is a bit harder to be sure we do the conversion efficiently.

So we need to update all the conversion functions so they are more abstract (so we can still do Coq to several codepoints); newer versions of LSP do allow for the client/server comms to be in UTF-8.

I'll merge the workaround for now; and hopefully we get to fix the whole setup first.

[ejgallego]

But then, what should we do when the position is out of bound? pass None to the implementation?

I need to check the LSP specification carefully, but my impression is that if the client sends an out-of-bounds positions, the request should indeed fail with the error code "invalid argument".

As far as I can see, when that situation would happen, that'd always be a client bug, right?

[ineol]

So we need to update all the conversion functions so they are more abstract (so we can still do Coq to several codepoints); newer versions of LSP do allow for the client/server comms to be in UTF-8.

Note that VSCode does not implement this extension as far as I understand microsoft/vscode-languageserver-node#1224

I think both emacs/eglot and neovim lsp clients support encoding negotiation.

[ejgallego]

So we need to update all the conversion functions so they are more abstract (so we can still do Coq to several codepoints); newer versions of LSP do allow for the client/server comms to be in UTF-8.

Note that VSCode does not implement this extension as far as I understand microsoft/vscode-languageserver-node#1224

I think both emacs/eglot and neovim lsp clients support encoding negotiation.

Yes, I assume we will need to support the UTF-16 setup for a long time; I'd like to support encoding negotiation tho as for Coq using UTF-8 will be more efficient; maybe it doesn't matter too much tho, but I'm unsure, there are very very large Coq files out there.

[ineol]

But then, what should we do when the position is out of bound? pass None to the implementation?

I need to check the LSP specification carefully, but my impression is that if the client sends an out-of-bounds positions, the request should indeed fail with the error code "invalid argument".

As far as I can see, when that situation would happen, that'd always be a client bug, right?

At least in the section Position it says:

If the character value is greater than the line length it defaults back to the line length.

[ejgallego]

But then, what should we do when the position is out of bound? pass None to the implementation?

I need to check the LSP specification carefully, but my impression is that if the client sends an out-of-bounds positions, the request should indeed fail with the error code "invalid argument".
As far as I can see, when that situation would happen, that'd always be a client bug, right?

At least in the section Position it says:

If the character value is greater than the line length it defaults back to the line length.

Thanks a lot for checking this, actually we already do that, but only because it covers the case where we are at EOL.

Let's then cap the column in that way, most of the code already behaves like this.

[ejgallego]

Hi @ineol , I did fix a few compile problems and pushed to your branch, still need to add a wrapper for the missing functions in older OCaml.

[ineol]

Hi @ineol , I did fix a few compile problems and pushed to your branch

thanks!

still need to add a wrapper for the missing functions in older OCaml.

So should I copy-paste from Stdlib in a compatibility module until the minimum supported version is 4.14? they are both LGPL so it should be fine.

[ejgallego]

Yup! I think we can put them in the Utf8 module, with clear attribution until we bump to 4.14

[ineol]

It's done. I didn't manage to test with an old ocaml version but according to the doc it should be fine.

[ejgallego]

Thanks!

I will fix the two remaining CI errors and merge, then I'll propagate your fix to other parts, it was very useful!

[ejgallego]

I've added a changelog, lowered the alcotest dep so win CI is happy, and placed the tests under test. Hopefully CI passes now.

I've also added an example that showcases other parts of the codebase where locations are incorrectly treated as UTF-8 (on hover, for diagnostics).

@ineol I was wondering if the kind of testing we are doing here wouldn't be better served by ppx_inline_test ?

I will for now keep the tests as they are, but something to keep in mind as we rework this code a bit.