Open ybertot opened 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.
Bottom line, changing the opam switch in the inner shell may not do "enough"
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.
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.
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.
Now fixed with the help of @gares.
F1 -> Preferences:User Settings -> Vscoq:path emptied the text-editing zone at that place.
I think we could improve the diagnostic popup in two ways:
Sounds good !
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).