Michele De Pascalis (Sep 06 2022 at 14:55): 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
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.
Michele De Pascalis (Sep 07 2022 at 07:37):Yes, like this:
image.png
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*?
Michele De Pascalis (Sep 07 2022 at 08:51):zsh: no matches found: coq*
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
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)?
Michele De Pascalis (Sep 07 2022 at 11:04):coqide does work
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.
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
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)
Paolo Giarrusso (Sep 07 2022 at 17:57):@Michael Soegtrop coqidetop.opt is also the standard name outside snaps (no idea why)
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.
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.
Paolo Giarrusso (Sep 08 2022 at 20:40):I wonder what does coqtop -v output? VsCoq claims it can't even parse that output...
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)
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.
Last updated: Jun 04 2023 at 22:30 UTC