VSCoq doesn't seem to work properly (doesn't interpret code).

[nothingnesses]

Reproduction

(click to expand)

Save the following into ~/a_days_of_the_week.v:

Inductive day : Type :=
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday
  | sunday.

Definition next_weekday (d:day) : day := 
  match d with
    | monday => tuesday
    | tuesday => wednesday
    | wednesday => thursday
    | thursday => friday
    | friday => monday
    | sunday => monday
    | saturday => monday
  end.

Compute (next_weekday friday).

Open with VSCode:

$ code-oss ~/a_days_of_the_week.v
node[27056]: pthread_create: Invalid argument
$

View, Open View..., Coq Language Server:

node[27742]: pthread_create: Invalid argument
Coq Language Server: process.version: v12.8.1, process.arch: x64}
Loading project with no root directory
Changed path to: 

Run command "Coq: Interpret to End" (Alt-End), then view output:

node[27742]: pthread_create: Invalid argument
Coq Language Server: process.version: v12.8.1, process.arch: x64}
Loading project with no root directory
Changed path to: 
starting coqtop
exec: coqtop -v
Detected coqtop version 8.11.2
Coqtop version parsed into semver version 8.11.2

System information

(click to expand)

$ uname --all
Linux a 5.4.42_1 #1 SMP PREEMPT Thu May 21 07:35:36 UTC 2020 x86_64 GNU/Linux
$ coqc -v
The Coq Proof Assistant, version 8.11.2 (May 2020)
compiled on May 15 2020 18:09:59 with OCaml 4.10.0
$ code-oss -v
node[8722]: pthread_create: Invalid argument
1.45.1
Unknown commit
x64
$ code-oss --list-extensions --show-versions | rg coq
node[21916]: pthread_create: Invalid argument
[email protected]
$

Other information

(click to expand)

Compiling and running the code through coqc works fine:

$ exa -l | rg a_days_of_the_week
.rw-r--r--  381 a 28 May 0:10 a_days_of_the_week.v
$ coqc ~/a_days_of_the_week.v
     = monday
     : day
$ exa -l | rg a_days_of_the_week
.rw-r--r-- 1.4k a 28 May 0:14 a_days_of_the_week.glob
.rw-r--r--  381 a 28 May 0:10 a_days_of_the_week.v
.rw-r--r-- 4.0k a 28 May 0:14 a_days_of_the_week.vo
.rw-r--r--    0 a 28 May 0:14 a_days_of_the_week.vok
.rw-r--r--    0 a 28 May 0:14 a_days_of_the_week.vos
$

[Coda-Coda]

For what it's worth, I just tried to reproduce your example and got no errors, VSCoq performed as expected. I am currently using Coq 8.9.1 on MacOS Catalina with VSCode 1.45.1 and VSCoq 0.3.1.

[nothingnesses]

Apparently my distro's coq package doesn't include coqide (but it does include coqidetop). Is coqide required for VSCoq?

[maximedenes]

In principle, only coqidetop.opt should be required. Is it provided by your distro's package? Make sure it is either in your path, or in the path selected in the VsCoq preferences.

[nothingnesses]

In principle, only coqidetop.opt should be required. Is it provided by your distro's package? Make sure it is either in your path

coqidetop.opt does appear to be in my $PATH:

$ echo $PATH
/home/a/.local/bin:/home/a/anaconda3/bin:/home/a/node_modules/.bin:/home/a/.cargo/bin:/home/a/.local/bin:/home/a/anaconda3/bin:/home/a/node_modules/.bin:/home/a/.cargo/bin:/usr/local/bin:/bin:/usr/bin:/usr/local/sbin:/usr/sbin:/sbin
$ whereis coqidetop.opt
coqidetop: /usr/bin/coqidetop /usr/bin/coqidetop.opt
$

, or in the path selected in the VsCoq preferences.

Not sure exactly which preference you're pertaining to here, but I haven't manually configured any preferences after I installed VSCoq. If you meant the preference "Coqtop: Bin Path", its field is currently blank.

[PhyX-Meow]

I have exactly the same problem, the extension tells me "coqtop is not running" and do nothing. I'm using Manjaro linux in wsl2.

[TheoWinterhalter]

I have exactly the same problem, the extension tells me "coqtop is not running" and do nothing. I'm using Manjaro linux in wsl2.

Are you having the same problem that it complains about "invalid argument"? "Coqtop is not running" is not an error, it's just stating the fact that you haven't started coqtop yet. Have you tried stepping in the file? Like Coq: Step Forward (obtained after opening the command palette)?

[PhyX-Meow]

I have exactly the same problem, the extension tells me "coqtop is not running" and do nothing. I'm using Manjaro linux in wsl2.

Are you having the same problem that it complains about "invalid argument"? "Coqtop is not running" is not an error, it's just stating the fact that you haven't started coqtop yet. Have you tried stepping in the file? Like Coq: Step Forward (obtained after opening the command palette)?

Oh, it now works perfectly. I thought it was an error. Thanks very much.

[liuxingpeng520521]

How to solve the error "coqtop is not running" ? I've been haunted for a long time.

[chaptercheng]

How to solve the error "coqtop is not running" ? I've been haunted for a long time.

I met the same problem yesterday and solved it. The simplest way is just setting the priority of ipv4 higher than ipv6. See https://github.com/coq-community/vscoq/issues/442 and https://learn.microsoft.com/en-US/troubleshoot/windows-server/networking/configure-ipv6-in-windows.

[HaoYang670]

I met the same error on coq 8.17.1 with vscoq1 on mac

exec: coqtop -v
Listening at ::1:54191
Listening at ::1:54192
Listening at ::1:54193
Listening at ::1:54194
Detected coqtop version 8.17.1
Coqtop version parsed into semver version 8.17.1
exec: coqidetop.opt -main-channel ::1:54191:54192 -control-channel ::1:54193:54194 -async-proofs on -Q . VFA -topfile file:///Users/remziy/Selection.v
coqtop started with pid 3457
coqtop-stderr: Error: host:portr:portw or stdfds expected after option -main-channel

Has there been a solution for this?

[4ever2]

@HaoYang670 Take a look at #613 and #614