From f82b8659739559220eff75fb330d9f36a94994cc Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 10 Jul 2008 18:26:13 +0000 Subject: Updated. --- COMPATIBILITY | 79 ++++++++++++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 68 insertions(+), 11 deletions(-) (limited to 'COMPATIBILITY') 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. + + + + -- cgit v1.2.3