diff options
| -rw-r--r-- | CHANGES | 10 | ||||
| -rw-r--r-- | COMPATIBILITY | 34 | ||||
| -rw-r--r-- | INSTALL | 61 |
3 files changed, 32 insertions, 73 deletions
@@ -1,6 +1,6 @@ -*- outline -*- -* Summary of Changes for Proof General 4.0 from 3.7.X +* Main Changes for Proof General 4.0 from 3.7.X ** Generic changes @@ -34,4 +34,12 @@ *** Electric terminator works without inserting terminator +*** Line numbers reported during script management + +*** Sync problems with bad input prevented by command wrapping + + +** Coq changes + +*** Holes mode can be turned on/off diff --git a/COMPATIBILITY b/COMPATIBILITY index ab94bd41..46331c1c 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -4,19 +4,16 @@ Compatibility of Proof General This version of Proof General has been tested with these Emacs versions on recent Linux systems: - Emacs 22.3.1 -- recommended and supported - Emacs 23.0.X -- CVS/beta snapshots, use time of PG release + Emacs 23.1 -- recommended and supported + Emacs 22.3.1 -- previous version, should work well -and (main) prover versions: - - Coq 8.1pl3 - Isabelle2009 +and (main) prover versions: Coq 8.1pl3, Isabelle2009 See below for notes about other operating systems. Maintaining compatibility across proof assistant versions, Emacs -versions and operating systems is virtually impossible. In this -major release, ** XEmacs compatibility has been dropped ** +versions and operating systems is virtually impossible. In this major +release ** XEmacs compatibility has been dropped ** Running on Windows ------------------ @@ -47,26 +44,17 @@ 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 23.1 build of GNU Emacs, which builds natively +on Mac OS X (based on the NextStep port). -We recommend the 22.X based Carbon Emacs, here: +Note that Mac compatibility isn't thoroughly tested. If you discover +problems, please send a report and/or fix to the address above. - http://homepage.mac.com/zenitani/emacs-e.html +There is also a wiki page for tips: -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. + http://proofgeneral.inf.ed.ac.uk/wiki/PG/PGEmacsOnMacOSX -Note: Emacs.app looks set to become the future supported Mac port of -GNU Emacs, and is based on GNU Emacs 23. It should work well with -this version of Proof General, but at the time of writing the latest -binary release is not as reliable as that of Carbon Emacs. -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. @@ -18,7 +18,7 @@ Proof General loaded. The command above will set the Emacs load path and add auto-loads for proof assistants, for example, visiting a file ending in .v will start Coq Proof General, and a file ending in .thy will start -Isabelle/Isar Proof General. See the manual for a full list of file +Isabelle Proof General. See the manual for a full list of file extensions and proof assistants, and the note below for how to disable those you don't need. @@ -42,58 +42,31 @@ Detailed installation Notes for Proof General Supported Emacs Versions. ------------------------- -This release has been tested with XEmacs 21.4.17 and GNU Emacs 21.3.1 -(running on i386 Linux). We recommend using these or later versions. +Please see COMPATIBILTY. -If you're not sure of your version of Emacs, inspect the -variable `emacs-version' by doing: +If you're not sure of your version of Emacs, inspect the variable +`emacs-version' by doing: C-h C-v emacs-version RET Other *recent* versions of either Emacs may also work, but please do not send bug reports for any version of Emacs which is more than a year older than the most recent stable release of that Emacs, unless -you are reasonably sure that the bug has something to do with Proof -General rather than Emacs. Unfortunately, compatibility across +you are reasonably sure that the bug has something to do with +Proof General rather than Emacs. Unfortunately, compatibility across different Emacs versions is very difficult to maintain as APIs change frequently and bugs come and go between Emacs releases. - -RPM packages. ------------- - -The RPMs are intended to be compatible with the RPMs distributed with -Red Hat/Fedora. Three packages are provided: ProofGeneral, -ProofGeneral-emacs-elc and ProofGeneral-xemacs-elc. The two elc RPMs -contain compiled elisp for GNU Emacs and XEmacs respectively. - -You should have a fully working ProofGeneral if you just install the -main package. The byte compiled files will provide extra -performance on the respective Emacs versions. - -The command "proofgeneral" will launch Emacs with Proof General -loaded. If you install the byte compiled files, Proof General should -be automatically added to your Emacs startup configuration: you can -just launch an Emacs and edit a proof script file to get going. - -If you want to add the uncompiled Proof General version to your -personal Emacs configuration, add this line: - - (load-file "/usr/share/emacs/ProofGeneral/generic/proof-site.el") - -to your .emacs file. - - Byte Compilation. ----------------- Compilation of the Emacs lisp files improves efficiency but can sometimes cause compatibility problems. In particular, byte compiled -files are generally not compatible between XEmacs and GNU Emacs. +files are generally not compatible between different Emacs versions. -We distribute .elcs for GNU Emacs, so you will have to delete -them and (optionally) recompile for XEmacs. +We distribute .elcs for GNU Emacs 23.1, so you will have to delete +them and (optionally) recompile for GNU Emacs 22. Use 'make clean' to remove all .elc files. Use 'make compile' to recompile .elc files. @@ -107,28 +80,18 @@ Dependency on Other Emacs Packages Proof General relies on several other Emacs packages, which are probably already supplied with your version of Emacs. If not, you -will need to find them. XEmacs is sometimes unbundled, so you may -need to select packages (or package groups) specially. These are the -packages that you need to use Proof General: +will need to find them. These are the packages that you need to use +Proof General: ESSENTIAL: * cl-macs * comint * custom * font-lock - * xml [ not yet essential but will be soon ] OPTIONAL: * outline - * func-menu or imenu - -If in doubt and you have the option, select the aptly named XEmacs -"sumo" package. - -The X Symbol package is now bundled with Proof General so you -do not need to download it separately. - - + * imenu Site-wide Installation |