siegebell/vscoq

Error when trying to run Coq server

Closed this issue · 2 comments

I have coq installed and can run coqc/coqtop fine. But when I try to run VsCoq, I get an error about the arguments.

System is a MacBook Pro 13 inch, 2017, 2.3 GHz i5, 8 gb ram, macOS High Sierra (10.13.4)
Coq version is 8.7.1 and Ocaml version is 4.06.0

Here is the output in VSCode when I try to "step forward"

"
Coq Language Server: process.version: v7.9.0, process.arch: x64}
Loaded project at /Users/mike/Documents/coding/X/Y/Other/coq
Changed path to:
Listening at ::1:50558
Listening at ::1:50559
Listening at ::1:50560
Listening at ::1:50561

qualid: Let
reset
exec: coqtop -v
Detected coqtop version 8.7.1
exec: coqtop -main-channel ::1:50558:50559 -control-channel ::1:50561:50560 -ideslave -async-proofs on
coqtop started with pid 67402
coqtop-stderr: Error: host:portr:portw or stdfds expected after option -main-channel

coqtop exited with code: 1
coqtop closed with code: 1
onCoqClosed(coqtop closed with code: 1)
"

I tried to add "-main-channel stdfds" to the arguments, but because they're evaluated in order, it still throws an error before it can get to there. Did I set up VSCoq wrong, or is this something else.

It seems that Coq doesn't support IPV6 addressed, you should either patch the plugin to send 127.0.0.1 in place of ::1 or submit a bug report to Coq [and then use master].

Lol nice. I ended up just using Tuareg Mode (Emacs) instead. Thanks for the help tho!