Alex Sanchez-Stern (Mar 16 2023 at 21:32): Alex Sanchez-Stern (Mar 16 2023 at 21:32):I wanted to try the solution Emilio suggested for improving coq-lsp performance, modifying the thread delay call. But to do that I had to switch from the opam distributed coq-lsp back to building from source. However, when I build from source on the main branch, even without any modifications, I'm getting some weird errors.
First, I get a "file not in workspace" error right after running the didOpen request. Which is true, there is no file in the workspace with that name, because my use case is not an editor. But in the past it had been fine with me passing "local1.v" as the filename and arbitrary contents without having to create a file.
From there, I get an error Fleche.Doc.create, internal error: Anomaly \"Uncaught exception Not_found.\"\n. That seems like it could be related to the previous error, though in the past when I've gotten a Not_found exception it didn't have anything to do with files I don't think.
Then, when I try to run any request on the document, like didChange or proof/goals, I then get the error [DocHandle.find]: file local1.v not available. Which would make sense if the didOpen request failed I guess.
These errors are what I get when I opam install the coq-lsp binary into my path. I thought that the environment might be the problem, so I tried dune exec coq-lsp too. But that gets to Done: 85% within a couple of seconds, then hangs there indefinitely.
Emilio Jesús Gallego Arias (Mar 16 2023 at 21:40):Hi @Alex Sanchez-Stern , indeed we were recently discussing what are the valid URIs that we should accept , see https://github.com/ejgallego/coq-lsp/issues/459
It is hard to say more about that concrete case without seeing at least some of the exact protocol calls that you are doing, is the uri in the workspace you have declared (even if the file doesn't exists)
The Not_found is for sure a bug, would be helpful to set debug to true and see where it is failing.
Emilio Jesús Gallego Arias (Mar 16 2023 at 21:40):You can touch local1.v and see if that's the problem meanwhile
Emilio Jesús Gallego Arias (Mar 16 2023 at 21:41):Note that even if you are not an editor, Coq needs to properly set the module Id of anything you open
Emilio Jesús Gallego Arias (Mar 16 2023 at 21:42):that's not very important, but usually recommended, so coq-lsp will always try to map your file name to a corresponding Coq module, that's what coqc does so it can infer foo/var.v goes to MyLib.foo.var module.
Emilio Jesús Gallego Arias (Mar 16 2023 at 21:48):It is very possible that you are seeing two different problems here:
Emilio Jesús Gallego Arias (Mar 16 2023 at 21:49):These errors are what I get when I opam install the coq-lsp binary into my path.
Yeah depending on how you built the thing, if you install coq-lsp for Coq master on a 8.16 env, you are gonna witness weird stuff
Alex Sanchez-Stern (Mar 16 2023 at 21:49):The exact protocols calls I'm using are in the performance measuring script I pasted earlier, here: https://pastebin.com/h6xFGB8d
Alex Sanchez-Stern (Mar 16 2023 at 21:50):Touching local1.v doesn't seem to help
Emilio Jesús Gallego Arias (Mar 16 2023 at 21:51):Mmmm are those valid uris ?
Emilio Jesús Gallego Arias (Mar 16 2023 at 21:51):I'm surprised that ever worked, URI are not filesystem paths
Emilio Jesús Gallego Arias (Mar 16 2023 at 21:51):Maybe in some very ancient version we didn't check that uris were uris, but now we do.
Alex Sanchez-Stern (Mar 16 2023 at 21:52):Re coq version mismatch: Hmm yeah it does seem to be picking up on my 8.16 stdlib ("Configuration loaded from Command-line arguments\n - coqlib is at: /gypsum/work1/brun/sanchezstern/coq-lsp/_build/install/default/lib/coq\n - Modules
[Coq.Init.Prelude] will be loaded by default\n - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope"), but building it's own Coq. Is there a way for me to get it to use my system coq instead?
Alex Sanchez-Stern (Mar 16 2023 at 21:52):Which uri's might not be valid? This script didn't throw any errors in the latest version of coq-lsp on opam, so it can't be that ancient.
Emilio Jesús Gallego Arias (Mar 16 2023 at 21:52):You need to use the 8.16 branch if you want that
Emilio Jesús Gallego Arias (Mar 16 2023 at 21:52):it is quite up-to-date with master
Emilio Jesús Gallego Arias (Mar 16 2023 at 21:53):with the main branch you need to use Coq master branch
Emilio Jesús Gallego Arias (Mar 16 2023 at 21:53):The 85% message it just means coq-lsp is listening for your input
Emilio Jesús Gallego Arias (Mar 16 2023 at 21:53):try to send some input
Emilio Jesús Gallego Arias (Mar 16 2023 at 21:54):An URI is usually file:///absolute/path
Emilio Jesús Gallego Arias (Mar 16 2023 at 21:54):LSP requires URIs (they are defined in corresponding RFC)
Alex Sanchez-Stern (Mar 16 2023 at 21:55):Ah huh. So if there's no real path, file:///local1.v should do the trick?
Alex Sanchez-Stern (Mar 16 2023 at 21:55):I was having some trouble building the 8.16 branch before, but I'll try again on a fresh switch.
Emilio Jesús Gallego Arias (Mar 16 2023 at 21:55):Actually I see I introduced a bug https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#uri
Emilio Jesús Gallego Arias (Mar 16 2023 at 21:55):rootPath is a path not an URI
Emilio Jesús Gallego Arias (Mar 16 2023 at 21:56):this is probably what you are seeing
Alex Sanchez-Stern (Mar 16 2023 at 21:57):Okay I've got some more things to try, will take a while creating a new switch though
Alex Sanchez-Stern (Mar 16 2023 at 21:57):Oh wait, what do you mean the path thing is what I'm seeing? You're saying that "." should be a valid rootPath according to the spec, but the implementation in coq-lsp tries to parse it as a URI and fails?
Emilio Jesús Gallego Arias (Mar 16 2023 at 22:03):Yes, that's a new bug, I'd suggest you just use rootURI
Emilio Jesús Gallego Arias (Mar 16 2023 at 22:04):relative paths seem too brittle to me, I'm gonna add a warning recommending that the path is absolute
Emilio Jesús Gallego Arias (Mar 16 2023 at 22:06):But the real bug seems you are not passing an URI in didOpen
Emilio Jesús Gallego Arias (Mar 16 2023 at 22:26):I've added a test that checks that opening a non-existing file works fine.
Emilio Jesús Gallego Arias (Mar 16 2023 at 23:12):Def can't reproduce the problems with your example with the equivalent tests in the test-suite
Emilio Jesús Gallego Arias (Mar 16 2023 at 23:13):Yeah so that error you are seeing is from the prelude failing to load and Coq emitting a quite strange error message.
Alex Sanchez-Stern (Mar 16 2023 at 23:34):Hmm when I try to build on the v8.16 branch to fix the prelude problem, I get a bunch of compile errors. Unbound type constructor Metasyntax.where_decl_notation, Unbound value Flags.set_native_compiler, Unbound value Reduction.hnf_prod_applist_assum, Unbound module LStream, and one type error.
Alex Sanchez-Stern (Mar 16 2023 at 23:36):I've fixed the uri stuff in the test script, so when I can build I'll have that in the test.
Alex Sanchez-Stern (Mar 16 2023 at 23:52):Okay I went ahead and switched back to the main branch to see what impact fixing the URI's would have. Here's the fixed URI's version of the script: https://pastebin.com/RXFLPbCH. Once the URI's are fixed, I don't get the "file not in workspace" message, but I still get the "Not_found" anomaly on the didOpen request, and [DocHandle.find]: file file:///local1.v not available. So those errors seem to be because of the mismatched prelude, so I'll need to figure out how to build the project on the 8.16 branch
Alex Sanchez-Stern (Mar 16 2023 at 23:58):Oh the build errors look like they were just an artifact of switching branches, after a good dune clean it builds
Emilio Jesús Gallego Arias (Mar 17 2023 at 02:45):Glad to hear it is working fine now, build will become soon a bit better.
Last updated: Apr 20 2024 at 14:01 UTC