[server] Initialize request doesn't handle properly the case where workspaceFolders is null.

[orilahav]

• open a new file in VSCode (via its menu - file:new).
• name the file something.v
• coq-Isp doesn't check the file ("no goals")

It does check the file if I save it and reopen it from the menu.

[Alizter]

I am not able to reproduce on main. Could it be that your goal window hasn't updated? If you press Alt + Enter it should refresh manually.

[ejgallego]

Indeed @orilahav I can't reproduce this, maybe it is an instance of the problem that #287 solves?

[ejgallego]

Hi @orilahav , any news on this?

[orilahav]

Now it fails to start (attached trace).
Perhaps something is broken with my installation if it works for others.
coq_lsp.txt

[ejgallego]

Mmm, that's indeed strange, what version of the extension do you have installed?

Thanks a lot for the log, could you try setting the Coq LSP > Trace setting to verbose?

It could be that for some reasons the settings got corrupted, could you try with a new VS Code profile too?

[A way to do this is to rename / remove .vscode files such as ~/.vscode and the one in the project.

I am improving the error message for the next release by the way, so we could better debug these cases, also we will add platform information.

[ejgallego]

In particular it seems the client is setting client_version to null, which is strange IMO, but could perfectly be a bug in the client config code.

[ejgallego]

In particular this piece of code:

let client_version = context.extension.packageJSON.version;
    const initializationOptions = CoqLspServerConfig.create(
      client_version,
      wsConfig
    );

[ejgallego]

So actions here:

• Improve error message
• Make init more resilient (show on default)
• Print platform

[orilahav]

I'm using version 0.1.6.
verbose log:
Coq_lsp_verbose.txt

[ejgallego]

Hi @orilahav , oh indeed that's a bug in coq-lsp!!

    "workspaceFolders": null

I really need to read the LSP spec more carefully...

Fix to main incoming.

[ejgallego]

While we prepare the fixed release, you should be able to workaround this by using "Open Folder" option in vscode.

Thanks and sorry for all the trouble.