yforster / coqsetup Goto Github PK

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