Updated.

1 files changed, 68 insertions, 11 deletions

diff --git a/COMPATIBILITY b/COMPATIBILITY
index 819a9299..d788b70c 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -2,9 +2,10 @@ Compatibility of Proof General
 ==============================
 
 This version of Proof General has been tested with these Emacs versions
-on Linux:
+on recent Linux systems:
 
- Emacs 22.1.1	       -- recommended and supported
+ 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
@@ -13,19 +14,75 @@ on Linux:
 and (main) prover versions:
 
  Coq 8.0, 8.1
- Isabelle2005, Isabelle2007
+ Isabelle2005, Isabelle2007, Isabelle2008
 
-Maintaining compatibility across proof assistant versions, Emacs
-versions and operating systems is a big challenge!  Please visit this
-wiki page to check on others experience and report your own:
-
- http://proofgeneral.inf.ed.ac.uk/wiki/Main/PGEmacsCompatibility  
+See below for notes about other operating systems.
 
-Unfortunately it's too difficult to maintain backward compatibility.
-Some old version compatibility has been removed here, specifically
-affecting:
+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 may be dropped soon,   ***
+*** switching to GNU Emacs 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/isaxsym.ttf, which
+you should install in Font Book.
+
+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.
+
+
+
+