New Confluence URL
The wiki is now accessible through wiki.khoury.northeastern.edu. Please update your bookmarks and documentation accordingly.
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.
@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
(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.)