Running Proof General on Windows XP

Using Cygwin

This is the recommended way to get things working. Visit 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

pencil Windows users: please add more content here

This topic: PG > WebHome > ProofGeneralEmacs > PGEmacsOnWindowsXP
Topic revision: r3 - 12 Sep 2006 - 23:24:53 - GiorgosF
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
This Wiki uses Cookies