PGEmacsOnWindowsXP < PG

PG Web>ProofGeneralEmacs>PGEmacsOnWindowsXP (12 Sep 2006, GiorgosF ) (raw view)EditAttach

---+ Running Proof General on Windows XP


%TOC%



---++ 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:

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

   * add the following lines to .emacs:

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

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

<verbatim>
      Path = %SystemRoot%\system32;%SystemRoot%;C:\Program Files\Coq\bin
</verbatim>


%ICON{pencil}% __Windows users: please add more content here__

Topic revision: r3 - 12 Sep 2006 - 23:24:53 - GiorgosF

Main.PGEmacsOnWindowsXP moved from Main.ProofGeneralOnWindowsXP on 23 Aug 2006 - 19:07 by DavidAspinall

Copyright © 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