Compatibility of Proof General
==============================

This version of Proof General has been tested with these Emacs versions
on recent Linux systems:

 Emacs 22.2.1	       -- recommended and supported
 Emacs 23.0.X          -- CVS/beta snapshots, use time of PG release

and (main) prover versions:

 Coq 8.1
 Isabelle2008

See below for notes about other operating systems.

Maintaining compatibility across proof assistant versions, Emacs
versions and operating systems is virtually impossible.  In this
major release, ** XEmacs compatibility has been dropped **

Running on Windows
------------------

For tips, please see here:

   http://proofgeneral.inf.ed.ac.uk/wiki/PG/PGEmacsOnWindows

We recommend EmacsW32 available at:

   http://www.ourcomments.org/Emacs/EmacsW32.html

Unpack the Proof General tar or zip file, and rename the folder to
"ProofGeneral" to remove the version number.  Put a line like this:

   (load-file "c:\\ProofGeneral\\generic\\proof-site.el")

into .emacs.  You should put .emacs in value of HOME if you set that,
or else in directory you installled Emacs in, e.g.  
c:\Program Files\Emacs\.emacs

Note that Windows compatibility isn't thoroughly tested by the
maintainers.  If you discover problems, please send a report and/or
fix to the address above.



Running on Mac OS X
-------------------

For tips, please see here:

  http://proofgeneral.inf.ed.ac.uk/wiki/PG/PGEmacsOnMacOSX

We recommend the 22.X based Carbon Emacs, here:

  http://homepage.mac.com/zenitani/emacs-e.html

This works with X-Symbol using the supplied TrueType font
x-symbol/etc/fonts-ttf/XSymb1.ttf, which you should install in Font
Book, or copy directly to /Library/Fonts or ~/Library/Fonts.

Note: Emacs.app looks set to become the future supported Mac port of
GNU Emacs, and is based on GNU Emacs 23.  It should work well with
this version of Proof General.

Note that Mac compatibility isn't thoroughly tested by the
maintainers.  If you discover problems, please send a report and/or
fix to the address above.