ebuitragod (Jan 14 2021 at 14:57): ebuitragod (Jan 14 2021 at 14:57):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.
imagen.png
Théo Winterhalter (Jan 14 2021 at 15:04):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.
ebuitragod (Jan 14 2021 at 15:21):Thanks a lot, you know hot to get a file to get executed in the VSC?
Théo Winterhalter (Jan 14 2021 at 15:22):What do you mean? Also there is a vscoq channel, where this would be a better fit.
ebuitragod (Jan 14 2021 at 15:22):Thanks!
Théo Winterhalter (Jan 14 2021 at 15:22):https://coq.zulipchat.com/#narrow/stream/237662-VsCoq-devs.20.26.20users
Théo Winterhalter (Jan 14 2021 at 15:23):But maybe a moderator can move the messages (cc. @Théo Zimmermann ?).
Théo Winterhalter (Jan 14 2021 at 15:23):Did you open the palette like I suggested?
Théo Winterhalter (Jan 14 2021 at 15:24):If you are on macOS type Cmd + Shift + P and then start typing Coq you will se the different commands that you can use.
ebuitragod (Jan 14 2021 at 15:31):Thanks a lot, yes, I got to switch of vhannel!
Notification Bot (Jan 14 2021 at 19:02):This topic was moved here from #Coq users > OSX users, please test by Théo Zimmermann
Last updated: Oct 08 2024 at 14:01 UTC