diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2008-07-24 09:51:53 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2008-07-24 09:51:53 +0000 |
| commit | 76d6b0b2b1f039549d308a0d2c478a6b05869af9 (patch) | |
| tree | 78cc7e13bf290a17e7006a6d4616a8a08e36ce8f /COMPATIBILITY | |
| parent | 8f8e9388b582ad6d3ee6e1eea842a8d443d4ce89 (diff) | |
Merge changes from Version4Branch.
Diffstat (limited to 'COMPATIBILITY')
| -rw-r--r-- | COMPATIBILITY | 28 |
1 files changed, 6 insertions, 22 deletions
diff --git a/COMPATIBILITY b/COMPATIBILITY index 302d5ef6..5e6fd390 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -7,30 +7,16 @@ 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 + 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. 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! *** -********************************************************************* +versions and operating systems is virtually impossible. In this +major release, ** XEmacs compatibility has been dropped ** Running on Windows ------------------ @@ -74,10 +60,8 @@ 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. +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 |