Vasileios Koutavas
Child pages
  • Coq-ProofGeneral-Emacs-Windows
Skip to end of metadata
  • Created by Unknown User (vkoutav), last modified on Nov 02, 2007
Go to start of metadata

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.

  1. GNU Emacs:
    1. If you have a recent version of GNU Emacs running (22.1 or later) then skip this section.
    2. Download the latest version of GNU Emacs for windows. I used version 22.1.0.0.
    3. Unzip the the installation zip, and copy it somewhere on you disk (e.g. C:\Program Files\Emacs\emacs-22.1).
    4. Run the program C:\Program Files\Emacs\emacs-22.1\bin\addpm.exe to create a Start Menu item for emacs.
  2. Coq:
    1. Download the latest version of Coq (8.1pl2, Oct. 2007)
    2. Install Coq in a local directory of your choice (e.g. C:\Program Files\Coq)
    3. 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: 
      @echo off
set COQTOP=C:\PROGRA~1\Coq
set COQLIB=%COQTOP%\lib
set COQBIN=%COQTOP%\bin
set PATH=%PATH%;%COQBIN%
set HOME=%HOMEPATH%
%COQBIN%\coqtop.opt.exe -top "%COQTOP%" -emacs-U
  3. ProofGeneral:
    1. 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.
    2. Install ProofGeneral in a local directory of your choice (e.g. C:\Program Files\Proofgeneral-3.7pre071025)
    3. 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.
    4. 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:

Definition A:Set.

and press "C-C C-n". The above line should be underlined and the following should appear in the *goals* buffer:

1 subgoal
  
  ============================
   Set

(Thanks to Mitch Wand for debugging this how-to and suggesting a better Emacs configuration than I initially had.)

  • No labels