Setting up emacs as interface for coq

Tags: / installation coq emacs /

An experience setting up emacs with Proof General for using coq interactively.

Proof general mode of emacs, together with the company-coq package can be used as an interface for coq as mentioned here.

.emacs file

Add the following to your `.emacs` file.

(require 'package)
(add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t)
(package-initialize)

(Source: Proof General github page)

Edit gpg.conf

Go to `~/.emacs.d/elpa/gnupg/` directory (make it if it doesn't exist) and open the gpg.conf file.

Add the following to it.

keyserver hkp://keys.gnupg.net:80

Receive gpg keys

Run

gpg --homedir ~/.emacs.d/elpa/gnupg --receive-keys 066DAFCB81E42C40

Install the packages inside emacs

Finally, open up emacs and run (to update the list of packages, I guess)

M-x package-refresh-contents

Then, install the packages with

M-x package-install RET proof-general 
M-x package-install RET company-coq

company-coq extends the proof general's coq mode.

Versions of software involved

References