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
@Cyril Cohen do you mind moving this topic to the VsCoq stream?
This topic was moved here from #Coq users > Installation of Coq in VS code on Mac OS by Cyril Cohen
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.
Have you tried using
Cmd + Shift + P then
Coq: Interpret to point or something similar?
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. ....
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.
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.
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.
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: Jan 30 2023 at 18:04 UTC