-*- outline -*- * Summary of Changes for Proof General 3.5 from 3.4 See also etc/release-log.txt for minor patches. ** Generic changes *** Support for Speedbar and Index menu ("Imenu") Imenu is an alternative to Function Menu (which has been supported for some time, but is not built-in to GNU Emacs). It displays a menu of named definitions, theorems, etc, in the file and allows quick navigation to them. Speedbar displays a file tree in a separate window on the display, allowing quick navigation. Middle/double-clicking or pressing + on a file icon opens up to display tags (definitions, theorems, etc) within the file. Middle/double-clicking on a file or tag jumps to that file/tag. To use Imenu, select Proof General -> Options -> Index Menu. This adds an "Index" menu to the main menu bar. You can also use M-x imenu for keyboard-driven completion. To use Speedbar, use Tools -> Display Speedbar (GNU Emacs), or Proof General -> Advanced -> Speedbar (XEmacs). Or if you prefer the old fashioned way, `M-x speedbar' does the same job. For more about Speedbar, see http://cedet.sourceforge.net/speedbar.shtml *** Improved display management The display handling functions have been overhauled to cope with latest API changes and diversions between Emacs versions. Multiframe mode should now work reasonably well on both Emacs versions, with cut-down frames (no toolbars, etc). There is a new user-level function `proof-layout-windows' which displays windows in a default form for the current display mode. This uses a vertical-horizontal split scheme for three-pane mode (due to Pierre Courtieu), but three-pane mode also works with three-way horizontal split as before. But see note in BUGS for remaining issues. *** More example proofs included Some additional example proofs are included with this release (and we hope to add more). The best and most accurate resource is of course the distribution of each proof assistant, but including some samples in Proof General allows you to see proofs in other systems without having to install them all. The "root2" example proofs of the irrationality of the square root of 2 were proofs written as a response to a challenge of Freek Wiedijk in his comparison of different theorem provers, see http://www.cs.kun.nl/~freek/comparison/. Those proof scripts are copyright by their named authors or as mentioned in the files. *** Improved RPM packages 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. These RPMs are intended to be compatible with the RPMs distributed with Red Hat/Fedora. Please try out these packages and report any problems. *** Desktop integration on freedesktop.org compliant desktops Provided automatically (and only) with the RPM package. Please send in i18n strings, and report any problems on particular desktops (only tested on Fedora Core 1/GNOME). *** Keyboard hints and other messages displayed in minibuffer Hints for keyboard usage and reporting on file processing are now displayed in the minibuffer. If you do not like this behaviour, customize the `pg-show-hints' variable. *** pre-compiled .elc files. NOTE: recompile needed for GNU Emacs Proof General can now be reliably run as compiled code. However, compiled Emacs Lisp files sometimes have incompatibilities between versions (and definitely between GNU Emacs and XEmacs). To recompile the sources for a particular Emacs version, try: make clean make compile Check the settings in the Makefile for your Emacs version. *** Bundling of X-Symbol Mode (4.5.1-beta) To disable use of the bundled version, either delete/move away the x-symbol subdirectory, or load your own local version first [put (require 'x-symbol-hooks) in .emacs, or unpack in your own .xemacs directory]. From now on, PG is not backward compatible with previous X-Symbol versions. Either upgrade your installed version, or be careful to load PG first (so that the bundled version of X-Symbol is used). Notice that the package version of X-Symbol may load itself first by default during XEmacs startup (especially if you have it installed site-wide), so it may be tricky to override. You can prevent this with "xemacs -no-autoloads", but that may result in other needed packages not being loaded! There is an attempt to prevent the built-in version loading in Proof General, but in case of problems, consult your sysadmin to try to prevent global loading of x-symbol. *** Bundling of MMM Mode (for multiple modes in one buffer) MMM mode allows submodes to be used in the same file. See http://mmm-mode.sourceforge.net/. At present it is configured for Isar, to allow LaTeX and sml-mode to be used inside Isar scripts. Contributions of configuration for other provers welcomed. *** X-Symbol (and MMM-mode) minor mode behaviour simplified These minor modes like to be responsible for turning themselves on and off. PG does not anymore try to synchronise the on/off settings in all PG buffers (which could lead to half an hour of fontification!). Instead the menu reflects the current minor mode status; toggling it will also update the default "global for PG" behaviour for new script buffers. *** Movement of cursor on interrupt is disabled By default, the cursor jumps to the end of the locked region on an error. Previously it also jumped on an interrupt. This is configurable via `proof-shell-handle-error-or-interrupt-hook', which see. After an interrupt you may use C-c . to move to the end of the locked region, or C-c ` (backquote) to move to the location given by an error message from the prover. *** Automatic slow-down on fast tracing display Proof General will try to configure itself to update the display of tracing output infrequently when the prover is producing rapid, perhaps voluminous, output. This counteracts the situation that otherwise Emacs may consume more CPU than the proof assistant, trying to fontify and refresh the display as fast as output appears. See `proof-trace-output-slow-catchup' for setting. *** Proof General -> Options menu changes **** Improvement to options handling Facility to reset to default values added, and saving of (just) proof assistant settings. **** Strict read only added Strict read only behaviour for the locked (blue) region can now be enabled/disabled without restarting scripting. (Output hightlighting option has been removed from this menu, but is still available under Advanced -> Customize -> User Options -> .. **** Deactivate Action added This setting controls an automatic action when scripting is deactivated in a partially processed buffer. Ordinarily, PG will query whether to retract or completely process the file. One of these can be chosen as a default action. **** Follow mode: add "followdown" setting In this mode, the point moves with the locked region when it moves down in the buffer (processing). For undo, the point does not move. **** Display management: added shrink-windows-tofit option This option shrinks and expands the display of prover output, within reasonable window sizes, when in 2-window mode. It avoids wasting half the screen with empty space (with the drawback of moving the boundary up and down). Available under PG -> Options -> Display -> Shrink To Fit. *** Add proof-indent-pad-eol setting to prettify locked regions in XEmacs. This works by adding unnecessary spaces to the end of lines when TAB is pressed. *** Parsing internals changed: minor user visible differences Please report any problems/annoyances which may be unexpected. NB: Not yet enabled for Isabelle/Isar. *** Tweaks to menus, colours Electric terminator menu option more visible. Reduce contrast for mouse highlighting of regions. *** Added `proof-shell-identifier-under-mouse-cmd' Allows PG to conveniently send a command to the prover which passes the identifier under the mouse, or the active region, as an argument. Bound globally to Control-Meta-Mouse-button1. Presently only configured in Isabelle/Isar, to parse terms (inside strings) and theorems (outside). ** GNU Emacs compatibility, simplified font-lock, handling nested comments *** Numerous improvements, thanks due to Stefan Monnier. *** Some GNU Emacs backwards compatibility removed: use 21.1 or later ** Changes for Isabelle *** Automatic refreshing of Logics list *** Theorem dependencies: displaying and highlighting dependencies. Dependencies for a theorem (i.e. other theorems,lemmas) can be displayed. Local dependencies within the same file can be highlighted in yellow, and places where a theorem is used are highlighted in orange. This aids editing of theories to remove dead lemmas, re-order proofs, etc. To activate it you need to select the "Theorem Dependencies" option in the Isabelle(/Isar) -> Settings menu. You may need to restart the prover before doing this to gather full dependency information. *** Beginnings of support PGIP protocol (wip with Isabelle2004) This is an internal change. Presently, it allows Isabelle to configure Proof General prover settings menu directly rather than using Elisp. ** Changes for Coq *** Coq 8.0 compatibility. Example files are Coq 8.0 format. **** Possibility to run Coq 8.0 in compatibility mode **** Further prover settings added **** Automatic compilation ("auto-compile-vos"), dependencies managed *** Command coq-intros inserts intros using "Show Intros" output *** Indentation improved *** Menu entries for inserting commands, tactics and terms *** "Holes" system, for editing structured expressions Holes are a powerful feature for complex expression editing. It is inspired from other tools, like Pcoq (http://www-sop.inria.fr/lemme/pcoq/index.html). The principle is simple, holes are pieces of text that can be "filled" by different means. The new menu system makes use of the holes system. Almost all holes operations are available in the Coq/holes menu. Note: Holes and menus make use of emacs abbreviation mechanism, please make sure you don't have an abbrev table defined in you config files (C-h v abbrev-file-name to see the name of the abbreviation file). If there is already such a table, you can do the following to merge with ProofGeneral's abbrev: M-x read-abbrev-file, then find the file named "coq-abbrev.el" in the ProofGeneral/coq directory. At emacs exit you will be asked if you want to save abbrevs, answer yes. *** X-symbols are much improved (more symbols, cleaner grammar) Much more symbols are supported now (C-= C-= for the symbol table). See coq/README for more details, including the syntax of sub/superscripts. ** Additional instances of Proof General *** ccc: Proof General for the Casl Consistency Checker Provided by Christoph Lüth . See http://www.informatik.uni-bremen.de/cofi/ccc for more information. *** pgshell: Proof General for shell scripts/simple command interpreters. This instance of PG is handy just for using script management to cut-and-paste into a buffer running an ordinary shell or tool with a command-line interpreter of some kind. Provides an instant and cheap interface to command-line interpreters, to avoid tiresomely using cut-and-paste to run pre-recorded commands.