vscoq icon indicating copy to clipboard operation
vscoq copied to clipboard

problem using vscoq on windows 10 via wsl

Open ellisonch opened this issue 5 months ago • 1 comments

I have a normal installation of VS Code on windows 10. I'd like to use the VsCoq extension.

I have set up coq as per the installation instructions on wsl, and everything worked fine.

$ which vscoqtop
/home/ellisonch/.opam/default/bin/vscoqtop

I can't use /home/ellisonch/.opam/default/bin/vscoqtop directly as the vscoq.path setting, as this isn't the "real" path to the executable: image

So, I thought I would be able to use wsl -- /home/ellisonch/.opam/default/bin/vscoqtop as my vscoq.path, since that command works totally fine outside of vscode. Here's me running that command in a normal windows 10 cmd.exe command prompt:

>wsl -- /home/ellisonch/.opam/default/bin/vscoqtop --version
The Coq Proof Assistant, version 8.18.0
compiled with OCaml 4.13.1

However, trying to use wsl -- /home/ellisonch/.opam/default/bin/vscoqtop as my vscoq.path also fails: image

When I click "Go to output", that popup goes away and it shows me this error message:

[Error - 11:27:25 PM] Starting client failed
Launching server using command wsl -- /home/ellisonch/.opam/default/bin/vscoqtop failed.

There aren't any other messages.

Is it possible to do what I want, or is vscoq just unsupported on windows vscode? I'd really like to avoid having a separation installation of vscode inside of wsl just for vscoq. Incidentally, I tried running my windows vscode from inside wsl, and it still fails in the above ways.

ellisonch avatar Jan 19 '24 04:01 ellisonch