Stream: VsCoq devs & users

Topic: Beginner's help


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip ebuitragod (Jan 14 2021 at 15:21):

Thanks a lot, you know hot to get a file to get executed in the VSC?

view this post on Zulip 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.

view this post on Zulip ebuitragod (Jan 14 2021 at 15:22):

Thanks!

view this post on Zulip Théo Winterhalter (Jan 14 2021 at 15:22):

https://coq.zulipchat.com/#narrow/stream/237662-VsCoq-devs.20.26.20users

view this post on Zulip Théo Winterhalter (Jan 14 2021 at 15:23):

But maybe a moderator can move the messages (cc. @Théo Zimmermann ?).

view this post on Zulip Théo Winterhalter (Jan 14 2021 at 15:23):

Did you open the palette like I suggested?

view this post on Zulip 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.

view this post on Zulip ebuitragod (Jan 14 2021 at 15:31):

Thanks a lot, yes, I got to switch of vhannel!

view this post on Zulip 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: Jan 30 2023 at 17:03 UTC