Hi you guys, I'm totally new to this.
First, how do I execute/compile a file name.v in VSC.
Second, I find a <<coqtop is not running>>... I'm sooo confused about this, thank you all in advanced.
You can open the command palette for instance (Cmd/Ctrl + Shift + P) and then use
Coq: Interpret to point or any other command you want.
coqtop is not running is because it just hasn't started yet. Nothing wrong.
Thanks a lot, you know hot to get a file to get executed in the VSC?
What do you mean? Also there is a
vscoq channel, where this would be a better fit.
But maybe a moderator can move the messages (cc. @Théo Zimmermann ?).
Did you open the palette like I suggested?
If you are on macOS type
Cmd + Shift + P and then start typing
Coq you will se the different commands that you can use.
Thanks a lot, yes, I got to switch of vhannel!
This topic was moved here from #Coq users > OSX users, please test by Théo Zimmermann
Last updated: Jan 30 2023 at 17:03 UTC