Better user feedback when vscoq-language-server installation errors are detected

coq-community / vscoq

A Visual Studio Code extension for Coq [maintainers=@rtetley,@huynhtrankhanh,@thery,@Blaisorblade]

MIT License

333 stars 68 forks source link

Better user feedback when vscoq-language-server installation errors are detected #836

Open ybertot opened 2 months ago

ybertot commented 2 months ago

I have been tinkering with various versions of vscoq, but now I don't manage to get back into a working context. It seems code does not use the version of Coq that is available in the current switch, as displayed in the following illustration, where the shell has a version of coq and vscoq seems to require another version (but I do not know which).

Screenshot at 2024-07-19 09-24-33

gares commented 2 months ago

FYI the $PATH in which vscoq looks for the language server is the $PATH of the shell from which you started vscode. It is not the PATH in the "embedded shell". Maybe this can explain your problems.

gares commented 2 months ago

Bottom line, changing the opam switch in the inner shell may not do "enough"

ybertot commented 2 months ago

I thought I had that part right. The shell I show you in the terminal part of the window has the same path as the shell where the code was started. The reason I show the shell in the window is for a smaller screen capture.

gares commented 2 months ago

Anyway, the message says that vcoqtop was compiled in a switch with ocaml 4.14, but the vo (with a coq compiled with) ocaml 4.13.From the shell it seems you wan to be in the 4.13 switch, I guess it also contains a vscoqtop.

Note that you may have also fixed the path to vscoqtop in the settings of vscoq, in that case changing PATH does not affect the language server that is started. that could also explain it. IIRC in the popup you get by clicking in the bottom bar on "vscoq-lang... 2.1.5" you get the actual path of the language server.

ybertot commented 2 months ago

Yes, this gets closer to a solution. The path shown when I click there explains the problem. This is the cause: the path shows that I am using a nix installed version of coq and a vscoq server from yet another location. All this seems wrong.

ybertot commented 2 months ago

Screenshot at 2024-07-19 11-48-57

ybertot commented 2 months ago

Now fixed with the help of @gares.

F1 -> Preferences:User Settings -> Vscoq:path emptied the text-editing zone at that place.

gares commented 2 months ago

I think we could improve the diagnostic popup in two ways:

tell the user that the Path of the language server is overridden from the settings (an maybe a link to open that UI)
have a warning if the two paths differ:
- here we can see a coq from nix and a vscoq from opam. IMO if the two binaries are not in the same path we could visually indicate the user is in "non standard" installation mode. Maybe a warning icon next to "vscoq-language-server...."

rtetley commented 2 months ago

Sounds good !