Stream: VsCoq devs & users

Topic: coqtop is not running


view this post on Zulip Michele De Pascalis (Sep 06 2022 at 14:55):

Hi, I just installed Coq on Ubuntu using the Snap package, and I am having a hard time setting up VsCoq. The executables are in /snap/bin/, but when I try to run Coq up to a line, the region flashes in green for a moment, but nothing appears and in the bottom right I can see "coqtop is not running". The command works fine in my terminal:

$ coqidetop.opt -v
The Coq Proof Assistant, version 8.15.2
compiled with OCaml 4.13.1

view this post on Zulip Michael Soegtrop (Sep 06 2022 at 15:42):

Did you set the coqtop bin path in VsCoq settings?

Snap only allows a relatively small number of executables to be mapped such that they are usable without setting a path - afaik various things VsCoq needs are not in there, so you need to set the path.

view this post on Zulip Michele De Pascalis (Sep 07 2022 at 07:37):

Yes, like this:
image.png

view this post on Zulip Michael Soegtrop (Sep 07 2022 at 08:12):

Are you sure coqtop does not require the .opt extension? Can you please send the result of ls -l /snap/bin coq*?

view this post on Zulip Michele De Pascalis (Sep 07 2022 at 08:51):

zsh: no matches found: coq*

view this post on Zulip Michele De Pascalis (Sep 07 2022 at 08:52):

Maybe you meant:

$ ls -l /snap/bin/coq*
lrwxrwxrwx 1 root root 15 set  6 17:22 /snap/bin/coqc -> coq-prover.coqc
lrwxrwxrwx 1 root root 17 set  6 17:22 /snap/bin/coqide -> coq-prover.coqide
lrwxrwxrwx 1 root root 20 set  6 17:22 /snap/bin/coqidetop.opt -> coq-prover.coqidetop
lrwxrwxrwx 1 root root 23 set  6 17:22 /snap/bin/coq_makefile -> coq-prover.coq-makefile
lrwxrwxrwx 1 root root 13 set  6 17:22 /snap/bin/coq-prover.coqc -> /usr/bin/snap
lrwxrwxrwx 1 root root 13 set  6 17:22 /snap/bin/coq-prover.coqide -> /usr/bin/snap
lrwxrwxrwx 1 root root 13 set  6 17:22 /snap/bin/coq-prover.coqidetop -> /usr/bin/snap
lrwxrwxrwx 1 root root 13 set  6 17:22 /snap/bin/coq-prover.coq-makefile -> /usr/bin/snap
lrwxrwxrwx 1 root root 13 set  6 17:22 /snap/bin/coq-prover.coqtop -> /usr/bin/snap
lrwxrwxrwx 1 root root 17 set  6 17:22 /snap/bin/coqtop -> coq-prover.coqtop

view this post on Zulip Michael Soegtrop (Sep 07 2022 at 09:11):

Yes, sorry for the typo. I guess the .opt for coqidetop is a historic artifact then (each individual link must be requested and they are hard to change). So in summary your settings look correct.

Does coqide work?

Did you try installing coq platform from scripts (the i=IDE level would be sufficient which compiles reasonably fast)?

view this post on Zulip Michele De Pascalis (Sep 07 2022 at 11:04):

coqide does work

view this post on Zulip Michael Soegtrop (Sep 07 2022 at 11:50):

OK, then I think the next step in tracking this down would be to test if installation via Coq Platform scripts or Opam works.

view this post on Zulip Paolo Giarrusso (Sep 07 2022 at 17:55):

@Michele De Pascalis
the "Coq Language Server" pane has logs that should help debug this issue:
image.png

view this post on Zulip Paolo Giarrusso (Sep 07 2022 at 17:56):

it's usually on the bottom inside "output", then you must select "Coq Language Server" on the dropdown box on the right (hope screenshot helps)

view this post on Zulip Paolo Giarrusso (Sep 07 2022 at 17:57):

@Michael Soegtrop coqidetop.opt is also the standard name outside snaps (no idea why)

view this post on Zulip Michael Soegtrop (Sep 07 2022 at 18:04):

@Paolo Giarrusso : as I said "historical artifact". The odd thing is /snap/bin/coqidetop.opt -> coq-prover.coqidetop. The link target doesn't have a .opt.

