Installation How-To for Coq + ProofGeneral + GNU Emacs + Windows
This is how I made Coq, Proof-General, Emacs, and Windows work all together. I describe my own situation, giving the version numbers of the programs I used, and the directories I've installed them in. I suppose you can install newer versions in different directories and things will still work. If you do that some renaming is necesary.
- GNU Emacs:
- If you have a recent version of GNU Emacs running (22.1 or later) then skip this section.
- Download the latest version of GNU Emacs for windows. I used version 22.214.171.124.
- Unzip the the installation zip, and copy it somewhere on you disk (e.g. C:\Program Files\Emacs\emacs-22.1).
- Run the program C:\Program Files\Emacs\emacs-22.1\bin\addpm.exe to create a Start Menu item for emacs.
- Download the latest version of Coq (8.1pl2, Oct. 2007)
- Install Coq in a local directory of your choice (e.g. C:\Program Files\Coq)
- You now have to make a .bat file that sets the right environment variables when calling Coq from within emacs, and passes the right command-line arguments to it. Create somewhere in your emacs's exec-path (typically someplace like C:/Program Files/Emacs/emacs-21.2/bin/) a file called 'coq-emacs.bat' that contains the following:
%COQBIN%\coqtop.opt.exe -top "%COQTOP%" -emacs-U
- Download the development release of ProofGeneral (3.7pre071025). In Windows, GNU Emacs communicates with the Coq process in unicode, but the stable release of ProofGeneral (3.5) can't handle unicode and hangs.
- Install ProofGeneral in a local directory of your choice (e.g. C:\Program Files\Proofgeneral-3.7pre071025)
- Make sure that there are no .elc files in C:\Program Files\Proofgeneral-3.7pre071025 and its sub-directories; the development release shouldn't have any, but if it does then just delete them.
- Run Emacs, open your .emacs file (C-X C-F ~/.emacs), and add the following two lines to it, in this order:
(defvar coq-prog-name "coq-emacs.bat")
(load-file "C:/Program Files/ProofGeneral-3.7pre071025/generic/proof-site.el")
Things should work now. If you fire up emacs and open a test.v file, you should see ProofGeneral's welcone buffer. Then write something trivial:
and press "C-C C-n". The above line should be underlined and the following should appear in the *goals* buffer:
(Thanks to Mitch Wand for debugging this how-to and suggesting a better Emacs configuration than I initially had.)