vscoq
vscoq copied to clipboard
problem using vscoq on windows 10 via wsl
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:
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:
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.