coq-lsp connection errors showing in non-Coq projects

[dariusf]

Thank you for developing coq-lsp!

I use many opam switches, most of which don't have coq-lsp installed.

With the new activation criteria (#737), when I open a project unrelated to Coq, e.g. containing only LaTeX and a Markdown readme, the extension activates and shows an error message about failing to connect to the LSP server, along with a rather obtrusive, persistent red section in the status bar.

Would it be possible to not activate the extension, or perhaps not show errors, if connecting to coq-lsp fails because it isn't installed?

[ejgallego]

Hi @dariusf , I'm sorry to hear of this problem, it shouldn't happen!

Do you mind sharing coq-lsp client and server versions, and how to reproduce?

I was not able to reproduce this problem in my testing, but indeed I am sure there are cases we didn't anticipate.

[ejgallego]

By the way, I agree this "red button" is annoying, in fact I have the same problem with rust-analyzer being red often, and I'm not surprised as we got inspired by rust-analyzer when designing the toolbar.

We will likely remove this button and favor the new LanguageStatusItem API.

[dariusf]

No worries, and good to know! 😄

Here's my environment and the steps I took:

VS Code version

``` Version: 1.89.1 Commit: dc96b837cf6bb4af9cd736aa3af08cf8279f7685 Date: 2024-05-07T05:14:24.611Z (4 wks ago) Electron: 28.2.8 ElectronBuildId: 27744544 Chromium: 120.0.6099.291 Node.js: 18.18.2 V8: 12.0.267.19-electron.0 OS: Darwin x64 22.6.0 ```

Coq LSP VS Code extension: v0.1.10

• opam switch 5.1.0; coq-lsp server is not installed
• code . in a directory with just an empty test.md file
• Open the file in VS Code
• The extension activates with Coq LSP Server client: couldn't create connection to server.

Coq LSP Server Events after

``` [Error - 18:20:03] Coq LSP Server client: couldn't create connection to server. Launching server using command coq-lsp failed. Error: spawn coq-lsp ENOENT ```

[ejgallego]

I see thanks, indeed I can reproduce. Will work on a fix ASAP.

For now you can workaround this by right clicking on the toolbar, and selecting hide. Use instead the new indicator in the language section (bottom-right corner {} symbol, then pin)

[dariusf]

Great, thank you!