[lsp] Fix bug when retrieving URIs from document params

[ejgallego]

That made the coq/saveVo fail with an invalid parsing error.

The issue was that when we handle generically the requests that need to wait for the document to be completed, we were retrieving the uri parameter using the de-serializer for the TextDocumentIdentifier data-type, however both coq/getDocument and coq/saveVo use VersionedTextDocumentIdentifier.

As the JSON parser finds this extra param, it fails. We solve this making the parser in this case no strict, but further hardening is needed at this level.

Thanks to Théo Zimmerman for the report and help with debugging this issue.

[Zimmi48]

FWIW, I tried updating coq-lsp to the version in this PR and still got (this is with Coq version 8.18+rc1):

[Trace - 2:19:07 PM] [process_queue]: Serving Request: coq/saveVo
[Trace - 2:19:07 PM] [process_queue]: bt=false
[Trace - 2:19:07 PM] [print_exn [OCaml]]: Invalid_argument("result is Error _")
[Trace - 2:19:07 PM] [print_exn [Coq  ]]: Anomaly "Uncaught exception Invalid_argument("result is Error _")."
Please report at http://coq.inria.fr/bugs/.

[ejgallego]

@Zimmi48 did you restart coq-lsp from VsCode ? That error message certianly seems from the older version (I've removed the Result.get_ok in this PR, which was responsible for the Invalid_argument)

Note that this PR targets Coq master, but the backport should be trivial.

[ejgallego]

(To be more sure, you can enable Debug in the preferences for coq-lsp in VsCode)

[Alizter]

In VSCode its

Ctrl + p

and then

> restart coq

and you'll find the command.

[Zimmi48]

I hadn't indeed. Now that I have, here is the error I get (still an anomaly, but with a trace):

[Trace - 2:51:00 PM] [process_queue]: Serving Request: coq/saveVo
[Trace - 2:51:00 PM] [process_queue]: bt=true
[Trace - 2:51:00 PM] [print_exn [OCaml]]: Invalid_argument("result is Error _")
[Trace - 2:51:00 PM] [print_exn [Coq  ]]: Anomaly "Uncaught exception Invalid_argument("result is Error _")."
Please report at http://coq.inria.fr/bugs/.
Raised at Stdlib.invalid_arg in file "stdlib.ml", line 30, characters 20-45
Called from Stdlib__Result.get_ok in file "result.ml" (inlined), line 21, characters 45-76
Called from Controller__Lsp_core.Helpers.get_uri in file "controller/lsp_core.ml", line 41, characters 6-100
Called from Controller__Lsp_core.do_document_request in file "controller/lsp_core.ml", line 303, characters 12-34
Called from Controller__Lsp_core.dispatch_request in file "controller/lsp_core.ml" (inlined), line 425, characters 2-35
Called from Controller__Lsp_core.dispatch_message in file "controller/lsp_core.ml", line 432, characters 4-46
Called from Controller__Lsp_core.dispatch_or_resume_check in file "controller/lsp_core.ml", line 471, characters 9-47
Called from Controller__Lsp_core.dispatch_or_resume_check in file "controller/lsp_core.ml", line 475, characters 11-53

[Trace - 2:51:00 PM] [print_bt  [OCaml]]: Raised at Stdlib.invalid_arg in file "stdlib.ml", line 30, characters 20-45
Called from Stdlib__Result.get_ok in file "result.ml" (inlined), line 21, characters 45-76
Called from Controller__Lsp_core.Helpers.get_uri in file "controller/lsp_core.ml", line 41, characters 6-100
Called from Controller__Lsp_core.do_document_request in file "controller/lsp_core.ml", line 303, characters 12-34
Called from Controller__Lsp_core.dispatch_request in file "controller/lsp_core.ml" (inlined), line 425, characters 2-35
Called from Controller__Lsp_core.dispatch_message in file "controller/lsp_core.ml", line 432, characters 4-46
Called from Controller__Lsp_core.dispatch_or_resume_check in file "controller/lsp_core.ml", line 471, characters 9-47
Called from Controller__Lsp_core.dispatch_or_resume_check in file "controller/lsp_core.ml", line 475, characters 11-53

[Zimmi48]

Note that this PR targets Coq master, but the backport should be trivial.

I had assumed that if it built fine with 8.18, then it meant that it was compatible with it. But I can try to use Coq master instead if that's helpful.

[ejgallego]

I had assumed that if it built fine with 8.18, then it meant that it was compatible with it. But I can try to use Coq master instead if that's helpful.

That's a valid assumption, modulo the submodules, but that should work.

Called from Controller__Lsp_core.Helpers.get_uri in file "controller/lsp_core.ml", line 41, characters 6-100

Mmm, the call to get_ok just after this one is removed in this PR, so it seems your vsCode is still not picking the right path to the new binary?

[ejgallego]

By the way I discussed with @bhaktishh about improving the build setup (on Zulip)

We hope to make things easier, for example it would be great to have a nix command to easily test a coq-lsp PR + all the required developments.

[In general testing coq-lsp is a bit more complex because you need to rebuild the whole chain until the .v file you need to test quickly]

[Zimmi48]

I am positive that the version of coq-lsp (server part) that I have installed now in my Gitpod workspace is indeed the one from this branch (I checked the Nix derivation and the source that was used for the build). However, it is possible that in my earlier test, the VS Code extension was picking the old server version instead of the new one in PATH. After reloading the Windows, I get a different error:

[Error - 4:23:31 PM] Coq LSP Server client: couldn't create connection to server.
Launching server using command coq-lsp failed. Error: spawn coq-lsp ENOENT

Could it be because I'm using the coq-lsp VS Code extension from the marketplace and this one is no longer compatible with the coq-lsp server from this branch?

[ejgallego]

@Zimmi48 confirmed this works, we still have to think of a better strategy to handle subtypes in the protocol.