search

coq / vscoq

Visual Studio Code extension for Coq
MIT License
335 stars 68 forks source link

VsCoq running, installed on Windows WSL using OPAM, but can't run proof view #921

Closed Mushow closed 1 week ago

Mushow commented 1 week ago

Hi everyone, I tried using Alt+Down, Alt+Right, nothing works, whenever I run Ctrl+Shift+P and click on "Coq: Display Proof View", nothing shows up.

I already tried re-installing, enabling/disabling the extension and also restarted VS Code a couple of times.

mush@DESKTOP-VOKIC6H:~$ coqidetop.opt -v
The Coq Proof Assistant, version 8.20.0
compiled with OCaml 4.14.0
mush@DESKTOP-VOKIC6H:~$

Output:

[Toolchain] Searching for vscoqtop
[Toolchain] Found path: /home/mush/.opam/4.14.0/bin/coqtop
VsCoq initialised

Has any body run into this before?

rtetley commented 1 week ago

Can you tell me which version of the server / extension you have ? It seems like they are not in sync. This typically happens when the server has a higher version then the extension.

Mushow commented 1 week ago

image VsCoq is on the latest version and the server I suppose is on 8.20?

opam list
[...]
coq                   8.20.0      The Coq Proof Assistant
coq-core              8.20.0      The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib            8.20.0      The Coq Proof Assistant -- Standard Library
coqide-server         8.20.0      The Coq Proof Assistant, XML protocol server
rtetley commented 1 week ago

The server version is independent of the Coq-version. In the list above I don't see vscoq-language-server ?

rtetley commented 1 week ago

You should be notified that the server is not up to date... But I've got the feeling that the server launch failed before it could send version info... Could you check that vscoq-language-server is also on version 2.2.1 ?

Mushow commented 1 week ago

I do not find that package under opam list.

rtetley commented 1 week ago

This is very suspicious, if you don't have the server installed somehow, vscoq should notify you. Could you search for vscoqtop in your shell ?

which vscoqtop
Mushow commented 1 week ago

mush@DESKTOP-VOKIC6H:~$ which vscoqtop /home/mush/.opam/4.14.0/bin/vscoqtop

vscoq-language-server 2.2.1 VSCoq language server

rtetley commented 1 week ago

Hi everyone, I tried using Alt+Down, Alt+Right, nothing works, whenever I run Ctrl+Shift+P and click on "Coq: Display Proof View", nothing shows up.

I already tried re-installing, enabling/disabling the extension and also restarted VS Code a couple of times.

mush@DESKTOP-VOKIC6H:~$ coqidetop.opt -v
The Coq Proof Assistant, version 8.20.0
compiled with OCaml 4.14.0
mush@DESKTOP-VOKIC6H:~$

Output:

[Toolchain] Searching for vscoqtop
[Toolchain] Found path: /home/mush/.opam/4.14.0/bin/coqtop
VsCoq initialised

Has any body run into this before?

Wait I just noticed that your log here says [Toolchain] Found path: /home/mush/.opam/4.14.0/bin/coqtop which is also suspicious... It should not be coqtop but vscoqtop. Did you perhaps set the path manually ? In which case could you just remove the setting or set it to /home/mush/.opam/4.14.0/bin/vscoqtop ?

Mushow commented 1 week ago

Now it works.. thanks.. I thought I had to set it manually. Thanks a lot!