Stream: coq-lsp

Topic: Configuration loaded


view this post on Zulip Alex Sanchez-Stern (Mar 03 2023 at 20:09):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 03 2023 at 20:14):

What coq-lsp version is this @Alex Sanchez-Stern ?

The criteria is to look for a _CoqProject file in each of the workspace folders

view this post on Zulip Emilio Jesús Gallego Arias (Mar 03 2023 at 20:15):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 03 2023 at 20:16):

You can set the server trace level to verbose to get more info

view this post on Zulip Emilio Jesús Gallego Arias (Mar 03 2023 at 20:17):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 03 2023 at 20:17):

didn't find the cycles, if anyone would like to add a small test for that it would be super-appreciated

view this post on Zulip Emilio Jesús Gallego Arias (Mar 03 2023 at 20:19):

The ~dir parameter is derived from the standard (if we didn't mess things up), that is to say:

view this post on Zulip Emilio Jesús Gallego Arias (Mar 03 2023 at 20:19):

Using workspace folders you can support projects that have multiple _CoqProject files

view this post on Zulip Emilio Jesús Gallego Arias (Mar 03 2023 at 20:20):

[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]

view this post on Zulip Alex Sanchez-Stern (Mar 03 2023 at 20:22):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 03 2023 at 20:24):

Oh yes you are correct, we forgot to update the message!

view this post on Zulip Emilio Jesús Gallego Arias (Mar 03 2023 at 20:24):

the message is indeed non-sense

view this post on Zulip Emilio Jesús Gallego Arias (Mar 03 2023 at 20:25):

see the code:

view this post on Zulip Emilio Jesús Gallego Arias (Mar 03 2023 at 20:25):

  let kind = Filename.concat (Sys.getcwd ()) "_CoqProject" in

view this post on Zulip Alex Sanchez-Stern (Mar 03 2023 at 20:25):

Oh yup, that would do it haha

view this post on Zulip Emilio Jesús Gallego Arias (Mar 03 2023 at 20:25):

let me fix that (and backport to 8.15]

view this post on Zulip Alex Sanchez-Stern (Mar 03 2023 at 20:25):

Great, thanks!

view this post on Zulip Emilio Jesús Gallego Arias (Mar 03 2023 at 20:25):

Yeah that message is from a very old version we forgot to update it

view this post on Zulip Emilio Jesús Gallego Arias (Mar 03 2023 at 20:25):

lack of tests ....

view this post on Zulip Emilio Jesús Gallego Arias (Mar 03 2023 at 20:28):

https://github.com/ejgallego/coq-lsp/pull/444

view this post on Zulip Emilio Jesús Gallego Arias (Mar 03 2023 at 20:28):

Thanks to you!

view this post on Zulip Emilio Jesús Gallego Arias (Mar 03 2023 at 20:29):

It was reading the right file tho

view this post on Zulip Emilio Jesús Gallego Arias (Mar 03 2023 at 20:29):

so if you ignore the message you should be able to continue using coq-lsp and likely find more bugs

view this post on Zulip Alex Sanchez-Stern (Mar 03 2023 at 20:30):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 03 2023 at 20:33):

Thanks!

view this post on Zulip Emilio Jesús Gallego Arias (Mar 03 2023 at 20:34):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 03 2023 at 20:34):

I've opened an issue to track when that will be solved

view this post on Zulip Alex Sanchez-Stern (Mar 03 2023 at 20:38):

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