Getting Started
(Part of the Coq FAQ)
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.
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.
Ask your question to other Coq users! For example using Zulip chat or the Discourse forum.
ℹ️ 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).
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
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.