When you start coq-lsp, after the "server initialized" message, it sends a message that is either "Configuration loaded from <filename>..." or "Configuration loaded from command-line arguments...". What makes it decide to pick one or the other? I thought it might look for a _CoqProject file in a canonical place, and load it if it exists, otherwise fall back on command line. But on my local machine, it prints "Configuration loaded from <working-dir>/_CoqProject", even though that _CoqProject file doesn't exist.
What coq-lsp version is this @Alex Sanchez-Stern ?
The criteria is to look for a _CoqProject file in each of the workspace folders
let guess ~debug ~cmdline ~dir =
let cp_file = Filename.concat dir "_CoqProject" in
if Sys.file_exists cp_file then
workspace_from_coqproject ~cmdline ~debug cp_file
else workspace_from_cmdline ~debug ~cmdline
You can set the server trace level to verbose to get more info
I wouldn't be surprised if we have bugs tho, we finally have a test infra and a small test suite, but we are not testing CoqProject setup
didn't find the cycles, if anyone would like to add a small test for that it would be super-appreciated
The ~dir
parameter is derived from the standard (if we didn't mess things up), that is to say:
workspaceFolders
if presentrootUri
rootPath
Using workspace folders you can support projects that have multiple _CoqProject files
[there is a minor problem due to findlib state, but that should not impact most people, the problem has its own issue so we will fix it]
Ah yeah, it does seem like I found a bug, but possibly only in the messages. Tried it both on coq-lsp 0.1.5, and the version of coq-lsp 0.1.7 on the v8.15 branch. It looks like what is happening is that it checks the workspace folder for a _CoqProject file to determine whether to load from a project file or not. But then when it prints "Configuration loaded from...", it reports as the path for the project file the current directory. So, for instance, if I set the workspace dir to "$PWD/../CompCert/", and there is a _CoqProject file in that folder, it'll print "Loading configuration file from $PWD/_CoqProject" instead of from $PWD/../CompCert/_CoqProject. Not sure if that means it's actually reading the correct file, and just reporting it wrong, or if it checks for the file in the right place, then if it exists, reads it from the wrong place.
Oh yes you are correct, we forgot to update the message!
the message is indeed non-sense
see the code:
let kind = Filename.concat (Sys.getcwd ()) "_CoqProject" in
Oh yup, that would do it haha
let me fix that (and backport to 8.15]
Great, thanks!
Yeah that message is from a very old version we forgot to update it
lack of tests ....
https://github.com/ejgallego/coq-lsp/pull/444
Thanks to you!
It was reading the right file tho
so if you ignore the message you should be able to continue using coq-lsp and likely find more bugs
Great will do! I'm investigating something right now where the same coq-lsp version seems to be behaving differently on different machines, trying to minimize and see if it's a bug.
Thanks!
8.15 branch will have worse incremental behavior as it needs an updated serlib version to properly track Ast modulo location-only changes, keep that in mind
I've opened an issue to track when that will be solved
Okay good to know. Now that I know I can build Compcert on 8.16 by passing configure options I'll probably switch back to the main release soon.
Last updated: Mar 29 2024 at 05:40 UTC