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 to #VsCoq devs & users > Coq in VS Code by Karl Palmskog.
Last updated: Feb 08 2023 at 23:03 UTC