Getting Started - coq/coq GitHub Wiki
(Part of the Coq FAQ)
I just want to try out Coq without having to install anything at first. Is that possible?
Yes! You can try out Coq in your browser. Here are some links:
- This tutorial works directly in the browser. Step through the document with ALT+Downarrow. If you ever lose the panels on the right side, click the red "power" button and they will appear.
- If you prefer starting from scratch, you can use the jsCoq scratchpad.
In the scratchpad, you can type something like
Theorem HelloCoq : 4 * 10 + 2 = 42.
Proof. simpl. reflexivity. Qed.
then press ALT+Downarrow several times, and watch Coq step through the proof.
-
You can also start reading and running the Software Foundations book series in your browser.
-
All of these options are using the jsCoq Interactive Online System, which allows you to run Coq in the browser.
I am ready to install Coq on my machine. Do you have some quick instructions on how to do that?
The Coq Platform is available from various package repositories: try brew install coq
on Mac OS X, sudo snap install coq-prover
on Linux, or on Windows download and run an installer from Assets, scrolling down a bit on this page.
You can check your installation by typing coqc --version
in a terminal.
This Wiki also contains more detailed installation instructions, sorted by operating system.
I have a background in mathematics / programming / other field. What are accessible resources for someone with my background?
The Software Foundations book series is traditionally recommended for people coming from programming, while the Mathematical components book is a natural starting point for mathematicians. Preferences seem to vary from person to person, though, and we recommend you try out some of the resources on Awesome Coq to find something that works for you.
Where can I find an overview of the various libraries, resources, packages and extensions of Coq that exist?
There is a pretty exhaustive list over at Awesome Coq.
I'm just getting started and my question isn't answered here. What can I do?
Ask your question to other Coq users! For example using Zulip chat or the Discourse forum.
:information_source: Request. When you do find the answer to your question, please add it to this page to help others! You can also clarify or supplement existing answers. Just click the Edit button on the right to get started (you'll need a Github account).
What IDE's are available for using Coq?
First make sure Coq is installed, see above. You can now start setting up your development/proving environment (official page), choose any of the following:
- Emacs and Proof-general
- Vscode and vscoq
- Coq IDE
- Vim/NeoVim and Coqtail