Jovial Cheukam (Nov 20 2020 at 11:16): Jovial Cheukam (Nov 20 2020 at 11:16):Hello ! I installed the VSCoq extension on VS code and I have the error on the bottom of window "coqtop is not running" and I cannot run any .v file. I use a Mac OS . Please can you help me to fix this ? Thanks...in advance. The file attached is the image showed by my screen. image3.png
Enrico Tassi (Nov 20 2020 at 11:19):@Cyril Cohen do you mind moving this topic to the VsCoq stream?
Notification Bot (Nov 20 2020 at 11:20):This topic was moved here from #Coq users > Installation of Coq in VS code on Mac OS by Cyril Cohen
Théo Winterhalter (Nov 20 2020 at 13:13):It's always saying that coqtop is not running on start. And it's not in the run tab that you're going to fix it.
Théo Winterhalter (Nov 20 2020 at 13:14):Have you tried using Cmd + Shift + P then Coq: Interpret to point or something similar?
Jovial Cheukam (Nov 20 2020 at 17:12):Thank you for replying , I manage as you said and the "coptop is not runnig" message became "ready". Also, the ProofView window opened but display the message "Not in proof mode." and I cannot still execute .v files. Excuse me that I'm a newbie in using VS code and Coq ...I dont know the usual way to exucute .v file of Coq in VScoq on VS code. ....
Enrico Tassi (Nov 20 2020 at 17:49):You move the caret after the sentence you are interested in and you "goto point" (ALT + right arrow on my PC). If you are in the middle of a proof, then the proof view will display your goals.
Théo Winterhalter (Nov 20 2020 at 17:53):Yeah, those messages you are seeing are just stating the obvious, you are not seeing a proof so "Not in proof mode". It will only show something if you step inside an interactive proof.
I think on macOS it's ctrl + alt + down to step, and ctrl + alt + right to go to where the cursor is.
But on vscode, like any serious text editor, you have the command palette (Cmd + Shift + P) which helps you search commands and shows you the different shortcuts available for them. Just type in Coq and you should see a lot of Coq: Interpret to point and the like.
Jovial Cheukam (Nov 20 2020 at 19:38):Thanks you very much. Now with thoses commands you stated before i can see execution of proofs in the ProofView. It works well and I gain some knowledge on how to use VScoq on Vs code...Thanks again.
Théo Winterhalter (Nov 20 2020 at 19:44):Don't hesitate to ask more questions here on how to use VSCoq, and on the "Coq users" stream for general use of Coq.
Last updated: Jun 04 2023 at 23:30 UTC