diff options
| -rw-r--r-- | BUGS | 9 | ||||
| -rw-r--r-- | CHANGES | 24 | ||||
| -rw-r--r-- | INSTALL | 66 | ||||
| -rw-r--r-- | README | 4 | ||||
| -rw-r--r-- | todo | 2 |
5 files changed, 48 insertions, 57 deletions
@@ -1,22 +1,17 @@ -*- outline -*- -* Known issues which will be resolved before 3.4 +* Bugs to be fixed before PG 3.4 is released. The items below are known and will be fixed (I hope!) before 3.4 is released. Please don't send email about them (unless you have a patch...) - ** X-Symbol probs with Isabelle -- latin1 chars may get saved in file [XE 21.1 only?] -- superscripts/subscripts not fully working [menu option ignored] ** X-Symbol probs with Coq, LEGO - -- X-Symbol 4.x not supported, don't try it or your Emacs will - explode - ------------------------------------------------------------------ - + -- X-Symbol 4.x not supported, don't try it or your Emacs will explode * Known Bugs and Workarounds for Proof General. @@ -17,10 +17,12 @@ It is now permitted to use Proof General in any context, without applying for a special license from University of Edinburgh. Free redistribution is also allowed under the GPL conditions. -*** Remove handling for provers you don't want +*** Support added for GNU Emacs 21.X; no support for GNU Emacs 20.X -You can simply remove the directories from the PG distribution, -instead of customizing the `proof-assistants' variable. +Toolbar, splash screen, and X-Symbol are all supported in GNU Emacs. + +Sorry, this version of PG does not support Emacs 20; backwards +compatibility is far too difficult to maintain. *** Colours altered @@ -28,14 +30,15 @@ Queue and locked colours made a little less lurid. (Look in proof-config for proof-locked-face, proof-queue-face and old settings if you want to change back). -*** Support added for GNU Emacs 21.X; no support for GNU Emacs 20.X +*** Improvements to visibility controls -Toolbar, splash screen, and X-Symbol are all supported in GNU Emacs. +Visibility controls now work for comments and commands in proof +scripts. An image is used in XEmacs to signal hidden text. -Sorry, this version of PG does not support Emacs 20; backwards -compatibility is far too difficult to maintain. +*** Improvement to "Favourites" user-defined menus -*** Improvement to "Favourites" user-defined menus (deletion added) +Favourites are now more robust. You can delete them and save them +when you want. *** Support for "tracing" buffers improved and enabled by default. @@ -44,6 +47,11 @@ Compared with experimental tracing in PG 3.3, there is now only one tracing buffer, treated somewhat like a response buffer. For minor issues, see isa/BUGS. +*** Easily remove handling for provers you don't want + +You can simply remove the directories from the PG distribution, +instead of customizing the `proof-assistants' variable. + ** Isabelle Changes @@ -1,12 +1,13 @@ Instructions for installing Proof General ========================================= -This file describes what to do to run Proof General. -Please let us know if you have problems trying to install it. +Proof General runs on a variety of platforms and with a variety of +Emacs versions; see notes below for particular hints. Please send us +additional hints for alternative platforms/Emacsen not mentioned. -Unpack this distribution somewhere. It will create a top-level -directory containing Proof General, called Proof-General-<something>. -Put this line in your .emacs file: +To install, unpack the distribution somewhere. It will create a +top-level directory containing Proof General, called +Proof-General-<something>. Put this line in your .emacs file: (load-file "<proofgeneral-home>/generic/proof-site.el") @@ -16,28 +17,17 @@ you can use the script in bin/proofgeneral to launch Emacs with Proof General loaded. The command above will set the Emacs load path and add auto-loads for -the assistants below: - - .v Coq files - .l LEGO files - .thy Isabelle files - .ML Isabelle files - .phx PhoX files - .sml HOL98 files - .elf Twelf files - .acl2 ACL2 files - -When you load a file with one of these extensions, the corresponding -Proof General mode will be entered. +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 +extensions and proof assistants, and the note below for how to disable +those you don't need. In case of difficulty, please check the documentation in doc/, the notes below, the README file for each prover, and the file BUGS. -If none of these files t help, then contact us via the address below. +If none of these files help, then contact us via the address below. - - David Aspinall. - - Proof General maintainer <support@proofgeneral.org> LFCS, Division Of Informatics, @@ -67,7 +57,8 @@ If you have the RPM file, this is the line you should add to your Running on Windows ------------------ -We recommend XEmacs compiled for Windows, see http://www.xemacs.org +We recommend XEmacs compiled for Windows, see http://www.xemacs.org. +Some Isabelle users have reported better operation with cygwin XEmacs. Unpack the Proof General tar or zip file, and rename the folder to "ProofGeneral" to remove the version number. Put a line like this: @@ -78,17 +69,16 @@ into .emacs. You should put .emacs in value of HOME if you set that, or else in directory you installled XEmacs in, e.g. c:\Program Files\XEmacs\.emacs -See also README.windows 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. Note that XEmacs is now being unbundled, -so you may need to select packages (or package groups) specially. -These are the packages that you need to use Proof General: +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: ESSENTIAL: * cl-macs @@ -126,8 +116,8 @@ If you are installing Proof General site-wide, you can put the components in the standard directories of the filesystem if you prefer, providing the variables in proof-site.el are adjusted accordingly. Make sure that the generic and assistant-specific elisp -files are kept in subdirectories of proof-home so that the autoload -directory calculations are correct. +files are kept in subdirectories of `proof-home-directory' so that the +autoload directory calculations are correct. To save every user needing the line in their .emacs file, you can put that into a site-wide file like default.el. Read the Emacs manual for @@ -137,15 +127,15 @@ details. Removing support for unwanted provers ------------------------------------- -You cannot run more than one instance of Proof General at a time: -e.g. if you're using Coq, you won't be able to run LEGO scripts. +You cannot run more than one instance of Proof General at a time in +the same Emacs process: e.g. if you're using Coq, you won't be able to +run LEGO scripts. -If there are some assistants supported that you never want to use, -you can remove them from the variable `proof-assistants` -to prevent Proof General autoloading for files with particular -extensions. This may be useful if you want to use other modes for -those files, for example, you may want sml-mode for .ML files or -Verilog mode for .v files. +If there are some assistants supported that you never want to use, you +can remove them from the variable `proof-assistants' to prevent Proof +General autoloading for files with particular extensions. This may be +useful if you want to use other modes for those files, for example, +you may want sml-mode for .ML files or Verilog mode for .v files. The easiest way to do this (and other customization of Proof General) is via the Customize mechanism, see the menu: @@ -4,7 +4,7 @@ Proof General --- Organize your proofs! Proof General is a generic Emacs interface for proof assistants. This is version 3.4 of Proof General. -(Check the About screen for precise version number). +(Check the About screen for a precise version number). The aim of the Proof General project is to provide a powerful and configurable interfaces which help user-interaction with interactive @@ -50,7 +50,7 @@ mailing list for Proof General, visit Proof General on the web at: http://www.proofgeneral.org David Aspinall <da@proofgeneral.org> -July 2002. +August 2002. ----- @@ -723,8 +723,6 @@ LIST OF THINGS FOR PG 3.4 ** Does proof-follow-mode have any effect??? -** Add glyphs for hidden proofs. - ** Fix-up show/hide for nested proofs. (Wierdness with cursor jumping as well) ** Show/hide in FSF Emacs. |