Stream: VsCoq devs & users

Topic: Coq in VS Code


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Sep 25 2022 at 13:48):

That you had to manually change language to Coq was the "tell" that makes me suspicious

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Damir Gabitov (Sep 25 2022 at 14:04):

And one thing: after opening file, there is no a Goal panel anyway

view this post on Zulip 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?

view this post on Zulip Notification Bot (Sep 25 2022 at 16:14):

This topic was moved here from #Coq users > Coq in VS Code by Karl Palmskog.

view this post on Zulip 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.

image.png

view this post on Zulip 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)

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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/

view this post on Zulip Karl Palmskog (Oct 27 2022 at 20:06):

(not sure if the 30 is the same on every system)

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Oct 28 2022 at 08:05):

what might be happening is that VsCoq can't tolerate the weird symlinking that snap does

view this post on Zulip Karl Palmskog (Oct 28 2022 at 08:05):

for example, coq-prover.coqidetop in /snap/bin is actually a symlink to /usr/bin/snap

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Oct 28 2022 at 15:06):

great that the workaround worked. I will test this problem again with the 8.16 snap

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jan 08 2023 at 16:47):

I'm not sure why symlinks would be a problem; snap containment, OTOH, would make sense

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jan 08 2023 at 16:49):

everything is in /snap in both cases, how is /home even involved?

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Paolo Giarrusso (Jan 08 2023 at 17:00):

Not sure why it is looking at /home but there could be many reasons, including .coqrc

view this post on Zulip 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...

view this post on Zulip Karl Palmskog (Jan 08 2023 at 17:34):

only x86-64 to my knowledge


Last updated: Jan 30 2023 at 18:04 UTC