# Installing Coq for 3110
You need to install Coq 8.6.1 and an IDE.
**Installing Coq 8.6.1.**
The easiest way to install Coq is to use OPAM. Simply do:
$ opam install coq.8.6.1
No version other than 8.6.1, not even slightly different,
**Installing an IDE.**
There are three choices for an IDE: Visual Studio Code,
Proof General, and coqide.
* **Visual Studio Code** is our strong recommendation for most people.
This is a full-featured editor made by the Microsoft Visual Studio team.
It is available for all major systems, including Windows, OS X, and Linux.
You can find it at https://code.visualstudio.com/.
After installing VS Code, and after installing Coq 8.6.1,
open VS Code and click on the bottom icon on the left-hand
side to open the extension installer. Install VSCoq. (You might
also want to install Prettify Symbols Mode, but it's not required.)
VS Code and its Coq support are both relatively new, so there might
be some rough edges that you encounter, but it's still the best
choice for most people.
* **Proof General** is the best Coq IDE, assuming you already know Emacs.
Follow the installation instructions at https://proofgeneral.github.io/.
* **coqide** is an IDE produced by the Coq team itself. It is more
difficult to install and its look-and-feel is not as modern as VS Code.
It can be installed through OPAM with `opam install coqide.8.6.1`.
But it has some OS package dependencies that can be difficult to get
**Check that it's working.** Open a new file in your IDE, and save it
with a name that ends in `.v`, for example, `test.v`. Put the following
definition in your file:
Let x := 42.
(Note that everything there is important: the capitalization, the colon, and
the period.) Now tell Coq to compile that definition:
* In VS Code, go to View->Command Palette, type coq, find Step Forward,
and note the key combination that appears. On Mac, for example,
it is Control-Command-Down. Go back to your file and use that key
* In coqide, go to Navigation->Forward, look for Forward, and note the key
combination that appears. On Mac, for example, it is Control-Down. Go back
to your file and use that key combination.
* In Proof General, type Control-c Control-n.
In each case, the definition you entered should be highlighted, and you should
see output that says `x is declared as a local definition` or just `x is defined`.
The course staff is happy to help you out with any trouble you might have.
It is far easier to diagnose problems in person, so we ask that you come
to office hours rather than post on Piazza.