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.
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
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
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)
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/
)