view this post on Zulip Michele De Pascalis (Sep 08 2022 at 08:32):

Thank you, that's useful. Here is the output:

starting coqtop
exec: /snap/bin/coqtop -v
Listening at 127.0.0.1:44799
Listening at 127.0.0.1:32853
Listening at 127.0.0.1:40089
Listening at 127.0.0.1:45355
[Warn  - 11:28:57] Could not detect coqtop version, defaulting to >= 8.10.
Coqtop version parsed into semver version 8.10.0
exec: /snap/bin/coqidetop.opt -main-channel 127.0.0.1:32853:44799 -control-channel 127.0.0.1:40089:45355 -async-proofs on -topfile file:///home/mikidep/Documenti/Coq/isset_eq.v
coqtop started with pid 71364
Client connected on main channel R (port 32853)
Client connected on main channel W (port 44799)
Client connected on control channel R (port 40089)
Client connected on control channel W (port 45355)
--------------------------------
Call Init()
Init: () --> 1
--------------------------------
Call Add("Definition isequiv (...", editId: 0, stateId: 1, verbose: true)
coqtop exited with code: 2
onCoqClosed(coqtop closed with code: 2)
onCoqClosed(undefined)
coqtop closed with code: 2
Listening at 127.0.0.1:42301
Listening at 127.0.0.1:35835
Listening at 127.0.0.1:42687
Listening at 127.0.0.1:42623

Apparently the executables are referred to correctly, but there is some issue that makes coqtop terminate prematurely.

view this post on Zulip Paolo Giarrusso (Sep 08 2022 at 20:40):

I wonder what does coqtop -v output? VsCoq claims it can't even parse that output...

view this post on Zulip Paolo Giarrusso (Sep 08 2022 at 20:42):

Meanwhile, Michael's suggestion is also good (I'm just a fellow user!) and might even give an alternative solution (tho root causing the problem seems still worthwhile)

view this post on Zulip Michael Soegtrop (Sep 09 2022 at 07:18):

@Michele De Pascalis : yes for checking if it is an issue in the installation process or the tools as such, it would be helpful to test a Coq Platform script based installation. The scripts are just a thin wrapper around opam, but they do quite a bit of sanity checking, which exclude a lot of possible errors. But direct use of opam is also fine, if you have it already installed. Otherwise please follow (https://github.com/coq/platform/blob/main/doc/README_Linux.md#installation-by-compiling-from-sources-using-opam). The level (i/IDE) should be sufficient.

view this post on Zulip walker (Sep 11 2023 at 07:52):

logs:

starting coqtop
exec: /home/user/.opam/default/bin/coqtop -v
Listening at ::1:46209
Listening at ::1:43507
Listening at ::1:46467
Listening at ::1:42183
Detected coqtop version 8.17.1
Coqtop version parsed into semver version 8.17.1
exec: /home/user/.opam/default/bin/coqidetop.opt -main-channel ::1:46209:43507 -control-channel ::1:46467:42183 -async-proofs on -w -notation-overridden -R theories sir -topfile file:///run/media/user/phd/sir/coq-typechecker/theories/e0/meta/stability.v
coqtop started with pid 28170
coqtop-stderr: Error: host:portr:portw or stdfds expected after option -main-channel

coqtop exited with code: 1
onCoqClosed(coqtop closed with code: 1)
onCoqClosed(undefined)
coqtop closed with code: 1
Listening at ::1:36987
Listening at ::1:34633
Listening at ::1:44579
Listening at ::1:36263

info:

VScoq version: 0.3.8

$ coqtop -v
The Coq Proof Assistant, version 8.17.1
compiled with OCaml 5.0.0

$ codium -v
1.82.0
13ae69686c4390a9aee7b71b44337eb488319f26
x64

I am not sure if that mean that 0.x is no longer supported

view this post on Zulip walker (Sep 11 2023 at 08:05):

found the issue: https://github.com/coq-community/vscoq/issues/613

view this post on Zulip walker (Sep 11 2023 at 08:13):

if Som1Lse is some one here, I want them to know that I am grateful for having a patch in the issue.


Last updated: Mar 29 2024 at 06:39 UTC