From 1774e2a7aad0605627dd1bc43552889e6268df8c Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 1 Sep 2009 23:18:45 +0000 Subject: Updates --- INSTALL | 61 ++++++++++++------------------------------------------------- 1 file changed, 12 insertions(+), 49 deletions(-) (limited to 'INSTALL') diff --git a/INSTALL b/INSTALL index 05b288a4..fb4cea59 100644 --- a/INSTALL +++ b/INSTALL @@ -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 -- cgit v1.2.3