Stream: Coq users

Topic: Help getting set up with CoqIDE


view this post on Zulip Franklin Pezzuti Dyer (Apr 05 2022 at 17:05):

Hey all! First-time Coq user here, and I'm having a lot of trouble getting set up. Would someone be willing to help me troubleshoot?

There's a nice tutorial online here, which I'd like to work through: https://cel.archives-ouvertes.fr/inria-00001173v6/document I've downloaded the CoqIDE (for MacOS), but I can't figure out how to run even a simple command like Check True. in the IDE. I can type the command into the left-hand pane of the IDE, but I have no idea how to actually run it, and I haven't been able to figure it out after clicking through every menu of the interface. According to the tutorial, the correct output would be True : Prop.

Screen-Shot-2022-04-05-at-11.04.40-AM.png

Can someone give me a pointer on how to get started? Apologies for the noobie question, but I'm finding the interface really opaque and couldn't find any tutorials online about how to use the IDE itself.

view this post on Zulip Gaëtan Gilbert (Apr 05 2022 at 17:13):

does the down arrow button not work?

view this post on Zulip Gaëtan Gilbert (Apr 05 2022 at 17:14):

the down arrow immediately right of the x button

view this post on Zulip Franklin Pezzuti Dyer (Apr 05 2022 at 17:15):

Ahhh. Yes, that worked, thank you @Gaëtan Gilbert :face_palm: It appeared to be greyed out and unclickable, but that was a wrong assumption apparently

view this post on Zulip Ali Caglayan (Apr 05 2022 at 17:15):

You should also be able to do cmd + down arrow to step down in the proof if I am not mistaken


Last updated: Jan 31 2023 at 13:02 UTC