search

coq / vscoq

Visual Studio Code extension for Coq
MIT License
343 stars 69 forks source link

vscoq cannot find coqtop when running in a "Remote Development using SSH" context #270

Open intoverflow opened 2 years ago

intoverflow commented 2 years ago

Briefly: vscoq works in Remote Development over SSH out of the box except for one little setting: the path to coqtop when coqtop is installed by opam.

Steps to reproduce

Launch vscode and connect to a remote development server per the instructions in Remote Development using SSH.

Open a remote folder containing a Coq project.

Open a file and start the interactive proof mode by interpreting the first sentence.

What happens

An error notification appears, triggered by failure at this line:

https://github.com/coq-community/vscoq/blob/a3025293e77c2b90c38486cb6fc7503b57c4b2bd/server/src/coqtop/CoqTop8.ts#L239

What's going on?

By default, vscoq assumes coqtop is in the search path (unless an explicit path is given in the settings, of course).

Locally this works fine, even when coqtop is installed to some user-local opam switch. But in a remote context, this strategy fails to locate coqtop.

Workaround

Specify an explicit "Coqtop: Bin Path" in the vscoq extension settings. Note that you can edit your remote settings separately from your local settings, which makes this workaround livable.

image

image

Expected behavior

It would be nice if vscoq could locate coqtop automatically in a remote context. The "server" logic runs on the remote host, so in principle it could query opam env to figure it out.

Relatedly, one might check to see what the ocaml community does about this (if anything).

Blaisorblade commented 2 years ago

This seems related/a duplicate of #257, and the same dev response seems to apply:

Ok, as far as I see, this would require some rewriting, as for example we currently access the file system of the host in the extension using the node package fs. (for example, to look for the _CoqProject).

intoverflow commented 2 years ago

257 might be related, I'm not sure. In that issue, it is reported that vscoq hangs. That's not the case here; here, vscoq works just fine if you specify the path on the (remote) host where coqtop can be located. The only "gotcha" is that you need to specify the path in the extension settings.

The OCaml Platform extension has features for detecting & changing your opam switch. It appears to work in remote mode (see screenshot below). It would be amazing if the vscoq plugin could interact with the ocaml plugin to figure out which switch is active, detect when the switch changes, and locate the tools.

image