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.
Yes, like this:
Are you sure coqtop does not require the .opt extension? Can you please send the result of
ls -l /snap/bin coq*?
zsh: no matches found: coq*
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)?
coqide does work
OK, then I think the next step in tracking this down would be to test if installation via Coq Platform scripts or Opam works.
@Michele De Pascalis
the "Coq Language Server" pane has logs that should help debug this issue:
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)
coqidetop.opt is also the standard name outside snaps (no idea why)
@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
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.
I wonder what does coqtop -v output? VsCoq claims it can't even parse that output...
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)
@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: Jan 30 2023 at 17:03 UTC