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

 Emacs 21.4.1          -- tested; poorer X-Symbol sub/superscript support
 XEmacs 21.5 (beta28)  -- tested; PG has workarounds for several bugs
 XEmacs 21.4.XX	       -- tested

and (main) prover versions:

 Coq 8.0, 8.1
 Isabelle2005, Isabelle2007, Isabelle2008

See below for notes about other operating systems.

Maintaining compatibility across proof assistant versions, Emacs
versions and operating systems is virtually impossible.  Backward
compatibility has to be sacrificed.  Some old version compatibility
has been removed here, specifically affecting:

 Coq 7
 Isabelle 2004
 Earlier buggy versions of GNU Emacs 21  

*********************************************************************
*** IMPORTANT NOTE: XEmacs compatibility will be dropped on next  ***
*** release of PG -- switching to GNU Emacs now is recommended!   ***
*********************************************************************

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, but being based on GNU Emacs 23, it has recently become
incompatible with X-Symbol because of API changes.  (A fix would be
welcome; may be simple).  If you do not care about X-Symbol, or
can use the Unicode Symbols mode, Emacs.app works just as well.

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.