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 ++++++++++++++++++++++++++++++++++++++++++++++++++--------- INSTALL | 61 ++------------------------------------------- 2 files changed, 70 insertions(+), 70 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. + + + + diff --git a/INSTALL b/INSTALL index 8ffb27de..05b288a4 100644 --- a/INSTALL +++ b/INSTALL @@ -1,5 +1,5 @@ -Instructions for installing Proof General -========================================= +Short Instructions for installing Proof General (details below) +=============================================================== Proof General runs on a variety of platforms and with a variety of Emacs versions; see COMPATIBILITY for further notes. @@ -36,9 +36,6 @@ If none of these files help, then contact me via the address below. - - - Detailed installation Notes for Proof General ============================================= @@ -88,60 +85,6 @@ personal Emacs configuration, add this line: to your .emacs file. -Running on Windows ------------------- - -For tips, please see here: - - http://proofgeneral.inf.ed.ac.uk/wiki/Main/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/Main/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. - - - - Byte Compilation. ----------------- -- cgit v1.2.3