These instructions are for Linux and Mac OS. If you are using Windows and want to use opam, you’re probably best off by using a virtual machine.

Coq opam repos:

Install opam. Then do

opam init -n --comp=ocaml-base-compiler.4.02.3 -j 2

You can now install Coq:

opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
opam switch system
eval $(opam env)
opam install coq.8.9.0

To install the equations package, run

opam install coq-equations.1.2~beta2+8.9

If you want to use Coq IDE, run

opam install coqide.8.9.0

Proof General:

In case you haven’t installed emacs already, see below.

It’s recommended to install Proof General from MELPA. All you need to do is M-x package-refresh-contents RET followed by M-x package-install RET proof-general RET.

It’s still possible to install via git:

git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG
cd ~/.emacs.d/lisp/PG
make

Then add the following to your .emacs:

;; Open .v files with Proof General's Coq mode
(load "~/.emacs.d/lisp/PG/generic/proof-site")

company-coq

company-coq is on MELPA. Just use M-x package-refresh-contents RET followed by M-x package-install RET company-coq RET to install and byte-compile company-coq and its dependencies (some of them will produce a few warnings; that’s OK).

To enable company-coq automatically, add the following to your .emacs:

;; Load company-coq when opening Coq files
(add-hook 'coq-mode-hook #'company-coq-mode)

Emacs

Install Emacs. You might want to use Aquamacs on a Mac. Emacs prelude provides some useful extensions and can be installed like this:

git clone git://github.com/bbatsov/prelude.git path/to/local/repo
ln -s path/to/local/repo ~/.emacs.d
cd ~/.emacs.d

(You have to adapt path/to/local/repo to e.g. ~/prelude/)