Stream: Coq 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 to #VsCoq devs & users > Coq in VS Code by Karl Palmskog.


Last updated: Feb 08 2023 at 23:03 UTC