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.
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
That you had to manually change language to Coq was the "tell" that makes me suspicious
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
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
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.
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?
And one thing: after opening file, there is no a Goal panel anyway
I have found some information too: one can try add coptop.opt.exe in the Path. But where this path-panel in VS Code?
This topic was moved to #VsCoq devs & users > Coq in VS Code by Karl Palmskog.
Last updated: Feb 08 2023 at 23:03 UTC