Running Proof General on Windows XP

Using Cygwin

This is the recommended way to get things working. Visit http://www.cygwin.com/ to find out more.

Using Coq + Emacs Windows port

The following steps are needed for ProofGeneral to integrate with the Windows port of Emacs and Coq. Tested with Proof General 3.5, Coq 8.0pl3 and Emacs 21.3.

• decompress ProofGeneral -3.5.tar.gz contents to a temporary folder

• copy ProofGeneral -3.5 folder to the Emacs /site-lisp directory

• search and delete all .elc files under the ProofGeneral -3.5 directory (including those in subdirs)

• edit coq/coq.el and set coq-prog-name to "coqtop.opt -emacs", for example:

      (defcustom coq-prog-name "coqtop.opt -emacs"
      "*Name of program to run as Coq."
      :type 'string
      :group 'coq)

• add the following lines to .emacs:

      ;; Proof general
      (load-file "<emacs directory>/site-lisp/ProofGeneral-3.5/generic/proof-site.el")

• add coq \bin directory to the Windows PATH (My Computer->Properties->Advanced->Environment Variables->add ";Coq path\bin" to PATH), for example:

      Path = %SystemRoot%\system32;%SystemRoot%;C:\Program Files\Coq\bin

Windows users: please add more content here