Damir Gabitov (Sep 25 2022 at 13:39): Damir Gabitov (Sep 25 2022 at 13:39):Hello. I have Coq with IDE. But I want to try Coq in VS Code. I have added extension VSCoq in VS Code. After creating a new file and changing language from Plain Text to Coq, I try to prove something. But I don't see a panel where will be my Goal. And there was a problem that coqtop isn't running. I have added settings for Coq on Setting panel in VS Code like Bin Path, Coqidetop Exe and Coqtop exe. For two last settings I simply have written the names of files: coqide and coqtop. But on output panel I see next messages: Listening at 127.0.0.1:50590... . After Step forward (Alt+Arrow Down) there is no change, and I don't see Goal panel anyway.
Paolo Giarrusso (Sep 25 2022 at 13:47):Did you save the file with a .v extension and a valid name (say, hello.v, but not hi-there.v — it must be a valid coq identifier)? Coqidetop won't start otherwise
Paolo Giarrusso (Sep 25 2022 at 13:48):That you had to manually change language to Coq was the "tell" that makes me suspicious
Damir Gabitov (Sep 25 2022 at 13:52):No, I simply created a new file and tried to prove something . I need save file before write something? Actually, VS Code detect language automaticaly. I changed it manually because at first, I used command File - New Text File. Before writing something I changed language manually
Damir Gabitov (Sep 25 2022 at 14:04):So, I save file. It has .v extension. I try again Step forward , but nothing happened. There is message : [Error - 18:58:49] Error on control channel (R): read ECONNRESET
onCoqClosed(undefined)
coqtop exited with code: null
coqtop closed with code: null
I restart VS Code, then File-Open File... , open my file, and that message after trying to prove:
Lemma mylem: 2+2=4.
Proof.
simpl.
Qed.
In bin directory of Coq there are files like coqide.exe, coqtop.exe, coqtop.opt.exe, coqidetop.opt.exe, etc. What filenames I need use in setting? Maybe I use incorrect filenames?
Damir Gabitov (Sep 25 2022 at 14:04):And one thing: after opening file, there is no a Goal panel anyway
Damir Gabitov (Sep 25 2022 at 14:07):I have found some information too: one can try add coptop.opt.exe in the Path. But where this path-panel in VS Code?
Notification Bot (Sep 25 2022 at 16:14):This topic was moved here from #Coq users > Coq in VS Code by Karl Palmskog.
Paolo Giarrusso (Sep 25 2022 at 20:54):I go to settings, search for coq path, and write the path to the bin folder in Coqtop: Bin Path.
image.png
I haven't changed the other ones, and these are my defaults — I hope your are fine, I'm not sure if you'd need coqidetop.opt.exe instead of coqidetop.opt.
Damir Gabitov (Sep 26 2022 at 09:16):Thank you. It works! Maybe I wrote incorrect file name in Coqidetop Exe: instead coqidetop.opt I wrote coqide or something similar)
Emily Riehl (Oct 24 2022 at 15:14):I have a basic installation question. Am I in the right channel?
I'm an inexperienced Ubuntu user. I've installed the VSCoq extension to VS Code, which gives me the syntax highlighting, but when I try to step through a file (alt + down) I'm told "coqtop is not running." My guess is that I installed Coq in the wrong place or the wrong way or that VS Code can't find it for whatever reason.
In case it's relevant, I've downloaded CoqIDE and as far as I can tell that seems to be working fine. But I'd prefer to use VS Code.
Thanks!
Karl Palmskog (Oct 24 2022 at 15:20):VsCoq uses an executable called coqidetop. As per this topic, you may want to check that the path to coqidetop/coqtop is set for VsCoq in its settings.
Emily Riehl (Oct 24 2022 at 17:50):My settings now correspond to those displayed in the screenshot by @Michele De Pascalis in that thread. I believe I used
"sudo snap install coq-prover" to install Coq. I don't understand the further troubleshooting suggestions.
Karl Palmskog (Oct 26 2022 at 08:16):if coqidetop is in a nonstandard location (e.g., after installing via snap), the VsCoq extension settings inside VS Code may have to be changed point to that location, I think it's something like /snap/bin/. If you do which coqidetop or which coqidetop.opt you might be able to see the location to input inside VS Code.
Karl Palmskog (Oct 26 2022 at 08:18):another possibly-time-consuming workaround is to install manually via the scripts for Linux: https://github.com/coq/platform/blob/main/doc/README_Linux.md#installation-by-compiling-from-sources-using-opam
Emily Riehl (Oct 27 2022 at 19:37):Thanks for sticking with me. I did update the path to /snap/bin/, which is where which coqidetop.opt tells me it is. Incidentally, I also have something called coq-prover.coqidetop in the same location, which seems to be the name given to the same file in the snap installation? I don't know if it's a problem if I have both of these things. I've experimented with listing both names under the VSCoq setting for "Coqidetop Exe" but have not noticed a difference.
Emily Riehl (Oct 27 2022 at 19:39):Most of the time when I try to step down in VSCode nothing happens but occasionally (one time out of 20) I get a long error message that I can't parse. One of the complaints is that "Could not detect coqtop version, defaulting to >= 8.10.
Coqtop version parsed into semver version 8.10.0". I don't know if this matters. The version I have installed is 8.15.2.
Karl Palmskog (Oct 27 2022 at 19:48):coqidetop.opt should be a symlink to coq-prover.coqidetop. This is part of how snaps on Linux works: https://github.com/coq/platform/blob/2022.09.0/doc/README_Linux.md#aliases
Karl Palmskog (Oct 27 2022 at 20:05):here's something that worked for me: set the path to /snap/coq-prover/30/coq-platform/2022-04-1/bin/
Karl Palmskog (Oct 27 2022 at 20:06):(not sure if the 30 is the same on every system)
Théo Zimmermann (Oct 28 2022 at 07:48):The fact that VsCoq cannot detect the coqtop version and defaults to 8.10.0 might be the root of the problem since the XML protocol changed a little between 8.10 and 8.15. It would be good to understand why this happens, but a workaround for users encountering this issue might simply be to keep VsCoq updated so that the default version is the one available in Snap.
Karl Palmskog (Oct 28 2022 at 08:05):what might be happening is that VsCoq can't tolerate the weird symlinking that snap does
Karl Palmskog (Oct 28 2022 at 08:05):for example, coq-prover.coqidetop in /snap/bin is actually a symlink to /usr/bin/snap
Michael Soegtrop (Oct 28 2022 at 08:10):I will push a new snap today where it should also be possible to call the binaries from the snap directly (this is an effect of the ocamlfind hacks I did).
Karl Palmskog (Oct 28 2022 at 08:11):but I think this already works? At least I could call coqidetop.opt and coqtop in /snap/coq-prover/30/coq-platform/2022-04-1/bin/ and VsCoq could as well
Karl Palmskog (Oct 28 2022 at 08:11):it's seemingly the indirection introduced by calling /usr/bin/snap with some symlink name that's the trouble here
Karl Palmskog (Oct 28 2022 at 08:12):would be good to test this stuff in a clean OS install though (e.g., via Docker)
Michael Soegtrop (Oct 28 2022 at 08:50):@Karl Palmskog : I can't say much about how it was before the switch to ocamlfind in 8.16. It is well imaginable that the root finding mechanisms integrated in coqc/coqtop work just fine. And I did not use snap back then.
What I can say is that for 8.16 I tested that it works (to some extent).
Emily Riehl (Oct 28 2022 at 14:51):Thank you thank you thank you thank you @Karl Palmskog. Changing the VsCoq settings to /snap/coq-prover/30/coq-platform/2022-04-1/bin/ did the trick!
I really appreciate you all helping me sort this out.
Karl Palmskog (Oct 28 2022 at 15:06):great that the workaround worked. I will test this problem again with the 8.16 snap
Paolo Giarrusso (Jan 08 2023 at 04:34):This problem seems related to https://github.com/coq-community/vscoq/issues/221#issuecomment-1374677472, as Github user @4ever2 points out there.
Karl Palmskog (Jan 08 2023 at 16:35):connect stuff didn't work for me, I think there is some deeper issue with VS Code and symlinks
Paolo Giarrusso (Jan 08 2023 at 16:47):I'm not sure why symlinks would be a problem; snap containment, OTOH, would make sense
Paolo Giarrusso (Jan 08 2023 at 16:49):Those programs ask for filesystem access to the home, but according to docs, that's still denied by default unless the store grants an exemption (same as tracks, aliases, etc). Did you apply for one? I'm on a phone, but have more details on the GitHub thread
Karl Palmskog (Jan 08 2023 at 16:49):everything is in /snap in both cases, how is /home even involved?
Karl Palmskog (Jan 08 2023 at 16:53):even if I use files in /tmp, /snap/bin/ as path to coqtop is a no-go.
Paolo Giarrusso (Jan 08 2023 at 16:59):I understand/guess that /snap/bin has symlinks to the snap binary that adds sandboxing; the other path links to the raw binaries. So I wonder if exit code 2 means that snap kills Coq for violating sandbox rules. Which would explain why coqtop does not die immediately but only when actually sending input (as suggested by the traces).
Paolo Giarrusso (Jan 08 2023 at 17:00):Not sure why it is looking at /home but there could be many reasons, including .coqrc
Paolo Giarrusso (Jan 08 2023 at 17:09):BTW, do you build snaps for ARM, or only x86? I'm wondering how hard it'd be to reproduce this in a VM...
Karl Palmskog (Jan 08 2023 at 17:34):only x86-64 to my knowledge
Last updated: Jun 04 2023 at 23:30 UTC