This is ProofGeneral.info, produced by makeinfo version 4.8 from ProofGeneral.texi. START-INFO-DIR-ENTRY * Proof General: (ProofGeneral). Organize your proofs with Emacs! END-INFO-DIR-ENTRY  File: ProofGeneral.info, Node: Top, Next: Preface, Up: (dir) Proof General ************* This file documents version 3.6 of Proof General, a generic Emacs interface for proof assistants. Proof General 3.6 has been tested with XEmacs 21.4.15 and GNU Emacs 21.3.1. It is supplied ready to use for the proof assistants LEGO, Coq, Isabelle, and PhoX. Experimental support is provided for several other provers. * Menu: * Preface:: * Introducing Proof General:: * Basic Script Management:: * Subterm Activation and Proof by Pointing:: * Advanced Script Management:: * Support for other Packages:: * Customizing Proof General:: * Hints and Tips:: * LEGO Proof General:: * Coq Proof General:: * Isabelle Proof General:: * HOL Proof General:: * Shell Proof General:: * Obtaining and Installing:: * Known Bugs:: * References:: * History of Proof General:: * Function Index:: * Variable Index:: * Keystroke Index:: * Concept Index::  File: ProofGeneral.info, Node: Preface, Next: Introducing Proof General, Prev: Top, Up: Top Preface ******* Welcome to Proof General! This preface has some news about the current release, future plans, and acknowledgements to those who have helped along the way. The appendix *Note History of Proof General:: contains old news about previous releases, and notes on the development of Proof General. Proof General has a home page at `http://proofgeneral.inf.ed.ac.uk'. Visit this page for the latest version of this manual, other documentation, system downloads, etc. * Menu: * Latest news for 3.5 and 3.6:: * Future:: * Credits::  File: ProofGeneral.info, Node: Latest news for 3.5 and 3.6, Next: Future, Up: Preface Latest news for 3.6 =================== Proof General versions 3.6 (and 3.5 shortly before it) collect together a cummulative set of improvements to Proof General 3.4. There are compatibility fixes for newer Emacs versions, and particularly for GNU Emacs: credit is due to Stefan Monnier for an intense period of debugging and patching. The options menu has been simplified and extended, and the display management is improved and repaired for Emacs API changes. There are some other usability improvements, prompted in part by feedback after Proof General's appearance at the TYPES 2002 Summer School. Support has been added for the useful Emacs packages Speedbar and Index Menu, both usually distributed with Emacs. Compatible versions of the Emacs packages X-Symbol (for mathematical symbols) and MMM Mode (for multiple modes in one buffer) are now bundled with Proof General to save the need for additional downloads. Proof General 3.6 runs reliably as compiled Elisp code, and is available in RPM package format which includes desktop integration on freedesktop.org compliant desktops (including, for example, many recent Linux distributions). See the `CHANGES' file in the distribution for more complete details of changes since version 3.4, and the appendix *Note History of Proof General:: for old news.  File: ProofGeneral.info, Node: Future, Next: Credits, Prev: Latest news for 3.5 and 3.6, Up: Preface Future ====== The aim of the Proof General project is to provide a powerful and configurable interfaces which help user-interaction with interactive proof assistants. The strategy Proof General uses is to targets power users rather than novices; other interfaces have often neglected this class of users. But we do include general user interface niceties, such as toolbar and menus, which make use easier for all. Proof General has been Emacs based so far, but plans are afoot to liberate it from the points and parentheses of Emacs Lisp. The successor project Proof General Kit proposes that proof assistants use a standard XML-based protocol for interactive proof, dubbed PGIP. PGIP will enable middleware for interactive proof tools and interface components. Rather than configuring Proof General for your proof assistant, you will need to configure your proof assistant to understand PGIP. There is a similarity however; the design of PGIP was based heavily on the Emacs Proof General framework. In 2004 a project to develop PGIP inside the Eclipse IDE will begin. There is also a prototype version of a PGIP-enabled Isabelle under development, and a middleware component for co-ordinating proof written in Haskell. Further collaborations are sought for more developments, especially the PGIP enabling of other provers. For more details, see the Proof General Kit webpage (http://proofgeneral.inf.ed.ac.uk/kit). Help us to help you organize your proofs!  File: ProofGeneral.info, Node: Credits, Prev: Future, Up: Preface Credits ======= The original developers of the basis of Proof General were: * David Aspinall, * Healfdene Goguen, * Thomas Kleymann, and * Dilip Sequeira. LEGO Proof General (the successor of `lego-mode') was written by Thomas Kleymann and Dilip Sequeira. It is presently maintained by David Aspinall and Paul Callaghan . Coq Proof General was written by Healfdene Goguen, with later contributions from Patrick Loiseleur. It is now maintained by Pierre Courtieu . Isabelle Proof General was written and is being maintained by David Aspinall . It has benefited greatly from tweaks and suggestions by Markus Wenzel , who wrote Isabelle/Isar Proof General and added Proof General support inside Isabelle. David von Oheimb supplied the original patches for X-Symbol support, which improved Proof General significantly. Christoph Wedler, the author of X-Symbol, has provided much useful support in adapting his package for PG. The generic base for Proof General was developed by Kleymann, Sequeira, Goguen and Aspinall. It follows some of the ideas used in Project CROAP (http://www.inria.fr/croap/). The project to implement a proof mode for LEGO was initiated in 1994 and coordinated until October 1998 by Thomas Kleymann, becoming generic along the way. In October 1998, the project became Proof General and has been managed by David Aspinall since then. This manual was written by David Aspinall and Thomas Kleymann. Some words found their way here from the user documentation of LEGO mode, prepared by Dilip Sequeira. Healfdene Goguen supplied some text for Coq Proof General. Since Proof General 2.0, this manual has been maintained and improved by David Aspinall. Pierre Courtieu and Markus Wenzel contributed some sections. The Proof General project has benefited indirectly from funding by EPSRC (Applications of a Type Theory Based Proof Assistant), the EC (Types for Proofs and Programs) and the support of the LFCS. Version 3.1 was prepared whilst David Aspinall was visiting ETL, Japan, supported by the British Council. For testing and feedback for older versions of Proof General, thanks go to Rod Burstall, Martin Hofmann, and James McKinna, and some of those who continued to help with the latest 3.x series, named next. During the development of Proof General 3.x releases, many people helped provide testing and other feedback, including the Proof General maintainers, Paul Callaghan, Pierre Courtieu, and Markus Wenzel, Stefan Berghofer, Gerwin Klein, and other folk who tested pre-releases or sent bug reports, including Cuihtlauac Alvarado, Lennart Beringer, Pascal Brisset, James Brotherston, Martin Buechi, Lucas Dixon, Matt Fairtlough, Kim Hyung Ho, Greg O'Keefe, Pierre Lescanne, John Longley, Stefan Monnier, Tobias Nipkow, Leonor Prensa Nieto, David von Oheimb, Lawrence Paulson, Paul Roziere, Randy Pollack, Robert R. Schneck, Norbert Schirmer, Sebastian Skalberg, Mike Squire, and Norbert Voelker. Thanks to all of you (and apologies to anyone missed).  File: ProofGeneral.info, Node: Introducing Proof General, Next: Basic Script Management, Prev: Preface, Up: Top 1 Introducing Proof General *************************** "Proof General" is a generic Emacs interface for interactive proof assistants,(1) developed at the LFCS in the University of Edinburgh. It works best under XEmacs, but can also be used with GNU Emacs. You do not have to be an Emacs militant to use Proof General! The interface is designed to be very easy to use. You develop your proof script(2) in-place rather than line-by-line and later reassembling the pieces. Proof General keeps track of which proof steps have been processed by the prover, and prevents you editing them accidently. You can undo steps as usual. The aim of Proof General is to provide a powerful and configurable interface for numerous interactive proof assistants. We target Proof General mainly at intermediate or expert users, so that the interface should be useful for large proof developments. Please help us! Send us comments, suggestsions, or (the best) patches to improve support for your chosen proof assistant. Contact us at `da+pg-support@inf.ed.ac.uk'. If your chosen proof assistant isn't supported, read the accompanying Adapting Proof General manual to find out how to configure PG for a new prover. * Menu: * Quick start guide:: * Features of Proof General:: * Supported proof assistants:: * Prerequisites for this manual:: * Organization of this manual:: ---------- Footnotes ---------- (1) A "proof assistant" is a computerized helper for developing mathematical proofs. For short, we sometimes call it a "prover", although we always have in mind an interactive system rather than a fully automated theorem prover. (2) A "proof script" is a sequence of commands which constructs a proof, usually stored in a file.  File: ProofGeneral.info, Node: Quick start guide, Next: Features of Proof General, Up: Introducing Proof General 1.1 Quick start guide ===================== Proof General may have been installed for you already. If so, when you visit a proof script file for your proof assistant, the corresponding Proof General mode will be invoked automatically: Prover Extensions Mode LEGO `.l' `lego-mode' Coq `.v' `coq-mode' Isabelle/Isar `.thy' `isar-mode' Isabelle `.thy',`.ML' `isa-mode' Phox `.phx' `phox-mode' HOL98 `.sml' `hol98-mode' ACL2 `.acl2' `acl2-mode' Twelf `.elf' `twelf-mode' Plastic `.lf' `plastic-mode' Lambda-CLAM `.lcm' `lclam-mode' CCC `.ccc' `ccc-mode' PG-Shell `.pgsh' `pgshell-mode' (The exact list of Proof Assistants supported may vary according to the version of Proof General and its local configuration). You can also invoke the mode command directly, e.g., type `M-x lego-mode', to turn a buffer into a lego script buffer. You'll find commands to process the proof script are available from the toolbar, menus, and keyboard. Type `C-h m' to get a list of the keyboard shortcuts for the current mode. The commands available should be easy to understand, but the rest of this manual describes them in some detail. The proof assistant itself is started automatically inside Emacs as an "inferior" process when you ask for some of the proof script to be processed. You can start the proof assistant manually with the menu command "Start proof assistant". To follow an example use of Proof General on a Isabelle proof, *note Walkthrough example in Isabelle/Isar::. If you know the syntax for proof scripts in another theorem prover, you can easily adapt the details given there. If Proof General has not already been installed, you should insert the line: (load "PROOF-GENERAL-HOME/generic/proof-site.el") into your `~/.emacs' file, where PROOF-GENERAL-HOME is the top-level directory that was created when Proof General was unpacked. *Note Obtaining and Installing::, if you need more information.  File: ProofGeneral.info, Node: Features of Proof General, Next: Supported proof assistants, Prev: Quick start guide, Up: Introducing Proof General 1.2 Features of Proof General ============================= Why would you want to use Proof General? Proof General is designed to be useful for novices and expert users alike. It will be useful to you if you use a proof assistant, and you'd like an interface with the following features: simplified interaction, script management, multiple file scripting, a script editing mode, proof by pointing, toolbar and menus, syntax highlighting, real symbols, functions menu, tags, and finally, adaptability. Here is an outline of some of these features. Look in the contents page or index of this manual to find out about the others! * Simplified interaction Proof General is designed for proof assistants which have a command-line shell interpreter. When using Proof General, the proof assistant's shell is hidden from the user. Communication takes place via three buffers (Emacs text widgets). Communication takes place via three buffers. The "script buffer" holds input, the commands to construct a proof. The "goals buffer" displays the current list of subgoals to be solved. The "response buffer" displays other output from the proof assistant. By default, only two of these three buffers are displayed. This means that the user normally only sees the output from the most recent interaction, rather than a screen full of output from the proof assistant. Proof General does not commandeer the proof assistant shell: the user still has complete access to it if necessary. For more details, *note Summary of Proof General buffers:: and *note Display customization::. * Script management Proof General colours proof script regions blue when they have been processed by the prover, and colours regions red when the prover is currently processing them. The appearance of Emacs buffers always matches the proof assistant's state. Coloured parts of the buffer cannot be edited. Proof General has functions for _asserting_ or _retracting_ parts of a proof script, which alters the coloured regions. For more details, *note Basic Script Management::, *Note Script processing commands::, and *Note Advanced Script Management::. * Script editing mode Proof General provides useful facilities for editing proof scripts, including syntax hilighting and a menu to jump to particular goals, definitions, or declarations. Special editing functions send lines of proof script to the proof assistant, or undo previous proof steps. For more details, *note Script editing commands::, and *Note Script processing commands::. * Toolbar and menus A script buffer has a toolbar with navigation buttons for processing parts of the proof script. A menu provides further functions for operations in the proof assistant, as well as customization of Proof General. For more details, *note Toolbar commands::, *Note Proof assistant commands::, and *Note Customizing Proof General::. * Proof by pointing Proof General has support for proof-by-pointing and similar features. Proof by pointing allows you to click on a subterm of a goal to be proved, and automatically apply an appropriate proof rule or tactic. Proof by pointing is specific to the proof assistant (and logic) in use; therefore it is configured mainly on the proof assistant side. If you would like to see proof by pointing support for Proof General in a particular proof assistant, petition the developers of the proof assistant to provide it.  File: ProofGeneral.info, Node: Supported proof assistants, Next: Prerequisites for this manual, Prev: Features of Proof General, Up: Introducing Proof General 1.3 Supported proof assistants ============================== Proof General comes ready-customized for several proof assistants, including these: * LEGO Proof General for LEGO Version 1.3.1 *Note LEGO Proof General::, for more details. * Coq Proof General for Coq Version 6.3, 7.x, 8.x *Note Coq Proof General::, for more details. * Isabelle Proof General for Isabelle2004 *Note Isabelle Proof General::, for more details. * Isabelle/Isar Proof General for Isabelle2004 *Note Isabelle Proof General::, and documentation supplied with Isabelle for more details. * HOL Proof General for HOL98 (HOL4) *Note HOL Proof General::, for more details. * Shell Proof General for shell scripts (not really a proof assistant!) *Note Shell Proof General::, for more details. Proof General is designed to be generic, so if you know how to write regular expressions, you can make: * Your Proof General for your favourite proof assistant. For more details of how to make Proof General work with another proof assistant, see the accompanying manual Adapting Proof General. The exact list of Proof Assistants supported may vary according to the version of Proof General you have and its local configuration; only the standard instances documented in this manual are listed above. Note that there is some variation between the features supported by different instances of Proof General. The main variation is proof by pointing, which is only supported in LEGO at the moment. For advanced features like this, some extensions to the output routines of the proof assistant are required, typically. If you like Proof General, please help us by asking the implementors of your favourite proof assistant to support Proof General as much as possible.  File: ProofGeneral.info, Node: Prerequisites for this manual, Next: Organization of this manual, Prev: Supported proof assistants, Up: Introducing Proof General 1.4 Prerequisites for this manual ================================= This manual assumes that you understand a little about using Emacs, for example, switching between buffers using `C-x b' and understanding that a key sequence like `C-x b' means "control with x, followed by b". A key sequence like `M-z' means "meta with z". ( may be labelled on your keyboard). The manual also assumes you have a basic understanding of your proof assistant and the language and files it uses for proof scripts. But even without this, Proof General is not useless: you can use the interface to _replay_ proof scripts for any proof assistant without knowing how to start it up or issue commands, etc. This is the beauty of a common interface mechanism. To get more from Proof General and adapt it to your liking, it helps to know a little bit about how Emacs lisp packages can be customized via the Customization mechanism. It's really easy to use. For details, *note How to customize::. *note ((xemacs))Easy customization::, for documentation in XEmacs. To get the absolute most from Proof General, to improve it or to adapt it for new provers, you'll need to know a little bit of Emacs lisp. Emacs is self-documenting, so you can begin from `C-h' and find out everything! Here are some useful commands: `C-h i' `info' `C-h m' `describe-mode' `C-h b' `describe-bindings' `C-h f' `describe-function' `C-h v' `describe-variable'  File: ProofGeneral.info, Node: Organization of this manual, Prev: Prerequisites for this manual, Up: Introducing Proof General 1.5 Organization of this manual =============================== This manual covers the user-level view and customization of Proof General. The accompanying Adapting Proof General manual considers adapting Proof General to new proof assistants, and documents some of the internals of Proof General. Three appendices of this manual contain some details about obtaining and installing Proof General and some known bugs. The contents of these final chapters is also covered in the files `INSTALL' and `BUGS' contained in the distribution. Refer to those files for the latest information. The manual concludes with some references and indexes. See the table of contents for full details.  File: ProofGeneral.info, Node: Basic Script Management, Next: Subterm Activation and Proof by Pointing, Prev: Introducing Proof General, Up: Top 2 Basic Script Management ************************* This chapter is an introduction to using the script management facilities of Proof General. We begin with a quick walkthrough example, then describe the concepts and functions in more detail. * Menu: * Walkthrough example in Isabelle/Isar:: * Proof scripts:: * Script buffers:: * Summary of Proof General buffers:: * Script editing commands:: * Script processing commands:: * Proof assistant commands:: * Toolbar commands:: * Interrupting during trace output::  File: ProofGeneral.info, Node: Walkthrough example in Isabelle/Isar, Next: Proof scripts, Up: Basic Script Management 2.1 Walkthrough example in Isabelle/Isar ======================================== Here's a short example in Isabelle/Isar to see how script management is used. The file you are asked to type below is included in the distribution as `isar/Example.thy'. If you're not using Isabelle, substitute some lines from a simple proof for your proof assistant, or consult the example file supplied with Proof General for your prover, called something like `foo/example.foo' for a proof assistant Foo. This walkthrough is keyboard based, but you could easily use the toolbar and menu functions instead. The best way to learn Emacs key bindings is by using the menus. You'll find the keys named below listed on the menus. * First, start Emacs with Proof General loaded. According to how you have installed Proof General, this may be by typing `proofgeneral', selecting it from a menu, or simply by starting Emacs itself. * Next, find a new file by `C-x C-f' and typing as the filename `Walkthrough.thy'. This should load Isabelle Proof General and the toolbar and Proof General menus will appear. You should have an empty buffer displayed. The notation `C-x C-f' means control key with `x' followed by control key with `f'. This is a standard notation for Emacs key bindings, used throughout this manual. This function also appears on the `File' menu of Emacs. The remaining commands used will be on the `Proof-General' menu. If you're not using Isabelle, you must choose a different file extension, appropriately for your proof assistant. If you don't know what to use, see the previous chapter for the list of supported assistants and file extensions. * Turn on "electric terminator" by typing `C-c ;' and enter: theory Walkthrough = Main:; This first command begins the definition of a new theory inside Isabelle, which extends the theory `Main'. (We're assuming that you have Isabelle/HOL available, which declares the `Main' theory. You should be able to see the list of installed logics in Isabelle on the `Logics' menu). Electric terminator sends commands to the proof assistant as you type them. The exact key binding is based on the terminator used for your proof assistant, but you can always check the menu if you're not sure. Electric terminator mode is popular, but not enabled by default because of the principle of least surprise. You can customize Proof General to enable it everytime if you want, *Note Customizing Proof General::. For this option, customization is particularly easy: just use the menu item `Proof General -> Options' to select some common options, and `Proof General -> Options -> Save Options' to save your choices. At the moment you type the semicolon, the `theory' command will be sent to Isabelle behind the scenes. First, there is a short delay while Isabelle is launched; you may see a welcome message. Then, you may notice that the command briefly is given an orange/pink background (or shown in inverse video if you don't have a colour display), before you see a window containing text like this: theory Walkthrough = {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp, Sum_Type, Relation, Record, Inductive, Transitive_Closure, Wellfounded_Recursion, Ring_and_Field, Nat, NatArith, Divides, Power, Finite_Set, Equiv, IntDef, Datatype_Universe, Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv, NatBin, NatSimprocs, SetInterval, Presburger, Relation_Power, Parity, PreList, List, Map, Hilbert_Choice, Infinite_Set, Extraction, Refute, Main, #} (Which gives you some idea of the theories that go to build up `Main'!). In this case of this first command, it is hard to see the orange/pink stage because the command is processed very quickly on most machines. But in general, processing commands can take an arbitrary amount of time (or not terminate at all). For this reason, Proof General maintains a queue of commands which are sent one-by-one from the proof script. As Isabelle successfully processes commands in the queue, they will turn from the orange/pink colour into blue. The blue regions indicate text that has been read by the prover and should not be edited; for this reason it is made read-only, by default. * Next type (on a new line if you like): theorem my_theorem: "A & B --> B & A"; The goal should be displayed in the goals buffer. * Now type: proof; assume "A & C"; This will update the goals buffer. But whoops! That was the wrong command, we typed `C' instead of `B'. * Press `C-c C-BS' to pretend that didn't happen. Note: `BS' means the backspace key. This key press sends an undo command to Isabelle, and deletes the `assume' command from the proof script. If you just want to undo without deleting, you can type `C-c C-u' instead, or use the toolbar navigation button. * Instead, let's try: assume "A & B"; Which is better. From this assumption we can get `B' and `A' by the trivial step `..' then obtain B and A .. Notice that this line doesn't have a terminator character -- but in fact, Isar does not need them to parse the file, and neither does Proof General (except for the electric effect). You can process the text up to the current position of the point with the key `C-c C-RET'. This is probably a more common way of working in Isabelle Proof General than using the electric terminator, to avoid cluttering the proof script with semicolons. After this proof step, the message from Isabelle indicates that the proof has succeeded, so we can conclude the proof with the `qed' command. * Finally, type: qed This last command closes the proof and saves the proved theorem. Moving the mouse pointer over the locked region now reveals that the entire proof has been aggregated into a single segment (if you did this before, you would see highlighting of each command separately). This reflects the fact that Isabelle has thrown away the history of the proof, so if we want to undo now, the whole proof must be retracted. * Suppose we decide to call the theorem something more sensible. Move the cursor up into the locked region, somewhere between `theorem' and `qed', enter `C-c C-RET'. You see that the locked segment for the whole proof is now unlocked (and uncoloured): it is transferred back into the editing region. The command `C-c C-RET' moves the end of the locked region to the cursor position, or as near as possible above or below it, sending undoing commands or proof commands as necessary. In this case, the locked region will always be moved back to the end of the `theory' line, since that is the closest possible position to the cursor that appears before it. * Now improve the goal name, for example: theorem and_commutes: "A & B --> B & A" You can swiftly replay the rest of the buffer now with `C-c C-b' (or the down arrow on the toolbar). * At the end of the buffer, you may insert the command end to complete the theory. Note that once a theory is completed in Isabelle, you cannot undo into it, again because Isabelle discards the history of the theory's creation. Just like completed proofs, there is no option other than undoing the whole theory. To prevent you doing this inadvertently, however (maybe undoing many proofs which are time-consuming to replay), the `C-c C-u' or `C-c C-RET' commands will generate an error message, typically: *** Cannot undo "end" *** At command "cannot_undo". If you really want to retract the theory for editing once more, you can use the key `C-c C-r' (which corresponds to the up arrow on the toolbar). Finally, once you are happy with your theory, you should save the file with `C-x C-s' before moving on to edit another file or exiting Emacs. If you forget to do this, Proof General or Emacs will surely prompt you sooner or later!  File: ProofGeneral.info, Node: Proof scripts, Next: Script buffers, Prev: Walkthrough example in Isabelle/Isar, Up: Basic Script Management 2.2 Proof scripts ================= A "proof script" is a sequence of commands which constructs definitions, declarations, theories, and proofs in a proof assistant. Proof General is designed to work with text-based interactive proof assistants, where the mode of working is usually a dialogue between the human and the proof assistant. Primitive interfaces for proof assistants simply present a "shell" (command interpreter) view of this dialogue: the human repeatedly types commands to the shell until the proof is completed. The system responds at each step, perhaps with a new list of subgoals to be solved, or perhaps with a failure report. Proof General manages the dialogue to show the human only the information which is relevant at each step. Often we want to keep a record of the proof commands used to prove a theorem, to build up a library of proved results. An easy way to store a proof is to keep a text file which contains a proof script; proof assistants usually provide facilities to read a proof script from a file instead of the terminal. Using the file, we can "replay" the proof script to prove the theorem again. Using only a primitive shell interface, it can be tedious to construct proof scripts with cut-and-paste. Proof General helps out by issuing commands directly from a proof script file, while it is being written and edited. Proof General can also be used conveniently to replay a proof step-by-step, to see the progress at each stage. "Scripting" is the process of building up a proof script file or replaying a proof. When scripting, Proof General sends proof commands to the proof assistant one at a time, and prevents you from editing commands which have been successfully completed by the proof assistant, to keep synchronization. Regions of the proof script are analysed based on their syntax and the behaviour of the proof assistant after each proof command.  File: ProofGeneral.info, Node: Script buffers, Next: Summary of Proof General buffers, Prev: Proof scripts, Up: Basic Script Management 2.3 Script buffers ================== A "script buffer" is a buffer displaying a proof script. Its Emacs mode is particular to the proof assistant you are using (but it inherits from "proof-mode"). A script buffer is divided into three regions: _locked_, _queue_ and _editing_. The proof commands in the script buffer can include a number of _Goal-save sequences_. * Menu: * Locked queue and editing regions:: * Goal-save sequences:: * Active scripting buffer::  File: ProofGeneral.info, Node: Locked queue and editing regions, Next: Goal-save sequences, Up: Script buffers 2.3.1 Locked, queue, and editing regions ---------------------------------------- The three regions that a script buffer is divided into are: * The _locked_ region, which appears in blue (underlined on monochrome displays) and contains commands which have been sent to the proof process and verified. The commands in the locked region cannot be edited. * The _queue_ region, which appears in pink (inverse video) and contains commands waiting to be sent to the proof process. Like those in the locked region, these commands can't be edited. * The _editing_ region, which contains the commands the user is working on, and can be edited as normal Emacs text. These three regions appear in the buffer in the order above; that is, the locked region is always at the start of the buffer, and the editing region always at the end. The queue region only exists if there is input waiting to be processed by the proof process. Proof General has two fundamental operations which transfer commands between these regions: _assertion_ (or processing) and _retraction_ (or undoing). *Assertion* causes commands from the editing region to be transferred to the queue region and sent one by one to the proof process. If the command is accepted, it is transferred to the locked region, but if an error occurs it is signalled to the user, and the offending command is transferred back to the editing region together with any remaining commands in the queue. Assertion corresponds to processing proof commands, and makes the locked region grow. *Retraction* causes commands to be transferred from the locked region to the editing region (again via the queue region) and the appropriate 'undo' commands to be sent to the proof process. Retraction corresponds to undoing commands, and makes the locked region shrink. For details of the commands available for doing assertion and retraction, *Note Script processing commands::.  File: ProofGeneral.info, Node: Goal-save sequences, Next: Active scripting buffer, Prev: Locked queue and editing regions, Up: Script buffers 2.3.2 Goal-save sequences ------------------------- A proof script contains a sequence of commands used to prove one or more theorems. As commands in a proof script are transferred to the locked region, they are aggregated into segments which constitute the smallest units which can be undone. Typically a segment consists of a declaration or definition, or all the text from a "goal" command to the corresponding "save" command, or the individual commands in the proof of an unfinished goal. As the mouse moves over the the region, the segment containing the pointer will be highlighted. Proof General therefore assumes that the proof script has a series of proofs which look something like this: goal MYTHM is G ... save theorem MYTHM interspersed with comments, definitions, and the like. Of course, the exact syntax and terminology will depend on the proof assistant you use. The name MYTHM can appear in a menu for the proof script to help quickly find a proof (*note Imenu and Speedbar (and Function Menu)::).  File: ProofGeneral.info, Node: Active scripting buffer, Prev: Goal-save sequences, Up: Script buffers 2.3.3 Active scripting buffer ----------------------------- You can edit as many script buffers as you want simultaneously, but only one buffer at a time can be used to process a proof script incrementally: this is the "active scripting buffer". The active scripting buffer has a special indicator: the word `Scripting' appears in its mode line. When you use a scripting command, it will automatically turn a buffer into the active scripting mode. You can also do this by hand, via the menu command 'Toggle Scripting' or the key `C-c C-s'. `C-c C-s' `proof-toggle-active-scripting' When active scripting mode is turned on, several things may happen to get ready for scripting (exactly what happens depends on which proof assistant you are using and some user settings). First, the proof assistant is started if it is not already running. Second, a command is sent to the proof assistant to change directory to the directory of the current buffer. If the current buffer corresponds to a file, this is the directory the file lives in. This is in case any scripting commands refer to files in the same directory as the script. The third thing that may happen is that you are prompted to save some unsaved buffers. This is in case any scripting commands may read in files which you are editing. Finally, some proof assistants may automatically read in files which the current file depends on implicitly. In Isabelle, for example, there is an implicit dependency between a `.ML' script file and a `.thy' theory file which defines its theory. If you have a partly processed scripting buffer and use `C-c C-s', or you attempt to use script processing in a new buffer, Proof General will ask you if you want to retract what has been proved so far, `Scripting incomplete in buffer myproof.l, retract?' or if you want to process the remainder of the active buffer, `Completely process buffer myproof.l instead?' before you can start scripting in a new buffer. If you refuse to do either, Proof General will give an error message: `Cannot have more than one active scripting buffer!'. To turn off active scripting, the buffer must be completely processed (all blue), or completely unprocessed. There are two reasons for this. First, it would certainly be confusing if it were possible to split parts of a proof arbitrarily between different buffers; the dependency between the commands would be lost and it would be tricky to replay the proof.(1) Second, we want to interface with file management in the proof assistant. Proof General assumes that a proof assistant may have a notion of which files have been processed, but that it will only record files that have been completely processed. For more explanation of the handling of multiple files, *Note Switching between proof scripts::. -- Command: proof-toggle-active-scripting &optional arg Toggle active scripting mode in the current buffer. With ARG, turn on scripting iff ARG is positive. ---------- Footnotes ---------- (1) Some proof assistants provide some level of support for switching between multiple concurrent proofs, but Proof General does not use this. Generally the exact context for such proofs is hard to define to easily split them into multiple files.  File: ProofGeneral.info, Node: Summary of Proof General buffers, Next: Script editing commands, Prev: Script buffers, Up: Basic Script Management 2.4 Summary of Proof General buffers ==================================== Proof General manages several kinds of buffers in Emacs. Here is a summary of the different kinds of buffers you will use when developing proofs. * The "proof shell buffer" is an Emacs shell buffer used to run your proof assistant. Usually it is hidden from view (but *note Escaping script management::). Communication with the proof shell takes place via two or three intermediate buffers. * A "script buffer", as we have explained, is a buffer for editing a proof script. The "active scripting buffer" is the script buffer which is currently being used to send commands to the proof shell. * The "goals buffer" displays the list of subgoals to be solved for a proof in progress. During a proof it is usually displayed together with the script buffer. The goals buffer has facility for "proof-by-pointing". * The "response buffer" displays other output from the proof assistant, for example error messages or informative messages. The response buffer is displayed whenever Proof General puts a new message in it. * The "trace buffer" is a special version of the response buffer. It may be used to display unusual debugging output from the prover, for example, tracing proof tactics or rewriting procedures. This buffer is also displayed whenever Proof General puts a new message in it (although it may be quickly replaced with the response or goals buffer in two-buffer mode). Normally Proof General will automatically reveal and hide the goals and response buffers as necessary during scripting. However there are ways to customize the way the buffers are displayed (*note Display customization::). The menu `Proof General -> Buffers' provides a convenient way to display or switch to a Proof General buffer: the active scripting buffer; the goal or response buffer; the tracing buffer; or the shell buffer. Another command on this menu, `Clear Responses', clears the response and tracing buffer.  File: ProofGeneral.info, Node: Script editing commands, Next: Script processing commands, Prev: Summary of Proof General buffers, Up: Basic Script Management 2.5 Script editing commands =========================== Proof General provides a few functions for editing proof scripts. The generic functions mainly consist of commands to navigate within the script. Specific proof assistant code may add more to these basics. Indentation is controlled by the user option `proof-script-indent' (*note User options::). When indentation is enabled, Proof General will indent lines of proof script with the usual Emacs functions, particularly `TAB', `indent-for-tab-command'. Unfortunately, indentation in Proof General 3.6 is somewhat slow. Therefore with large proof scripts, we recommend `proof-script-indent' is turned off. Here are the commands for moving around in a proof script, with their default key-bindings: `C-c C-a' `proof-goto-command-start' `C-c C-e' `proof-goto-command-end' `C-c C-.' `proof-goto-end-of-locked' -- Command: proof-goto-command-start Move point to start of current (or final) command of the script. -- Command: proof-goto-command-end Set point to end of command at point. The variable `proof-terminal-char' is a prover-specific character to terminate proof commands. LEGO and Isabelle use a semicolon, `;'. Coq employs a full-stop `.'. -- Command: proof-goto-end-of-locked &optional switch Jump to the end of the locked region, maybe switching to script buffer. If called interactively or SWITCH is non-nil, switch to script buffer. If called interactively, a mark is set at the current location with ``push-mark'' During the course of a large proof, it may be useful to copy previous commands. As you move the mouse over previous portions of the script, you'll notice that each proof command is highlighted individually. (Once a goal...save sequence is "closed", the whole sequence is highlighted). There is a useful mouse binding for copying the highlighted command under the mouse: `C-button1' `proof-mouse-track-insert' -- Command: proof-mouse-track-insert Copy highlighted command under the mouse to point. Ignore comments. If there is no command under the mouse, behaves like `mouse-track-insert'. Read the documentation in Emacs to find out about the normal behaviour of `proof-mouse-track-insert', if you don't already know what it does.  File: ProofGeneral.info, Node: Script processing commands, Next: Proof assistant commands, Prev: Script editing commands, Up: Basic Script Management 2.6 Script processing commands ============================== Here are the commands for asserting and retracting portions of the proof script, together with their default key-bindings. Sometimes assertion and retraction commands can only be issued when the queue is empty. You will get an error message `Proof Process Busy!' if you try to assert or retract when the queue is being processed.(1) `C-c C-n' `proof-assert-next-command-interactive' `C-c C-u' `proof-undo-last-successful-command' `C-c C-BS' `proof-undo-and-delete-successful-command' `C-c C-RET' `proof-goto-point' `C-c C-b' `proof-process-buffer' `C-c C-r' `proof-retract-buffer' `C-c TERMINATOR-CHARACTER' `proof-electric-terminator-toggle' The last command, `proof-electric-terminator-toggle', is triggered using the character which terminates proof commands for your proof assistant's script language. For LEGO and Isabelle, use `C-c ;', for Coq, use `C-c .'. This not really a script processing command. Instead, if enabled, it causes subsequent key presses of `;' or `.' to automatically activate `proof-assert-next-command-interactive' for convenience. Rather than use a file command inside the proof assistant to read a proof script, a good reason to use `C-c C-b' (`proof-process-buffer') is that with a faulty proof script (e.g., a script you are adapting to prove a different theorem), Proof General will stop exactly where the proof script fails, showing you the error message and the last processed command. So you can easily continue development from exactly the right place in the script. Here is the full set of script processing commands. -- Command: proof-assert-next-command-interactive Process until the end of the next unprocessed command after point. If inside a comment, just process until the start of the comment. -- Command: proof-undo-last-successful-command Undo last successful command at end of locked region. -- Command: proof-undo-and-delete-last-successful-command Undo and delete last successful command at end of locked region. Useful if you typed completely the wrong command. Also handy for proof by pointing, in case the last proof-by-pointing command took the proof in a direction you don't like. Notice that the deleted command is put into the Emacs kill ring, so you can use the usual `yank' and similar commands to retrieve the deleted text. -- Command: proof-goto-point Assert or retract to the command at current position. Calls `proof-assert-until-point' or `proof-retract-until-point' as appropriate. -- Command: proof-process-buffer Process the current (or script) buffer, and maybe move point to the end. -- Command: proof-retract-buffer Retract the current buffer, and maybe move point to the start. -- Command: proof-electric-terminator-toggle arg Toggle ``proof-electric-terminator-enable''. With ARG, turn on iff ARG>0. This function simply uses `customize-set-variable' to set the variable. It was constructed with ``proof-deftoggle-fn''. -- Command: proof-assert-until-point-interactive Process the region from the end of the locked-region until point. Default action if inside a comment is just process as far as the start of the comment. -- Command: proof-retract-until-point-interactive &optional delete-region Tell the proof process to retract until point. If invoked outside a locked region, undo the last successfully processed command. If called with a prefix argument (DELETE-REGION non-nil), also delete the retracted region from the proof-script. As experienced Emacs users will know, a prefix argument is a numeric argument supplied by some key sequence typed before a command key sequence. You can supply a specific number by typing with the digits, or a "universal" prefix of `C-u'. See *note ((xemacs))Arguments:: for more details. Several Proof General commands, like `proof-retract-until-point-interactive', may accept a prefix argument to adjust their behaviour somehow. ---------- Footnotes ---------- (1) In fact, this is an unnecessary restriction imposed by the original design of Proof General. There is nothing to stop future versions of Proof General allowing the queue region to be extended or shrunk, whilst the prover is processing it. Proof General 3.0 already relaxes the original design, by allowing successive assertion commands without complaining.  File: ProofGeneral.info, Node: Proof assistant commands, Next: Toolbar commands, Prev: Script processing commands, Up: Basic Script Management 2.7 Proof assistant commands ============================ There are several commands for interacting with the proof assistant and Proof General, which do not involve the proof script. Here are the key-bindings and functions. `C-c C-l' `proof-display-some-buffers' `C-c C-p' `proof-prf' `C-c C-t' `proof-ctxt' `C-c C-h' `proof-help' `C-c C-f' `proof-find-theorems' `C-c C-w' `pg-response-clear-displays' `C-c C-c' `proof-interrupt-process' `C-c C-v' `proof-minibuffer-cmd' `C-c C-s' `proof-shell-start' `C-c C-x' `proof-shell-exit' -- Command: proof-display-some-buffers Display the reponse, trace, goals, or shell buffer, rotating. A fixed number of repetitions of this command switches back to the same buffer. Also move point to the end of the response buffer if it's selected. If in three window or multiple frame mode, display two buffers. The idea of this function is to change the window->buffer mapping without adjusting window layout. -- Command: proof-prf Show the current proof state. Issues a command to the assistant based on `proof-showproof-command'. -- Command: proof-ctxt Show the current context. Issues a command to the assistant based on `proof-context-command'. -- Command: proof-help Show a help or information message from the proof assistant. Typically, a list of syntax of commands available. Issues a command to the assistant based on `proof-info-command'. -- Command: proof-find-theorems Search for items containing given constants. Issues a command based on ARG to the assistant, using `proof-find-theorems-command'. The user is prompted for an argument. -- Command: pg-response-clear-displays Clear Proof General response and tracing buffers. You can use this command to clear the output from these buffers when it becomes overly long. Particularly useful when ``proof-tidy-response'' is set to nil, so responses are not cleared automatically. -- Command: proof-interrupt-process Interrupt the proof assistant. Warning! This may confuse Proof General. This sends an interrupt signal to the proof assistant, if Proof General thinks it is busy. This command is risky because when an interrupt is trapped in the proof assistant, we don't know whether the last command succeeded or not. The assumption is that it didn't, which should be true most of the time, and all of the time if the proof assistant has a careful handling of interrupt signals. -- Command: proof-minibuffer-cmd do minibuffer cmd then undo it, if error-free. As if the last two commands weren't risky enough, there's also a command which explicitly adjusts the end of the locked region, to be used in extreme circumstances only. *Note Escaping script management::. There are a few commands for starting, stopping, and restarting the proof assistant process. The first two have key bindings but restart does not. As with any Emacs command, you can invoke these with `M-x' followed by the command name. -- Command: proof-shell-start Initialise a shell-like buffer for a proof assistant. Also generates goal and response buffers. Does nothing if proof assistant is already running. -- Command: proof-shell-exit Query the user and exit the proof process. This simply kills the ``proof-shell-buffer'' relying on the hook function ``proof-shell-kill-function'' to do the hard work. -- Command: proof-shell-restart Clear script buffers and send ``proof-shell-restart-cmd''. All locked regions are cleared and the active scripting buffer deactivated. If the proof shell is busy, an interrupt is sent with ``proof-interrupt-process'' and we wait until the process is ready. The restart command should re-synchronize Proof General with the proof assistant, without actually exiting and restarting the proof assistant process. It is up to the proof assistant how much context is cleared: for example, theories already loaded may be "cached" in some way, so that loading them the next time round only performs a re-linking operation, not full re-processing. (One way of caching is via object files, used by Lego and Coq).  File: ProofGeneral.info, Node: Toolbar commands, Next: Interrupting during trace output, Prev: Proof assistant commands, Up: Basic Script Management 2.8 Toolbar commands ==================== The toolbar provides a selection of functions for asserting and retracting portions of the script, issuing non-scripting commands, and inserting "goal" and "save" type commands. The latter functions are not available on keys, but are available from the from the menu, or via `M-x', as well as the toolbar. -- Command: proof-issue-goal Write a goal command in the script, prompting for the goal. Issues a command based on ARG to the assistant, using `proof-goal-command'. The user is prompted for an argument. -- Command: proof-issue-save Write a save/qed command in the script, prompting for the theorem name. Issues a command based on ARG to the assistant, using `proof-save-command'. The user is prompted for an argument.  File: ProofGeneral.info, Node: Interrupting during trace output, Prev: Toolbar commands, Up: Basic Script Management 2.9 Interrupting during trace output ==================================== If your prover generates output which is recognized as tracing output in Proof General, you may need to know about a special provision for interrupting the prover process. If the trace output is voluminous, perhaps looping, it may be difficult to interrupt with the ordinary `C-c C-c' (`proof-interrupt-process') or the corresponding button/menu. In this case, you should try Emacs's quit key, `C-g'. This will cause a quit in any current editing commands, as usual, but during tracing output it will also send an interrupt signal to the prover. Hopefully this will stop the tracing output, and Emacs should catch up after a short delay. Here's an explanation of the reason for this special provision. When large volumes of output from the prover arrive quickly in Emacs, as typically is the case during tracing (especially tracing looping tactics!), Emacs may hog the CPU and spend all its time updating the display with the trace output. This is especially the case when features like output fontification and X-Symbol display are active. If this happens, ordinary user input in Emacs is not processed, and it becomes difficult to do normal editing. The root of the problem is that Emacs runs in a single thread, and pending process output is dealt with before pending user input. Whether or not you see this problem depends partly on the processing power of your machine (or CPU available to Emacs when the prover is running). One way to test is to start an Emacs shell with `M-x shell' and type a command such as `yes' which produces output indefinitely. Now see if you can interrupt the process! (Warning -- on slower machines especially, this can cause lockups, so use a fresh Emacs.)  File: ProofGeneral.info, Node: Subterm Activation and Proof by Pointing, Next: Advanced Script Management, Prev: Basic Script Management, Up: Top 3 Subterm Activation and Proof by Pointing ****************************************** This chapter describes what you can do from inside the goals buffer, providing support for these features exists for your proof assistant. As of Proof General 3.0, it only exists for LEGO. If you would like to see subterm activation support for Proof General in another proof assistant, please petition the developers of that proof assistant to provide it! * Menu: * Goals buffer commands::  File: ProofGeneral.info, Node: Goals buffer commands, Up: Subterm Activation and Proof by Pointing 3.1 Goals buffer commands ========================= When you are developing a proof, the input focus (Emacs cursor) is usually on the script buffer. Therefore Proof General binds mouse buttons for commands in the goals buffer, to avoid the need to move the cursor between buffers. The mouse bindings are these: `button2' `pg-goals-button-action' `C-button2' `proof-undo-and-delete-last-successful-command' `button3' `pg-goals-yank-subterm' Where `button2' indicates the middle mouse button, and `button3' indicates the right hand mouse button. The idea is that you can automatically construct parts of a proof by clicking. Using the middle mouse button asks the proof assistant to try to do a step in the proof, based on where you click. If you don't like the command which was inserted into the script, you can use the control key with the middle button to undo the step, and delete it from your script. Note that proof-by-pointing may construct several commands in one go. These are sent back to the proof assistant altogether and appear as a single step in the proof script. However, if the proof is later replayed (without using PBP), the proof-by-pointing constructions will be considered as separate proof commands, as usual. -- Command: pg-goals-button-action Construct a proof-by-pointing command based on the mouse-click EVENT. This function should be bound to a mouse button in the Proof General goals buffer. The EVENT is used to find the smallest subterm around a point. A position code for the subterm is sent to the proof assistant, to ask it to construct an appropriate proof command. The command which is constructed will be inserted at the end of the locked region in the proof script buffer, and immediately sent back to the proof assistant. If it succeeds, the locked region will be extended to cover the proof-by-pointing command, just as for any proof command the user types by hand. Proof-by-pointing uses markup describing the term structure of the concrete syntax output by the proof assistant. This markup is useful in itself: it allows you to explore the structure of a term using the mouse (the smallest subexpression that the mouse is over is highlighted), and easily copy subterms from the output to a proof script. The right-hand mouse button provides this convenient way to copy subterms from the goals buffer, using the function `pg-goals-yank-subterm'. -- Command: pg-goals-yank-subterm Copy the subterm indicated by the mouse-click EVENT. This function should be bound to a mouse button in the Proof General goals buffer. The EVENT is used to find the smallest subterm around a point. The subterm is copied to the `kill-ring', and immediately yanked (copied) into the current buffer at the current cursor position. In case the current buffer is the goals buffer itself, the yank is not performed. Then the subterm can be retrieved later by an explicit yank.  File: ProofGeneral.info, Node: Advanced Script Management, Next: Support for other Packages, Prev: Subterm Activation and Proof by Pointing, Up: Top 4 Advanced Script Management **************************** If you are working with large proof developments, you may want to know about the advanced script management features of Proof General covered in this chapter. Large developments may contain files with many long proofs. Proof General provides functions that let you hide completed proofs from view, temporarily. Large proof developments are typically spread across various files which depend on each other in some way. Proof General knows enough about the dependencies to allow script management across multiple files. With large developments particularly, users may occasionally need to escape from script management, in case Proof General loses synchronization with the proof assistant. Proof General provides you with several escape mechanisms if you want to do this. * Menu: * Visibility of completed proofs:: * Switching between proof scripts:: * View of processed files :: * Retracting across files:: * Asserting across files:: * Automatic multiple file handling:: * Escaping script management:: * Experimental features::  File: ProofGeneral.info, Node: Visibility of completed proofs, Next: Switching between proof scripts, Up: Advanced Script Management 4.1 Visibility of completed proofs ================================== Large developments may consist of large files with many proofs. To help see what has been proved without the detail of the proof itself, Proof General can hide portions of the proof script. Two different kinds of thing can be hidden: comments and (what Proof General designates as) the body of proofs. You can toggle the visibility of a proof script portion by using the context sensitive menu triggered by clicking the right mouse button on a completed proof, or the key `C-c v', which runs `pg-toggle-visibility'. You can also select the "disappearing proofs" mode from the menu, Proof-General -> Options -> Disappearing Proofs This automatically hides each the body of each proof portion as it is completed by the proof assistant. Two further menu commands in the main Proof-General menu, _Show all_ and _Hide all_ apply to all the completed portions in the buffer. Notice that by design, this feature only applies to completed proofs, _after_ they have been processed by the proof assistant. When files are first visited in Proof General, no information is stored about proof boundaries. The relevant elisp functions and settings are mentioned below. -- Command: pg-toggle-visibility Toggle visibility of region under point. -- Command: pg-show-all-proofs Display all completed proofs in the buffer. -- Command: pg-hide-all-proofs Hide all completed proofs in the buffer. -- User Option: proof-disappearing-proofs Non-nil causes Proof General to hide proofs as they are completed. The default value is `nil'.  File: ProofGeneral.info, Node: Switching between proof scripts, Next: View of processed files, Prev: Visibility of completed proofs, Up: Advanced Script Management 4.2 Switching between proof scripts =================================== Basic modularity in large proof developments can be achieved by splitting proof scripts across various files. Let's assume that you are in the middle of a proof development. You are working on a soundness proof of Hoare Logic in a file called(1) `HSound.l'. It depends on a number of other files which develop underlying concepts e.g. syntax and semantics of expressions, assertions, imperative programs. You notice that the current lemma is too difficult to prove because you have forgotten to prove some more basic properties about determinism of the programming language. Or perhaps a previous definition is too cumbersome or even wrong. At this stage, you would like to visit the appropriate file, say `sos.l' and retract to where changes are required. Then, using script management, you want to develop some more basic theory in `sos.l'. Once this task has been completed (possibly involving retraction across even earlier files) and the new development has been asserted, you want to switch back to `HSound.l' and replay to the point you got stuck previously. Some hours (or days) later you have completed the soundness proof and are ready to tackle new challenges. Perhaps, you want to prove a property that builds on soundness or you want to prove an orthogonal property such as completeness. Proof General lets you do all of this while maintaining the consistency between proof script buffers and the state of the proof assistant. However, you cannot have more than one buffer where only a fraction of the proof script contains a locked region. Before you can employ script management in another proof script buffer, you must either fully assert or retract the current script buffer. ---------- Footnotes ---------- (1) The suffix may depend of the specific proof assistant you are using e.g, LEGO's proof script files have to end with `.l'.  File: ProofGeneral.info, Node: View of processed files, Next: Retracting across files, Prev: Switching between proof scripts, Up: Advanced Script Management 4.3 View of processed files =========================== Proof General tries to be aware of all files that the proof assistant has processed or is currently processing. In the best case, it relies on the proof assistant explicitly telling it whenever it processes a new file which corresponds(1) to a file containing a proof script. If the current proof script buffer depends on background material from other files, proof assistants typically process these files automatically. If you visit such a file, the whole file is locked as having been processed in a single step. From the user's point of view, you can only retract but not assert in this buffer. Furthermore, retraction is only possible to the _beginning_ of the buffer. Unlike a script buffer that has been processed step-by-step via Proof General, automatically loaded script buffers do not pass through a "red" phase to indicate that they are currently being processed. This is a limitation of the present implementation. Proof General locks a buffer as soon as it sees the appropriate message from the proof assistant. Different proof assistants may use different messages: either _early locking_ when processing a file begins (e.g. LEGO) or _late locking_ when processing a file ends (e.g. Isabelle). With _early locking_, you may find that a script which has only been partly processed (due to an error or interrupt, for example), is wrongly completely locked by Proof General. Visit the file and retract back to the start to fix this. With _late locking_, there is the chance that you can break synchronization by editing a file as it is being read by the proof assistant, and saving it before processing finishes. In fact, there is a general problem of editing files which may be processed by the proof assistant automatically. Synchronization can be broken whenever you have unsaved changes in a proof script buffer and the proof assistant processes the corresponding file. (Of course, this problem is familiar from program development using separate editors and compilers). The good news is that Proof General can detect the problem and flashes up a warning in the response buffer. You can then visit the modified buffer, save it and retract to the beginning. Then you are back on track. ---------- Footnotes ---------- (1) For example, LEGO generates additional compiled (optimised) proof script files for efficiency.  File: ProofGeneral.info, Node: Retracting across files, Next: Asserting across files, Prev: View of processed files, Up: Advanced Script Management 4.4 Retracting across files =========================== Make sure that the current script buffer has either been completely asserted or retracted (Proof General enforces this). Then you can retract proof scripts in a different file. Simply visit a file that has been processed earlier and retract in it, using the retraction commands from *note Script processing commands::. Apart from removing parts of the locked region in this buffer, all files which depend on it will be retracted (and thus unlocked) automatically. Proof General reminds you that now is a good time to save any unmodified buffers.  File: ProofGeneral.info, Node: Asserting across files, Next: Automatic multiple file handling, Prev: Retracting across files, Up: Advanced Script Management 4.5 Asserting across files ========================== Make sure that the current script buffer has either been completely asserted or retracted. Then you can assert proof scripts in a different file. Simply visit a file that contains no locked region and assert some command with the usual assertion commands, *note Script processing commands::. Proof General reminds you that now is a good time to save any unmodified buffers. This is particularly useful as assertion may cause the proof assistant to automatically process other files.  File: ProofGeneral.info, Node: Automatic multiple file handling, Next: Escaping script management, Prev: Asserting across files, Up: Advanced Script Management 4.6 Automatic multiple file handling ==================================== To make it easier to adapt Proof General for a proof assistant, there is another possibility for multiple file support -- that it is provided automatically by Proof General and not integrated with the file-management system of the proof assistant. In this case, Proof General assumes that the only files processed are the ones it has sent to the proof assistant itself. Moreover, it (conservatively) assumes that there is a linear dependency between files in the order they were processed. If you only have automatic multiple file handling, you'll find that any files loaded directly by the proof assistant are _not_ locked when you visit them in Proof General. Moreover, if you retract a file it may retract more than is strictly necessary (because it assumes a linear dependency). For further technical details of the ways multiple file scripting is configured, see Handling multiple files in the Adapting Proof General manual.  File: ProofGeneral.info, Node: Escaping script management, Next: Experimental features, Prev: Automatic multiple file handling, Up: Advanced Script Management 4.7 Escaping script management ============================== Occasionally you may want to review the dialogue of the entire session with the proof assistant, or check that it hasn't done something unexpected. Experienced users may also want to directly communicate with the proof assistant rather than sending commands via the minibuffer, *note Proof assistant commands::. Although the proof shell is usually hidden from view, it is run in a buffer which provides the usual full editing and history facilities of Emacs shells (see the package `comint.el' distributed with your version of Emacs). You can switch to it using the menu: Proof-General -> Buffers -> Shell Warning: you can probably cause confusion by typing in the shell buffer! Proof General may lose track of the state of the proof assistant. Output from the assistant is only fully monitored when Proof General is in control of the shell. When in control, Proof General watches the output from the proof assistant to guess when a file is loaded or when a proof step is taken or undone. What happens when you type in the shell buffer directly depends on how complete the communication is between Proof General and the prover (which depends on the particular instantiation of Proof General). If synchronization is lost, you have two options to resynchronize. If you are lucky, it might suffice to use the key: `C-c C-z' `proof-frob-locked-end' This command is disabled by default, to protect novices using it accidently. If `proof-frob-locked-end' does not work, you will need to restart script management altogether (*note Proof assistant commands::). -- Command: proof-frob-locked-end Move the end of the locked region backwards to regain synchronization. Only for use by consenting adults. This command can be used to repair synchronization in case something goes wrong and you want to tell Proof General that the proof assistant has processed less of your script than Proof General thinks. You should only use it to move the locked region to the end of a proof command.  File: ProofGeneral.info, Node: Experimental features, Prev: Escaping script management, Up: Advanced Script Management 4.8 Experimental features ========================= During the development of Proof General, we experiment with new features in the interface. The particular features available the version of Proof General you have are described in the file `README.exper' which is included in the distribution. The experimental features are automatically enabled in development releases of Proof General, but disabled in the stable releases. To adjust the setting, customize the variable below. After changing the setting you should restart Proof General to see (or remove) the new features. -- User Option: proof-experimental-features Whether to enable certain features regarded as experimental. Proof General includes a few features designated as "experimental". Enabling these will usually have no detrimental effects on using PG, but the features themselves may be buggy. We encourage users to set this flag and test the features, but being aware that the features may be buggy (problem reports and suggestions for improvements are welcomed). The default value is `t'.  File: ProofGeneral.info, Node: Support for other Packages, Next: Customizing Proof General, Prev: Advanced Script Management, Up: Top 5 Support for other Packages **************************** Proof General makes some configuration for other Emacs packages which provide various useful facilities that can make your editing more effective. Sometimes this configuration is purely at the proof assistant specific level (and so not necessarily available), and sometimes it is made using Proof General settings. When adding support for a new proof assistant, we suggest that these other packages are supported, as a convention. The packages currently supported are `font-lock', `x-symbol', `func-menu', `outline-mode', `completion', and `etags'. * Menu: * Syntax highlighting:: * X-Symbol support:: * Imenu and Speedbar (and Function Menu):: * Support for outline mode:: * Support for completion:: * Support for tags::  File: ProofGeneral.info, Node: Syntax highlighting, Next: X-Symbol support, Up: Support for other Packages 5.1 Syntax highlighting ======================= Proof script buffers are decorated (or fontified) with colours, bold and italic fonts, etc, according to the syntax of the proof language and the settings for `font-lock-keywords' made by the proof assistant specific portion of Proof General. Moreover, Proof General usually decorates the output from the proof assistant, also using `font-lock'. In XEmacs, fontification is automatically turned on. To automatically switch on fontification in GNU Emacs 20.4, you may need to engage `M-x global-font-lock-mode'. The old mechanism of adding hooks to the mode hooks (`lego-mode-hooks', `coq-mode-hooks', etc) is no longer recommended; it should not be needed in latest Emacs versions which have more flexible customization. Fontification for output is controlled by a separate switch in Proof General. Set `proof-output-fontify-enable' to `nil' if you don't want the output from your proof assistant to be fontified according to the setting of `font-lock-keywords' in the proof assistant specific portion of Proof General. *Note User options::. By the way, the choice of colour, font, etc, for each kind of markup is fully customizable in Proof General. Each _face_ (Emacs terminology) is controlled by its own customization setting. You can display a list of all of them using the customize menu: Proof General -> Advanced -> Customize -> Faces -> Proof Faces.  File: ProofGeneral.info, Node: X-Symbol support, Next: Imenu and Speedbar (and Function Menu), Prev: Syntax highlighting, Up: Support for other Packages 5.2 X-Symbol support ==================== The X-Symbol package displays characters from a variety of fonts in Emacs buffers, automatically converting between codes for special characters and tokens which are character sequences stored in files. Proof General uses X-Symbol to allow interaction between the user and the proof assistant to use tokens, yet appear to be using special characters. So proof scripts and proofs can be processed with real mathematical symbols, Greek letters, etc. The X-Symbol package is now bundled with Proof General. You will be able to enable X-Symbol support if support has been provided in Proof General for a token language for your proof assistant. To enable X-Symbol, use the menu item: Proof-General -> Options -> X-Symbol To enable it automatically every time you use Proof General, just use Proof-General -> Options -> Save Options once it has been selected. (Alternatively, customize the setting `_PA_-x-symbol-enable'). You may also simply use `M-x x-symbol-mode' to turn on and off X-Symbol display in the scripting buffer, as you would when using X-Symbol for other modes, or indeed, as for any other Emacs minor mode. However, this way of turning on and off symbols will only affect the current script buffer, and will not change the status of any symbol configuration for the prover input/output (some proof assistants, such as Isabelle, have switches for enabling symbol output). To make sure that symbol output is switched on or off for the prover as a whole, use the menu option mentioned above, or its underlying command, `M-x proof-x-symbol-toggle'. Notice that for proper symbol support, the proof assistant needs to have a special token language, or a special character set, to use symbols. In this case, the proof assistant will output, and accept as input, tokens like `\longrightarrow', which display as the corresponding symbols. However, for proof assistants which do not have such token support, we can use "fake" symbol support quite effectively, displaying ordinary ASCII character sequences such as `-->' with symbols. For more information about the X-Symbol package, please visit its home page at `http://x-symbol.sourceforge.net/'.  File: ProofGeneral.info, Node: Imenu and Speedbar (and Function Menu), Next: Support for outline mode, Prev: X-Symbol support, Up: Support for other Packages 5.3 Imenu and Speedbar (and Function Menu) ========================================== The Emacs packages `imenu' (Index Menu) and `func-menu' (Function Menu) each provide a menu built from the names of entities (e.g., theorems, definitions, etc) declared in a buffer. This allows easy navigation within the file. Proof General configures both packages automatically so that you can quickly jump to particular proofs in a script buffer. (Developers note: the automatic configuration is done with the settings `proof-goal-with-hole-regexp' and `proof-save-with-hole-regexp'. Better configuration may be made manually with several other settings, see the Adapting Proof General manual for further details). To use Imenu, select the option Proof General -> Options -> Index Menu This adds an "Index" menu to the main menu bar for proof script buffers. You can also use `M-x imenu' for keyboard-driven completion of tags built from names in the buffer. To use Function Menu (distributed only with XEmacs), use `M-x function-menu'. To enable it by default each time you visit a proof script file (i.e. avoid typing `M-x function-menu'), you should find the file `func-menu.el' and follow the instructions there. 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 or tag. To use Speedbar, use Tools -> Display Speedbar (for GNU Emacs), or Proof General -> Advanced -> Speedbar (for XEmacs). If you prefer the old fashioned way, `M-x speedbar' does the same job. For more information about Speedbar, see `http://cedet.sourceforge.net/speedbar.shtml'.  File: ProofGeneral.info, Node: Support for outline mode, Next: Support for completion, Prev: Imenu and Speedbar (and Function Menu), Up: Support for other Packages 5.4 Support for outline mode ============================ Proof General configures Emacs variables (`outline-regexp' and `outline-heading-end-regexp') so that outline minor mode can be used on proof script files. The headings taken for outlining are the "goal" statements at the start of goal-save sequences, *note Goal-save sequences::. If you want to use `outline' to hide parts of the proof script in the _locked_ region, you need to disable `proof-strict-read-only'. Use `M-x outline-minor-mode' to turn on outline minor mode. Functions for navigating, hiding, and revealing the proof script are available in menus. Please note that outline-mode may not work well in processed proof script files, because of read-only restrictions of the protected region. This is an inherent problem with outline because it works by modifying the buffer. If you want to use outline with processed scripts, you can turn off the `Strict Read Only' option. See *note ((xemacs))Outline Mode:: for more information about outline mode.  File: ProofGeneral.info, Node: Support for completion, Next: Support for tags, Prev: Support for outline mode, Up: Support for other Packages 5.5 Support for completion ========================== You might find the _completion_ facility of Emacs useful when you're using Proof General. The key `C-RET' is defined to invoke the `complete' command. Pressing `C-RET' cycles through completions displaying hints in the minibuffer. Completions are filled in according to what has been recently typed, from a database of symbols. The database is automatically saved at the end of a session. Proof General has the additional facility for setting a completion table for each supported proof assistant, which gets loaded into the completion database automatically. Ideally the completion table would be set from the running process according to the identifiers available are within the particular context of a script file. But until this is available, this table may be set to contain a number of standard identifiers available for your proof assistant. The setting `_PA_-completion-table' holds the list of identifiers for a proof assistant. The function `proof-add-completions' adds these into the completion database. -- Variable: PA-completion-table List of identifiers to use for completion for this proof assistant. Completion is activated with C-return. If this table is empty or needs adjusting, please make changes using ``customize-variable'' and send suggestions to da+pg-support@@inf.ed.ac.uk The completion facility uses a library `completion.el' which usually ships with XEmacs and GNU Emacs, and supplies the `complete' function. -- Command: complete Fill out a completion of the word before point. Point is left at end. Consecutive calls rotate through all possibilities. Prefix args: `C-u' leave point at the beginning of the completion, not the end. `a number' rotate through the possible completions by that amount `0' same as -1 (insert previous completion) See the comments at the top of `completion.el' for more info.  File: ProofGeneral.info, Node: Support for tags, Prev: Support for completion, Up: Support for other Packages 5.6 Support for tags ==================== An Emacs "tags table" is a description of how a multi-file system is broken up into files. It lists the names of the component files and the names and positions of the functions (or other named subunits) in each file. Grouping the related files makes it possible to search or replace through all the files with one command. Recording the function names and positions makes possible the `M-.' command which finds the definition of a function by looking up which of the files it is in. Some instantiations of Proof General (currently LEGO and Coq) are supplied with external programs (`legotags' and `coqtags') for making tags tables. For example, invoking `coqtags *.v' produces a file `TAGS' for all files `*.v' in the current directory. Invoking `coqtags `find . -name \*.v`' produces a file `TAGS' for all files ending in `.v' in the current directory structure. Once a tag table has been made for your proof developments, you can use the Emacs tags mechanisms to find tags, and complete symbols from tags table. One useful key-binding you might want to make is to set the usual tags completion key `M-tab' to run `tag-complete-symbol' to use completion from names in the tag table. To set this binding in Proof General script buffers, put this code in your `.emacs' file: (add-hook 'proof-mode-hook (lambda () (local-set-key '(meta tab) 'tag-complete-symbol))) Since this key-binding interferes with a default binding that users may already have customized (or may be taken by the window manager), Proof General doesn't do this automatically. Apart from completion, there are several other operations on tags. One common one is replacing identifiers across all files using `tags-query-replace'. For more information on how to use tags, *note ((xemacs))Tags::. To use tags for completion at the same time as the completion mechanism mentioned already, you can use the command `M-x add-completions-from-tags-table'. -- Command: add-completions-from-tags-table Add completions from the current tags table.  File: ProofGeneral.info, Node: Customizing Proof General, Next: Hints and Tips, Prev: Support for other Packages, Up: Top 6 Customizing Proof General *************************** There are two ways of customizing Proof General: it can be customized for a user's preferences using a particular proof assistant, or it can be customized by a developer to add support for a new proof assistant. The latter kind of customization we call instantiation, or _adapting_. See the Adapting Proof General manual for how to do this. Here we cover the user-level customization for Proof General. There are two kinds of user-level settings in Proof General: * Settings that apply _globally_ to all proof assistants. * those that can be adjusted for each proof assistant _individually_. The first sort have names beginning with `proof-'. The second sort have names which begin with a symbol corresponding to the proof assistant: for example, `isa-', `coq-', etc. The symbol is the root of the mode name. *Note Quick start guide::, for a table of the supported modes. To stand for an arbitrary proof assistant, we write `_PA_-' for these names. In this chapter we only consider the generic settings: ones which apply to all proof assistants (globally or individually). The support for a particular proof assistant may provide extra individual customization settings not available in other proof assistants. See the chapters covering each assistant for details of those settings. * Menu: * Basic options:: * How to customize:: * Display customization:: * User options:: * Changing faces:: * Tweaking configuration settings::  File: ProofGeneral.info, Node: Basic options, Next: How to customize, Up: Customizing Proof General 6.1 Basic options ================= Proof General has some common options which you can toggle directly from the menu: Proof-General -> Options The effect of changing one of these options will be seen immediately (or in the next proof step). The window-control options on this menu are described shortly. *Note Display customization::. To save the current settings for these options (only), use the Save Options command in the submenu: Proof General -> Options -> Save Options or `M-x customize-save-customized'. The options on this sub-menu are also available in the complete user customization options group for Proof General. For this you need to know a little bit about how to customize in Emacs.  File: ProofGeneral.info, Node: How to customize, Next: Display customization, Prev: Basic options, Up: Customizing Proof General 6.2 How to customize ==================== Proof General uses the Emacs customization library to provide a friendly interface. You can access all the customization settings for Proof General via the menu: Proof-General -> Advanced -> Customize Using the customize facility is straightforward. You can select the setting to customize via the menus, or with `M-x customize-variable'. When you have selected a setting, you are shown a buffer with its current value, and facility to edit it. Once you have edited it, you can use the special buttons SET, SAVE and DONE. You must use one of SET or SAVE to get any effect. The SAVE button stores the setting in your `.emacs' file. The command `M-x customize-save-customized' or XEmacs menubar item `Options -> Save Options' saves all settings you have edited. A technical note. In the customize menus, the variable names mentioned later in this chapter may be abbreviated -- the "`proof'-" or similar prefixes are omitted. Also, some of the option settings may have more descriptive names (for example, ON and OFF) than the low-level lisp values (non-`nil', `nil') which are mentioned in this chapter. These features make customize rather more friendly than raw lisp. You can also access the customize settings for Proof General from other (non-script) buffers. In XEmacs, the menu path is: Options -> Customize -> Emacs -> External -> Proof General in XEmacs. In GNU Emacs, use the menu: Help -> Customize Emacs -> Top-level Customization Group and select the `External' and then `Proof-General' groups. The complete set of customization settings will only be available after Proof General has been fully loaded. Proof General is fully loaded when you visit a script file for the first time, or if you type `M-x load-library RET proof RET'. For more help with customize, see *note (xemacs)Easy Customization::.  File: ProofGeneral.info, Node: Display customization, Next: User options, Prev: How to customize, Up: Customizing Proof General 6.3 Display customization ========================= By default, Proof General displays two buffers during scripting, in a split window on the display. One buffer is the script buffer. The other buffer is either the goals buffer (e.g. `*isabelle-goals*') or the response buffer (`*isabelle-response*'). Proof General switches between these last two automatically. Proof General allows several ways to customize this default display model, by splitting the Emacs frames in different ways and maximising the amount of information shown, or by using multiple frames. The customization options are explained below; they are also available on the menu: Proof-General -> Options -> Display and you can save your preferred default. If your screen is large enough, you may prefer to display all three of the interaction buffers at once. This is useful, for example, to see output from the `proof-find-theorems' command at the same time as the subgoal list. Set the user option `proof-three-window-enable' to make Proof General keep both the goals and response buffer displayed. -- User Option: proof-three-window-enable Whether response and goals buffers have dedicated windows. If non-nil, Emacs windows displaying messages from the prover will not be switchable to display other windows. This option can help manage your display. Setting this option triggers a three-buffer mode of interaction where the goals buffer and response buffer are both displayed, rather than the two-buffer mode where they are switched between. It also prevents Emacs automatically resizing windows between proof steps. If you use several frames (the same Emacs in several windows on the screen), you can force a frame to stick to showing the goals or response buffer. The default value is `nil'. Sometimes during script management, there is no response from the proof assistant to some command. In this case you might like the empty response window to be hidden so you have more room to see the proof script. The setting `proof-delete-empty-windows' helps you do this. -- User Option: proof-delete-empty-windows If non-nil, automatically remove windows when they are cleaned. For example, at the end of a proof the goals buffer window will be cleared; if this flag is set it will automatically be removed. If you want to fix the sizes of your windows you may want to set this variable to `'nil'' to avoid windows being deleted automatically. If you use multiple frames, only the windows in the currently selected frame will be automatically deleted. The default value is `nil'. This option only has an effect when you have set `proof-three-window-mode'. If you are working on a machine with a window system, you can use Emacs to manage several frames on the display, to keep the goals buffer displayed in a fixed place on your screen and in a certain font, for example. A convenient way to do this is via the user option -- User Option: proof-multiple-frames-enable Whether response and goals buffers have separate frames. If non-nil, Emacs will make separate frames (screen windows) for the goals and response buffers, by altering the Emacs variable ``special-display-regexps''. The default value is `nil'. Multiple frames work best when `proof-delete-empty-windows' is off and `proof-three-window-mode' is on. Finally, there are two commands available which help to switch between buffers or refresh the window layout. These are on the menu: Proof-General -> Buffers -- Command: proof-display-some-buffers Display the reponse, trace, goals, or shell buffer, rotating. A fixed number of repetitions of this command switches back to the same buffer. Also move point to the end of the response buffer if it's selected. If in three window or multiple frame mode, display two buffers. The idea of this function is to change the window->buffer mapping without adjusting window layout. -- Command: proof-layout-windows Refresh the display of windows according to current display mode. For single frame mode, this uses a canonical layout made by splitting Emacs windows vertically in equal proportions. You can then adjust the proportions by dragging the separating bars. In three pane mode, the canonical layout is to split both horizontally and vertically, to display the prover responses in two panes on the right-hand side, and the proof script in a taller pane on the left. A prefix argument will prevent the horizontal split, and result in three windows spanning the full width of the Emacs frame. For multiple frame mode, this function obeys the setting of ``proof-eagerly-raise'', which see.  File: ProofGeneral.info, Node: User options, Next: Changing faces, Prev: Display customization, Up: Customizing Proof General 6.4 User options ================ Here is the complete set of user options for Proof General, apart from the three display options mentioned above. User options can be set via the customization system already mentioned, via the old-fashioned `M-x edit-options' mechanism, or simply by adding `setq''s to your `.emacs' file. The first approach is strongly recommended. Unless mentioned, all of these settings can be changed dynamically, without needing to restart Emacs to see the effect. But you must use customize to be sure that Proof General reconfigures itself properly. -- User Option: proof-splash-enable If non-nil, display a splash screen when Proof General is loaded. The default value is `t'. -- User Option: proof-electric-terminator-enable If non-nil, use electric terminator mode. If electric terminator mode is enabled, pressing a terminator will automatically issue ``proof-assert-next-command'' for convenience, to send the command straight to the proof process. If the command you want to send already has a terminator character, you don't need to delete the terminator character first. Just press the terminator somewhere nearby. Electric! The default value is `nil'. -- User Option: proof-toolbar-enable If non-nil, display Proof General toolbar for script buffers. The default value is `t'. -- User Option: PA-x-symbol-enable Whether to use x-symbol in Proof General for this assistant. If you activate this variable, whether or not you really get x-symbol support depends on whether your proof assistant supports it and whether X-Symbol is installed in your Emacs. The default value is `nil'. -- User Option: proof-output-fontify-enable Whether to fontify output from the proof assistant. If non-nil, output from the proof assistant will be highlighted in the goals and response buffers. (This is providing `font-lock-keywords' have been set for the buffer modes). The default value is `t'. -- User Option: proof-strict-read-only Whether Proof General is strict about the read-only region in buffers. If non-nil, an error is given when an attempt is made to edit the read-only region. If nil, Proof General is more relaxed (but may give you a reprimand!). The default value is `strict'. -- User Option: proof-toolbar-use-button-enablers If non-nil, toolbars buttons may be enabled/disabled automatically. Toolbar buttons can be automatically enabled/disabled according to the context. Set this variable to nil if you don't like this feature or if you find it unreliable. Notes: * Toolbar enablers are only available with XEmacs 21 and later. * With this variable nil, buttons do nothing when they would otherwise be disabled. * If you change this variable it will only be noticed when you next start Proof General. * The default value for XEmacs built for solaris is nil, because of unreliabilities with enablers there. The default value is `t'. -- User Option: proof-query-file-save-when-activating-scripting If non-nil, query user to save files when activating scripting. Often, activating scripting or executing the first scripting command of a proof script will cause the proof assistant to load some files needed by the current proof script. If this option is non-nil, the user will be prompted to save some unsaved buffers in case any of them corresponds to a file which may be loaded by the proof assistant. You can turn this option off if the save queries are annoying, but be warned that with some proof assistants this may risk processing files which are out of date with respect to the loaded buffers! The default value is `t'. -- User Option: PA-script-indent If non-nil, enable indentation code for proof scripts. The default value is `t'. -- User Option: proof-one-command-per-line If non-nil, format for newlines after each proof command in a script. This option is not fully-functional at the moment. The default value is `nil'. -- User Option: proof-prog-name-ask If non-nil, query user which program to run for the inferior process. The default value is `nil'. -- User Option: proof-prog-name-guess If non-nil, use ``proof-guess-command-line'' to guess `proof-prog-name'. This option is compatible with `proof-prog-name-ask'. No effect if `proof-guess-command-line' is nil. The default value is `nil'. -- User Option: proof-tidy-response Non-nil indicates that the response buffer should be cleared often. The response buffer can be set either to accumulate output, or to clear frequently. With this variable non-nil, the response buffer is kept tidy by clearing it often, typically between successive commands (just like the goals buffer). Otherwise the response buffer will accumulate output from the prover. The default value is `t'. -- User Option: proof-keep-response-history Whether to keep a browsable history of responses. With this feature enabled, the buffers used for prover responses will have a history that can be browsed without processing/undoing in the prover. (Changes to this variable take effect after restarting the prover). The default value is `nil'. -- User Option: proof-show-debug-messages Whether to display debugging messages in the response buffer. If non-nil, debugging messages are displayed in the response giving information about what Proof General is doing. To avoid erasing the messages shortly after they're printed, you should set ``proof-tidy-response'' to nil. The default value is `nil'. -- User Option: proof-follow-mode Choice of how point moves with script processing commands. One of the symbols: `'locked', `'follow', `'followdown', `'ignore'. If `'locked', point sticks to the end of the locked region. If `'follow', point moves just when needed to display the locked region end. If `'followdown', point if necessary to stay in writeable region If `'ignore', point is never moved after movement commands or on errors. If you choose `'ignore', you can find the end of the locked using `M-x `proof-goto-end-of-locked''. The default value is `locked'. -- User Option: proof-auto-action-when-deactivating-scripting If `'retract' or `'process', do that when deactivating scripting. With this option set to `'retract' or `'process', when scripting is turned off in a partly processed buffer, the buffer will be retracted or processed automatically. With this option unset (nil), the user is questioned instead. Proof General insists that only one script buffer can be partly processed: all others have to be completely processed or completely unprocessed. This is to make sure that handling of multiple files makes sense within the proof assistant. NB: A buffer is completely processed when all non-whitespace is locked (coloured blue); a buffer is completely unprocessed when there is no locked region. The default value is `nil'. -- User Option: proof-script-command-separator String separating commands in proof scripts. For example, if a proof assistant prefers one command per line, then this string should be set to a newline. Otherwise it should be set to a space. The default value is `" "'. -- User Option: proof-rsh-command Shell command prefix to run a command on a remote host. For example, ssh bigjobs Would cause Proof General to issue the command `ssh bigjobs isabelle' to start Isabelle remotely on our large compute server called `bigjobs'. The protocol used should be configured so that no user interaction (passwords, or whatever) is required to get going. For proper behaviour with interrupts, the program should also communicate signals to the remote host. The default value is `nil'.  File: ProofGeneral.info, Node: Changing faces, Next: Tweaking configuration settings, Prev: User options, Up: Customizing Proof General 6.5 Changing faces ================== The fonts and colours that Proof General uses are configurable. If you alter faces through the customize menus (or the command `M-x customize-face'), only the particular kind of display in use (colour window system, monochrome window system, console, ...) will be affected. This means you can keep separate default settings for each different display environment where you use Proof General. As well as the faces listed below, Proof General may use the regular `font-lock-' faces (eg `font-lock-keyword-face', `font-lock-variable-name-face', etc) for fontifying the proof script or proof assistant output. These can be altered to your taste just as easily, but note that changes will affect all other modes which use them! -- Face: proof-queue-face Face for commands in proof script waiting to be processed. -- Face: proof-locked-face Face for locked region of proof script (processed commands). -- Face: proof-error-face Face for error messages from proof assistant. -- Face: proof-warning-face Face for warning messages. Warning messages can come from proof assistant or from Proof General itself. -- Face: proof-debug-message-face Face for debugging messages from Proof General. -- Face: proof-declaration-name-face Face for declaration names in proof scripts. Exactly what uses this face depends on the proof assistant. -- Face: proof-tacticals-name-face Face for names of tacticals in proof scripts. Exactly what uses this face depends on the proof assistant. -- Face: proof-eager-annotation-face Face for important messages from proof assistant. The slightly bizarre name of the last face comes from the idea that while large amounts of output are being sent from the prover, some messages should be displayed to the user while the bulk of the output is hidden. The messages which are displayed may have a special annotation to help Proof General recognize them, and this is an "eager" annotation in the sense that it should be processed as soon as it is observed by Proof General.  File: ProofGeneral.info, Node: Tweaking configuration settings, Prev: Changing faces, Up: Customizing Proof General 6.6 Tweaking configuration settings =================================== This section is a note for advanced users. Configuration settings are the per-prover customizations of Proof General. These are not intended to be adjusted by the user. But occasionally you may like to test changes to these settings to improve the way Proof General works. You may want to do this when a proof assistant has a flexible proof script language in which one can define new tactics or even operations, and you want Proof General to recognize some of these which the default settings don't mention. So please feel free to try adjusting the configuration settings and report to us if you find better default values than the ones we have provided. The configuration settings appear in the customization group `prover-config', or via the menu Proof-General -> Internals -> Prover Config One basic example of a setting you may like to tweak is: -- Variable: proof-assistant-home-page Web address for information on proof assistant. Used for Proof General's help menu. Most of the others are more complicated. For more details of the settings, see Adapting Proof General for full details. To browse the settings, you can look through the customization groups `prover-config', `proof-script' and `proof-shell'. The group `proof-script' contains the configuration variables for scripting, and the group `proof-shell' contains those for interacting with the proof assistant. Unfortunately, although you can use the customization mechanism to set and save these variables, saving them may have no practical effect because the default settings are mostly hard-wired into the proof assistant code. Ones we expect may need changing appear as proof assistant specific configurations. For example, `proof-assistant-home-page' is set in the LEGO code from the value of the customization setting `lego-www-home-page'. At present there is no easy way to save changes to other configuration variables across sessions, other than by editing the source code. (In future versions of Proof General, we plan to make all configuration settings editable in Customize, by shadowing the settings as prover specific ones using the `_PA_-' mechanism).  File: ProofGeneral.info, Node: Hints and Tips, Next: LEGO Proof General, Prev: Customizing Proof General, Up: Top 7 Hints and Tips **************** Apart from the packages officially supported in Proof General, many other features of Emacs are useful when using Proof General, even though they need no specific configuration for Proof General. It is worth taking a bit of time to explore the Emacs manual to find out about them. Here we provide some hints and tips for a couple of Emacs features which users have found valuable with Proof General. Further contributions to this chapter are welcomed! * Menu: * Adding your own keybindings:: * Using file variables:: * Using abbreviations::  File: ProofGeneral.info, Node: Adding your own keybindings, Next: Using file variables, Up: Hints and Tips 7.1 Adding your own keybindings =============================== Proof General follows Emacs convention for file modes in using prefix key-bindings for its own functions, which is why some of the default keyboard short-cuts are quite lengthy. Some users may prefer to add additional key-bindings for shorter sequences. This can be done interactively with the command `M-x local-set-key', or for longevity, by adding code like this to your `.emacs' (or `.xemacs/init.el') file: (eval-after-load "proof-script" '(progn (define-key proof-mode-map [(control n)] 'proof-assert-next-command-interactive) (define-key proof-mode-map [(control b)] 'proof-undo-last-successful-command) )) This lisp fragment adds bindings for every buffer in proof script mode (the Emacs keymap is called `proof-mode-map'). To just affect one prover, use a keymap name like `isar-mode-map' and evaluate after the library `isar' has been loaded. To find the names of the functions you may want to bind, look in this manual, or query current bindings interactively with `C-h k'. This command (`describe-key') works for menu operations as well; also use it to discover the current key-bindings which you're losing by declarations such as those above. By default, `C-n' is `next-line' and `C-b' is `backward-char-command'; neither are really needed if you have working cursor keys. If you're using XEmacs and your keyboard has a super modifier (on my PC keyboard it has a Windows symbol and is next to the control key), you can freely bind keys on that modifier globally (since none are used by default). Use lisp like this: (global-set-key [(super l)] 'x-symbol-INSERT-lambda) (global-set-key [(super n)] 'x-symbol-INSERT-notsign) (global-set-key [(super a)] 'x-symbol-INSERT-logicaland) (global-set-key [(super o)] 'x-symbol-INSERT-logicalor) (global-set-key [(super f)] 'x-symbol-INSERT-universal1) (global-set-key [(super t)] 'x-symbol-INSERT-existential1) (global-set-key [(super A)] 'x-symbol-INSERT-biglogicaland) (global-set-key [(super e)] 'x-symbol-INSERT-equivalence) (global-set-key [(super u)] 'x-symbol-INSERT-notequal) (global-set-key [(super m)] 'x-symbol-INSERT-arrowdblright) (global-set-key [(super i)] 'x-symbol-INSERT-longarrowright) This defines a bunch of short-cuts for insert X-Symbol logical symbols which are often used in Isabelle.  File: ProofGeneral.info, Node: Using file variables, Next: Using abbreviations, Prev: Adding your own keybindings, Up: Hints and Tips 7.2 Using file variables ======================== A very convenient way to customize file-specific variables is to use the File Variables (*note (xemacs)File Variables::). This feature of Emacs allows to specify the values to use for certain Emacs variables when a file is loaded. Those values are written as a list at the end of the file. For example, in projects involving multiple directories, it is often useful to set the variables `proof-prog-name', `proof-prog-args' and `compile-command' for each file. Here is an example for Coq users: for the file `.../dir/bar/foo.v', if you want Coq to be started with the path `.../dir/theories/' added in the libraries path (`"-I"' option), you can put at the end of `foo.v': (* *** Local Variables: *** *** coq-prog-name: "coqtop" *** *** coq-prog-args: ("-emacs" "-I" "../theories") *** *** End: *** *) That way the good command is called when the scripting starts in `foo.v'. Notice that the command argument `"-I" "../theories"' is specific to the file `foo.v', and thus if you set it via the configuration tool, you will need to do it each time you load this file. On the contrary with this method, Emacs will do this operation automatically when loading this file. Please notice that all the strings above should never contain spaces see documentation of variables `proof-prog-name' and `proof-prog-args'. Extending the previous example, if the makefile for `foo.v' is located in directory `.../dir/', you can add the right compile command. And if you want a non standard coq executable to be used, here is what you should put in variables: (* Local Variables: coq-prog-name: "../../coqsrc/bin/coqtop" coq-prog-args: "-emacs" "-I" "../theories" compile-command: "make -C .. -k bar/foo.vo" End: *) And then the right call to make will be done if you use the `M-x compile' command. Notice that the lines are commented in order to be ignored by the proof assistant. It is possible to use this mechanism for any other buffer local variable. *note (xemacs)File Variables::.  File: ProofGeneral.info, Node: Using abbreviations, Prev: Using file variables, Up: Hints and Tips 7.3 Using abbreviations ======================= A very useful package of Emacs supports automatic expansions of abbreviations as you type, *note ((xemacs))Abbrevs::. For example, the proof assistant Coq has many command strings that are long, such as "reflexivity," "Inductive," "Definition" and "Discriminate." Here is a part of the Coq Proof General abbreviations: "abs" "absurd " "ap" "apply " "as" "assumption" The above list was taken from the file that Emacs saves between sessions. The easiest way to configure abbreviations is as you write, by using the key presses `C-x a g' (`add-global-abbrev') or `C-x a i g' (`inverse-add-global-abbrev'). To enable automatic expansion of abbreviations (which can be annoying), the `Abbrev' minor mode, type `M-x abbrev-mode RET'. When you are not in Abbrev mode you can expand an abbreviation by pressing `C-x '' (`expand-abbrev'). See the Emacs manual for more details. Coq Proof General has a special experimental feature called "Holes" which makes use of the abbreviation mechanism and includes a large list of command abbreviations. *Note Holes feature::, for details. With other provers, you may use the standard Emacs commands above to set up your own abbreviation tables.  File: ProofGeneral.info, Node: LEGO Proof General, Next: Coq Proof General, Prev: Hints and Tips, Up: Top 8 LEGO Proof General ******************** LEGO proof script mode is a mode derived from proof script mode for editing LEGO scripts. An important convention is that proof script buffers _must_ start with a module declaration. If the proof script buffer's file name is `fermat.l', then it must commence with a declaration of the form Module fermat; If, in the development of the module `fermat', you require material from other module e.g., `lib_nat' and `galois', you need to specify this dependency as part of the module declaration: Module fermat Import lib_nat galois; No need to worry too much about efficiency. When you retract back to a module declaration to add a new import item, LEGO does not actually retract the previously imported modules. Therefore, reasserting the extended module declaration really only processes the newly imported modules. Using the LEGO Proof General, you never ever need to use administrative LEGO commands such as `Forget', `ForgetMark', `KillRef', `Load', `Make', `Reload' and `Undo' again (1). * Menu: * LEGO specific commands:: * LEGO tags:: * LEGO customizations:: ---------- Footnotes ---------- (1) And please, don't even think of including those in your LEGO proof script!  File: ProofGeneral.info, Node: LEGO specific commands, Next: LEGO tags, Up: LEGO Proof General 8.1 LEGO specific commands ========================== In addition to the commands provided by the generic Proof General (as discussed in the previous sections) the LEGO Proof General provides a few extensions. In proof scripts, there are some abbreviations for common commands: `C-c C-a C-i' intros `C-c C-a C-I' Intros `C-c C-a C-R' Refine  File: ProofGeneral.info, Node: LEGO tags, Next: LEGO customizations, Prev: LEGO specific commands, Up: LEGO Proof General 8.2 LEGO tags ============= You might want to ask your local system administrator to tag the directories `lib_Prop', `lib_Type' and `lib_TYPE' of the LEGO library. See *Note Support for tags::, for further details on tags.  File: ProofGeneral.info, Node: LEGO customizations, Prev: LEGO tags, Up: LEGO Proof General 8.3 LEGO customizations ======================= We refer to chapter *Note Customizing Proof General::, for an introduction to the customisation mechanism. In addition to customizations at the generic level, for LEGO you can also customize: -- User Option: lego-tags The directory of the TAGS table for the LEGO library The default value is `"/usr/lib/lego/lib_Type/"'. -- Variable: lego-www-home-page Lego home page URL.  File: ProofGeneral.info, Node: Coq Proof General, Next: Isabelle Proof General, Prev: LEGO Proof General, Up: Top 9 Coq Proof General ******************* Coq Proof General is an instantiation of Proof General for the Coq proof assistant. It supports most of the generic features of Proof General, but does not have integrated file management or proof-by-pointing yet. * Menu: * Coq-specific commands:: * Coq-specific variables:: * Editing multiple proofs:: * User-loaded tactics:: * Holes feature::  File: ProofGeneral.info, Node: Coq-specific commands, Next: Coq-specific variables, Up: Coq Proof General 9.1 Coq-specific commands ========================= Coq Proof General supplies the following key-bindings: `C-c C-a C-i' Inserts "Intros " `C-c C-a C-a' Inserts "Apply " `C-c C-a C-s' Inserts "Section " `C-c C-a C-e' Inserts "End ." (this should work well with nested sections). `C-c C-a C-o' Prompts for a SearchIsos argument.  File: ProofGeneral.info, Node: Coq-specific variables, Next: Editing multiple proofs, Prev: Coq-specific commands, Up: Coq Proof General 9.2 Coq-specific variables ========================== The variable coq-version-is-Vx (where x is 8-0 or 8-1) is used to force version of Coq, if it is t, then Coq is considered in version x. ProofGeneral sets it automatically by doing the following shell command: (concat coq-prog-name "-v") So you should not have to set this variable unless you have problems with different versions of Coq, you can set to t the variable corresponding to the version you are using in your config file (before ProofGeneral is loaded) and ProofGeneral won't override it.  File: ProofGeneral.info, Node: Editing multiple proofs, Next: User-loaded tactics, Prev: Coq-specific variables, Up: Coq Proof General 9.3 Editing multiple proofs =========================== Coq allows the user to enter top-level commands while editing a proof script. For example, if the user realizes that the current proof will fail without an additional axiom, he or she can add that axiom to the system while in the middle of the proof. Similarly, the user can nest lemmas, beginning a new lemma while in the middle of an earlier one, and as the lemmas are proved or their proofs aborted they are popped off a stack. Coq Proof General supports this feature of Coq. Top-level commands entered while in a proof are well backtracked. If new lemmas are started, Coq Proof General lets the user work on the proof of the new lemma, and when the lemma is finished it falls back to the previous one. This is supported to any nesting depth that Coq allows. Warning! Using coq commands for navigating inside the different proofs (`Resume' and especially `Suspend') are not supported, backtracking will break syncronization. Special note: The old feature that moved nested proofs outside the current proof is disabled.  File: ProofGeneral.info, Node: User-loaded tactics, Next: Holes feature, Prev: Editing multiple proofs, Up: Coq Proof General 9.4 User-loaded tactics ======================= Another feature that Coq allows is the extension of the grammar of the proof assistant by new tactic commands. This feature interacts with the proof script management of Proof General, because Proof General needs to know when a tactic is called that alters the proof state. When the user tries to retract across an extended tactic in a script, the algorithm for calculating how far to undo has a default behavior that is not always accurate in proof mode: do "`Undo'". Coq Proof General does not currently support dynamic tactic extension in Coq: this is desirable but requires assistance from the Coq core. Instead we provide a way to add tactic and command names in the `.emacs' file. Four Configurable variables allows to register personal new tactics and commands into four categories: * _state changing commands_, which need "`Back'" to be backtracked; * _state changing tactics_, which need "`Undo'" to be backtracked; * _state preserving commands_, which do not need to be backtracked; * _state preserving tactics_, which do not need to be backtracked; We give an example of existing commands that fit each category. * `coq-user-state-preserving-commands': example: "`Print'" * `coq-user-state-changing-commands': example: "`Require'" * `coq-user-state-changing-tactics': example: "`Intro'" * `coq-user-state-preserving-tactics': example: "`Idtac'" This variables are regexp string lists. See their documentations in emacs (`C-h v coq-user...') for details on how to set them in your `.emacs' file. Here is a simple example: (setq coq-user-state-changing-commands '("MyHint" "MyRequire")) (setq coq-user-state-preserving-commands '("Show\\s-+Mydata")) The regexp character sequence `\\s-+' means "one or more whitespaces". See the Emacs documentation of `regexp-quote' for the syntax and semantics. WARNING: you need to restart Emacs to make the changes to these variables effective. In case of losing synchronization, the user can use `C-c C-z' to move the locked region to the proper position, (`proof-frob-locked-end', *note Escaping script management::) or `C-c C-v' to re-issue an erroneously back-tracked tactic without recording it in the script.  File: ProofGeneral.info, Node: Holes feature, Prev: User-loaded tactics, Up: Coq Proof General 9.5 Holes feature ================= _Holes_ are an experimental 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 coq command insertion menu system makes use of the holes system. Almost all holes operations are available in the Coq/holes menu. Note: Holes make use of the Emacs abbreviation mechanism, it will work without problem if you don't have an abbrev table defined for Coq in your config files (`C-h v abbrev-file-name' to see the name of the abbreviation file). If you already have such a table it won't be automatically overwritten (so that you keep your own abbreviations). But you must read the abbrev file given in PG/Coq sources to be able to use the command insertion menus. You can do the following to merge your abbreviations with ProofGeneral's abbreviations: `M-x read-abbrev-file', then select 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.  File: ProofGeneral.info, Node: Isabelle Proof General, Next: HOL Proof General, Prev: Coq Proof General, Up: Top 10 Isabelle Proof General ************************* Isabelle Proof General supports all major generic features of Proof General, including integration with Isabelle's theory loader for proper automatic multiple file handling. Only support for tags and proof-by-pointing is missing. It is important to note that there are actually two different versions of Isabelle Proof General: for "classic" Isabelle and for Isabelle/Isar. An old-style Isabelle theory typically consists of `.thy' and correspondent `.ML' files, while Isabelle/Isar theories usually have a new-style `.thy' only, which has a slightly different syntax and may contain both definitions and proofs. While Isabelle is able to manage both classic and Isar theories at the same time (the theory loader determines the source format automatically), Proof General does not admit to work on both kinds of Isabelle source files at the same time! Proof General treats `isa' and `isar' as different instances; there is no way to switch modes once Proof General has been started. The classic version of Isabelle Proof General includes a mode for editing theory files taken from David Aspinall's Isamode interface, see `http://proofgeneral.inf.ed.ac.uk/~isamode'. Detailed documentation for the theory file mode is included with `Isamode', there are some notes on the special functions available and customization settings below. Note that in "classic" Isabelle, `.thy' files contain definitions and declarations for a theory, while `.ML' contain proof scripts. So most of Proof General's functions only make sense in `.ML' files, and there is no toolbar and only a short menu for `.thy' files. In Isabelle/Isar, on the other hand, `.thy' files contain proofs as well as definitions for theories, so scripting takes place there and you see the usual toolbar and scripting functions of Proof General. Most Isabelle users now use Isabelle/Isar because it is more convenient, even if working with tactic-based scripts. For this reason, the default Emacs mode setup of Proof General prefers the `isar' instance over the `isa' instance. To load the "classic" Isabelle mode, you can either make sure to visit a `.ML' before a `.thy' file, or set the environment variable `PROOFGENERAL_ASSISTANTS=isa' before starting Emacs in order to prevent loading of the Isabelle/Isar mode. Another way of forcing classic Isabelle is to put a special modeline like this: (* -*- isa -*- *) near the top of your Isabelle `.thy' files (or at least, the first file you visit). This Emacs feature overrides the default choice of mode based on the file extension. Isabelle provides yet another way to invoke Proof General via the `Isabelle' script. The standard installation of Isabelle also makes the `isar' version of Proof General its default user interface: running plain `Isabelle' starts an Emacs session with Isabelle/Isar Proof General; giving an option `-I false' refers to the classic version instead. The defaults may be changed by editing the Isabelle settings, see the Isabelle documentation for details. * Menu: * Classic Isabelle:: * Isabelle/Isar:: * Logics and Settings::  File: ProofGeneral.info, Node: Classic Isabelle, Next: Isabelle/Isar, Up: Isabelle Proof General 10.1 Classic Isabelle ===================== Proof General for classic Isabelle primarily manages `.ML' files containing proof scripts. There is a separate mode for editing old-style `.thy' files, which supports batch mode only. * Menu: * ML files:: * Theory files:: * General commands for Isabelle:: * Specific commands for Isabelle:: * Isabelle customizations::  File: ProofGeneral.info, Node: ML files, Next: Theory files, Up: Classic Isabelle 10.1.1 ML files --------------- In Isabelle, ML files are used to hold proof scripts, as well as definitions of tactics, proof procedures, etc. So ML files are the normal domain of Proof General. But there are some things to be wary of. Proof General does not understand full ML syntax, so ideally you should only use Proof General's scripting commands on `.ML' files which contain proof commands (no ML functions, structures, etc). If you do use files with Proof General which declare functions, structures, etc, you should be okay provided your code doesn't include non top-level semi-colons (which will confuse Proof General's simplistic parser), and provided all value declarations (and other non proof-steps) occur outside proofs. This is because within proofs, Proof General considers every ML command to be a proof step which is undoable. For example, do this: structure S = struct val x = 3 val y = 4 end; instead of this: structure S = struct val x = 3; val y = 4; end In the second case, just the first binding in the structure body will be sent to Isabelle and Proof General will wait indefinitely. And do this: val intros1 = REPEAT (resolve_tac [impI,allI] 1); Goal "Q(x) --> (ALL x. P(x) --> P(x))"; br impI 1; by intros1; ba 1; qed "mythm"; instead of this: Goal "Q(x) --> (ALL x. P(x) --> P(x))"; br impI 1; val intros1 = REPEAT (resolve_tac [impI,allI] 1); by intros1; ba 1; qed "mythm"; In the last case, when you undo, Proof General wrongly considers the `val' declaration to be a proof step, and it will issue an `undo' to Isabelle to undo it. This leads to a loss of synchronization. To fix things when this happens, simply retract to some point before the `Goal' command and rearrange your script. Having ML as a top-level, Isabelle even lets you redefine the entire proof command language, which will certainly confuse Proof General. Stick to using the standard functions, tactics, and tacticals and there should be no problems. (In fact, there should be no problems provided you don't use your own "goal" or "qed" forms, which Proof General recognizes. As the example above shows, Proof General makes no attempt to recognize arbitrary tactic applications).  File: ProofGeneral.info, Node: Theory files, Next: General commands for Isabelle, Prev: ML files, Up: Classic Isabelle 10.1.2 Theory files ------------------- As well as locking ML files, Isabelle Proof General locks theory files when they are loaded. Theory files are always completely locked or completely unlocked, because they are processed atomically. Proof General tries to load the theory file for a `.ML' file automatically before you start scripting. This relies on support especially for Proof General built into Isabelle's theory loader. However, because scripting cannot begin until the theory is loaded, and it should not begin if an error occurs during loading the theory, Proof General *blocks* waiting for the theory loader to finish. If you have a theory file which takes a long time to load, you might want to load it directly, from the `.thy' buffer. Extra commands are provided in theory mode for this: The key `C-c C-b' (`isa-process-thy-file') will cause Isabelle to read the theory file being edited. This causes the file and all its children (both theory and ML files) to be read. Any top-level ML file associated with this theory file is _not_ read, in contrast with the `use_thy' command of Isabelle. The key `C-c C-u' (`isa-retract-thy-file') will retract (unlock) the theory file being edited. This unlocks the file and all its children (theory and ML files); no changes occur in Isabelle itself. -- Command: isa-process-thy-file Process the theory file FILE. If interactive, use `buffer-file-name'. -- Command: isa-retract-thy-file Retract the theory file FILE. If interactive, use `buffer-file-name'. To prevent inconsistencies, scripting is deactivated before doing this. So if scripting is active in an ML file which is not completely processed, you will be asked to retract the file or process the remainder of it.  File: ProofGeneral.info, Node: General commands for Isabelle, Next: Specific commands for Isabelle, Prev: Theory files, Up: Classic Isabelle 10.1.3 General commands for Isabelle ------------------------------------ This section has some notes on the instantiation of the generic part of Proof General for Isabelle. (The generic part of Proof General applies to all proof assistants supported, and is described in detail in the rest of this manual). *Find theorems*. This toolbar/menu command invokes a special version of `thms_containing'. To give several constants, separate their names with commas.  File: ProofGeneral.info, Node: Specific commands for Isabelle, Next: Isabelle customizations, Prev: General commands for Isabelle, Up: Classic Isabelle 10.1.4 Specific commands for Isabelle ------------------------------------- This section mentions some commands which are added specifically to the Isabelle Proof General instance. In Isabelle proof script mode, `C-c C-o' (`thy-find-other-file') finds and switches to the associated theory file, that is, the file with the same base name but extension `.thy' swapped for `.ML'. The same function (and key-binding) switches back to an ML file from the theory file. -- Command: thy-find-other-file &optional samewindow Find associated .ML or .thy file. Finds and switch to the associated ML file (when editing a theory file) or theory file (when editing an ML file). If SAMEWINDOW is non-nil (interactively, with an optional argument) the other file replaces the one in the current window.  File: ProofGeneral.info, Node: Isabelle customizations, Prev: Specific commands for Isabelle, Up: Classic Isabelle 10.1.5 Isabelle customizations ------------------------------ Here are some of the user options specific to Isabelle. You can set these as usual with the customization mechanism. -- Variable: isabelle-web-page URL of web page for Isabelle. -- User Option: thy-use-sml-mode If non-nil, invoke `sml-mode' inside "ML" section of theory files. This option is left-over from Isamode. Really, it would be more useful if the script editing mode of Proof General itself could be based on `sml-mode', but at the moment there is no way to do this. The default value is `nil'. -- User Option: thy-indent-level Indentation level for Isabelle theory files. An integer. The default value is `2'. -- Variable: thy-sections Names of theory file sections and their templates. Each item in the list is a pair of a section name and a template. A template is either a string to insert or a function. Useful functions are: `thy-insert-header', `thy-insert-class', `thy-insert-default-sort', `thy-insert-const', `thy-insert-rule'. The nil template does nothing. You can add extra sections to theory files by extending this variable. -- Variable: thy-template Template for theory files. Contains a default selection of sections in a traditional order. You can use the following format characters: `%t' -- replaced by theory name. `%p' -- replaced by names of parents, separated by `+' characters.  File: ProofGeneral.info, Node: Isabelle/Isar, Next: Logics and Settings, Prev: Classic Isabelle, Up: Isabelle Proof General 10.2 Isabelle/Isar ================== Proof General for Isabelle/Isar manages Isar `.thy' files, which may contain both definitions and proofs. Proofs may be human readable proof texts as well as traditional tactic scripts adjusted to follow the Isar syntax. The syntax of Isabelle/Isar input is technically simple, enabling Proof General to provide reliable control over incremental execution of the text. Thus it is very hard to let Proof General lose synchronization with the Isabelle/Isar process. The caveats of `.ML' files discussed for the classic Isabelle version (*note Classic Isabelle::) do not apply here. * Menu: * General commands for Isabelle/Isar:: * Specific commands for Isabelle/Isar::  File: ProofGeneral.info, Node: General commands for Isabelle/Isar, Next: Specific commands for Isabelle/Isar, Up: Isabelle/Isar 10.2.1 General commands for Isabelle/Isar ----------------------------------------- *Find theorems*. This toolbar/menu command invokes `thms_containing'. Several term arguments may be given, separated by white space as usual in Isar.  File: ProofGeneral.info, Node: Specific commands for Isabelle/Isar, Prev: General commands for Isabelle/Isar, Up: Isabelle/Isar 10.2.2 Specific commands for Isabelle/Isar ------------------------------------------ The Isabelle/Isar instance of Proof General supplies several specific help key bindings; these functions are offered within the prover help menu as well. `C-c C-a r' Invokes `refute' on the current subgoal. Only available in HOL and derived logics. `C-c C-a C-q' Invokes `quickcheck' on the current subgoal. `C-c C-a C-d' Displays a draft document of the current theory. `C-c C-a h A' Shows available antiquotation commands and options. `C-c C-a h C' Shows the current Classical Reasoner context. `C-c C-a h I' Shows the current set of induct/cases rules. `C-c C-a h S' Shows the current Simplifier context. `C-c C-a h T' Shows the current set of transitivity rules (for calculational reasoning). `C-c C-a h a' Shows attributes available in current theory context. `C-c C-a h b' Shows all local term bindings. `C-c C-a h c' Shows all named local contexts (cases). `C-c C-a h f' Shows all local facts. `C-c C-a h i' Shows inner syntax of the current theory context (for types and terms). `C-c C-a h m' Shows proof methods available in current theory context. `C-c C-a h o' Shows all available commands of Isabelle/Isar's outer syntax. `C-c C-a h t' Shows theorems stored in the current theory node. The following shortcuts insert control sequences into the text, modifying the appearance of individual symbols (single letters, mathematical entities etc.); the X-Symbol package will provide immediate visual feedback. `C-c C-a C-u' Inserts "\<^sup>" (superscript character) `C-c C-a C-l' Inserts "\<^sub>" (subscript character) `C-c C-a u' Inserts "\<^bsup> \<^esup>" (superscript string) `C-c C-a l' Inserts "\<^bsub> \<^esub>" (subscript string) `C-c C-a C-i' Inserts "\<^isub>" (identifier subscript letter) `C-c C-a r' Inserts "\<^raw:>" (raw LaTeX text). Command termination via ``;'' is an optional feature of Isar syntax. Neither Isabelle/Isar nor Proof General require semicolons to do their job. The following command allows to get rid of command terminators in existing texts. -- Command: isar-strip-terminators Remove explicit Isabelle/Isar command terminators `;' from the buffer.  File: ProofGeneral.info, Node: Logics and Settings, Prev: Isabelle/Isar, Up: Isabelle Proof General 10.3 Logics and Settings ======================== The prover specific menu (the same on both Isabelle variants of Proof General) offers a way to select the invoked object logic, and also access to numerous settings of Isabelle. If you look at the menu: Isabelle -> Logics -> you should see the list of logics available to Isabelle. This menu is generated from the output of the command `isatool findlogics', so you should check that Proof General can find the `isatool' program for it to operate correctly. (Similarly, the documentation menu is partly generated from `isatool doc'). The logics menu is refreshed dynamically so you can select any newly built heap images in the same Emacs session. However, notice that the choices are greyed out while Isabelle is actually runnning -- you can only switch to a new logic if you first exit Isabelle (similarly to Proof General, Isabelle operates with only one logic at a time). The prover specific menu also contains a `Settings' submenu, which allows you to configure things such as the behaviour of Isabelle's term pretty printer (display of types, sorts, etc). Note that you won't see this sub-menu until Isabelle has been started, because it is generated by Isabelle itself. Proof General, on the other hand, is responsible for recording any settings that are configured when you select `Isabelle -> Settings -> Save Settings'. They are stored along with the other Emacs customization settings.  File: ProofGeneral.info, Node: HOL Proof General, Next: Shell Proof General, Prev: Isabelle Proof General, Up: Top 11 HOL Proof General ******************** HOL Proof General is a "technology demonstration" of Proof General for HOL4 (aka HOL98). This means that only a basic instantiation has been provided, and that it is not yet supported as a maintained instantiation of Proof General. HOL Proof General has basic script management support, with a little bit of decoration of scripts and output. It does not rely on a modified version of HOL, so the pattern matching may be fragile in certain cases. Support for multiple files deduces dependencies automatically, so there is no interaction with the HOL make system yet. See the `example.sml' file for a demonstration proof script which works with Proof General. Note that HOL proof scripts often use batch-oriented single step tactic proofs, but Proof General does not (yet) offer an easy way to edit these kind of proofs. They will replay simply as a single step proof and you will need to convert from the interactive to batch form as usual if you wish to obtain batch proofs. Also note that Proof General does not contain an SML parser, so there can be problems if you write complex ML in proof scripts. *Note ML files::, for the same issue with Isabelle. HOL Proof General may work with variants of HOL other than HOL98, but is untested. Probably a few of the settings would need to be changed in a simple way, to cope with small differences in output between the systems. (Please let us know if you modify the HOL98 version for another variant of HOL). Perhaps somebody from the HOL community is willing to adopt HOL Proof General and support and improve it. Please volunteer!  File: ProofGeneral.info, Node: Shell Proof General, Next: Obtaining and Installing, Prev: HOL Proof General, Up: Top 12 Shell Proof General ********************** This instance of Proof General is not really for proof assistants at all, but simply provided as a handy way to use a degenerate form of script management with other tools. Suppose you have a software tool of some kind with a command line interface, and you want to demonstrate several example uses of it, perhaps at a conference. But the command lines for your tool may be quite complicated, so you do not want to type them in live. Instead, you just want to cut and paste from a pre-recorded list. But watching somebody cut and paste commands into a window is almost as tedious as watching them type those commands! Shell Proof General comes to the rescue. Simply record your commands in a file with the extension `.pgsh', and load up Proof General. Now use the toolbar to send each line of the file to your tool, and have the output displayed clearly in another window. Much easier and more pleasant for your audience to watch! If you wish, you may adjust the value of `proof-prog-name' in `pgshell.el' to launch your program rather than the shell interpreter. We welcome feedback and suggestions concerning this subsidiary provision in Proof General. Please recommend it to your colleagues (e.g., the model checking crew).  File: ProofGeneral.info, Node: Obtaining and Installing, Next: Known Bugs, Prev: Shell Proof General, Up: Top Appendix A Obtaining and Installing *********************************** Proof General has its own home page (http://proofgeneral.inf.ed.ac.uk) hosted at Edinburgh. Visit this page for the latest news! * Menu: * Obtaining Proof General:: * Installing Proof General from tarball:: * Installing Proof General from RPM package:: * Setting the names of binaries:: * Notes for syssies::  File: ProofGeneral.info, Node: Obtaining Proof General, Next: Installing Proof General from tarball, Up: Obtaining and Installing A.1 Obtaining Proof General =========================== You can obtain Proof General from the URL `http://proofgeneral.inf.ed.ac.uk'. The distribution is available in three forms * A source tarball, `http://proofgeneral.inf.ed.ac.uk/ProofGeneral-devel-latest.tar.gz' * A Linux RPM package (for any architecture), `http://proofgeneral.inf.ed.ac.uk/ProofGeneral-latest.noarch.rpm' * A developer's tarball, `http://proofgeneral.inf.ed.ac.uk/ProofGeneral-devel-latest.tar.gz' Both the source tarball and the RPM package include the generic elisp code, and code for LEGO, Coq, Isabelle, and other provers. Also included are installation instructions (reproduced in brief below) and this documentation. The developer's tarball contains our full source tree, including all of the elisp and documentation, along with our low-level list of things to do, sources for the images, some make files used to generate the release itself from our CVS repository, and some test files. Developers interested in accessing our CVS repository directly should contact `da+pg-support@inf.ed.ac.uk'.  File: ProofGeneral.info, Node: Installing Proof General from tarball, Next: Installing Proof General from RPM package, Prev: Obtaining Proof General, Up: Obtaining and Installing A.2 Installing Proof General from tarball ========================================= Copy the distribution to some directory MYDIR. Unpack it there. For example: # cd MYDIR # gunzip ProofGeneral-VERSION.tar.gz # tar -xpf ProofGeneral-VERSION.tar If you downloaded the version called LATEST, you'll find it unpacks to a numeric version number. Proof General will now be in some subdirectory of MYDIR. The name of the subdirectory will depend on the version number of Proof General. For example, it might be `ProofGeneral-2.0'. It's convenient to link it to a fixed name: # ln -sf ProofGeneral-2.0 ProofGeneral Now put this line in your `.emacs' file: (load-file "MYDIR/ProofGeneral/generic/proof-site.el")  File: ProofGeneral.info, Node: Installing Proof General from RPM package, Next: Setting the names of binaries, Prev: Installing Proof General from tarball, Up: Obtaining and Installing A.3 Installing Proof General from RPM package ============================================= To install an RPM package you need to be root. Then type # rpm -Uvh ProofGeneral-latest.noarch.rpm Now add the line: (load-file "/usr/share/emacs/ProofGeneral/generic/proof-site.el") to your `.emacs' or the site-wide initialisation file `site-start.el'.  File: ProofGeneral.info, Node: Setting the names of binaries, Next: Notes for syssies, Prev: Installing Proof General from RPM package, Up: Obtaining and Installing A.4 Setting the names of binaries ================================= The `load-file' command you have added will load `proof-site' which sets the Emacs load path for Proof General and add auto-loads and modes for the supported assistants. The default names for proof assistant binaries may work on your system. If not, you will need to set the appropriate variables. The easiest way to do this (and most other customization of Proof General) is via the Customize mechanism, see the menu item: Proof-General -> Advanced -> Customize -> NAME OF ASSISTANT -> Prog Name The Proof-General menu is available from script buffers after Proof General is loaded. To load it manually, type M-x load-library RET proof RET If you do not want to use customize, simply add a line like this: (setq coq-prog-name "/usr/bin/coqtop -emacs") to your `.emacs' file.  File: ProofGeneral.info, Node: Notes for syssies, Prev: Setting the names of binaries, Up: Obtaining and Installing A.5 Notes for syssies ===================== Here are some more notes for installing Proof General in more complex ways. Only attempt things in this section if you really understand what you're doing. Byte compilation ---------------- Compilation of the Emacs lisp files improves efficiency but can sometimes cause compatibility problems, especially if you use more than one version of Emacs with the same `.elc' files. Furthermore, we develop Proof General with source files so may miss problems with the byte compiled versions. If you discover problems using the byte-compiled `.elc' files which aren't present using the source `.el' files, please report them to us. You can compile Proof General by typing `make' in the directory where you installed it. Site-wide installation ---------------------- 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 (see Proof General site configuration in Adapting Proof General for more details). Make sure that the `generic/' and assistant-specific elisp files are kept in subdirectories (`coq/', `isa/', `lego/') of `proof-home-directory' so that the autoload directory calculations are correct. To prevent every user needing to edit their own `.emacs' files, you can put the `load-file' command to load `proof-site.el' into `site-start.el' or similar. Consult the Emacs documentation for more details if you don't know where to find this file. Removing support for unwanted provers ------------------------------------- You cannot run more than one instance of Proof General at a time: so if you're using Coq, visiting an `.ML' file will not load Isabelle Proof General, and the buffer remains in fundamental mode. If there are some assistants supported that you never want to use, you can adjust the variable `proof-assistants' in `proof-site.el' to remove the extra autoloads. This is advisable in case the extensions clash with other Emacs modes, for example `sml-mode' for `.ML' files, or Verilog mode for `.v' files. See Proof General site configuration in Adapting Proof General, for more details of how to adjust the `proof-assistants' setting. A simple alternative is to delete the relevant directories from the PG distribution. For example, to remove support for Coq, delete the `coq' directory in the Proof General home directory.  File: ProofGeneral.info, Node: Known Bugs, Next: References, Prev: Obtaining and Installing, Up: Top Appendix B Known Bugs ********************* This appendix has been removed. Please consult the file `BUGS' (http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-latest/BUGS) in the distribution for an up-to-date description of bugs and other issues. If you discover a problem which isn't mentioned in `BUGS', please let us know by sending a note to `da+pg-support@inf.ed.ac.uk'.  File: ProofGeneral.info, Node: References, Next: History of Proof General, Prev: Known Bugs, Up: Top References ********** A short overview of the Proof General system is described in the note: * [Asp00] David Aspinall. Proof General: A Generic Tool for Proof Development. Tools and Algorithms for the Construction and Analysis of Systems, Proc TACAS 2000. LNCS 1785. Script management as used in Proof General is described in the paper: * [BT98] Yves Bertot and Laurent The'ry. A generic approach to building user interfaces for theorem provers. Journal of Symbolic Computation, 25(7), pp. 161-194, February 1998. Proof General has support for proof by pointing, as described in the document: * [BKS97] Yves Bertot, Thomas Kleymann-Schreiber and Dilip Sequeira. Implementing Proof by Pointing without a Structure Editor. LFCS Technical Report ECS-LFCS-97-368. Also published as Rapport de recherche de l'INRIA Sophia Antipolis RR-3286  File: ProofGeneral.info, Node: History of Proof General, Next: Function Index, Prev: References, Up: Top History of Proof General ************************ It all started some time in 1994. There was no Emacs interface for LEGO. Back then, Emacs militants worked directly with the Emacs shell to interact with the LEGO system. David Aspinall convinced Thomas Kleymann that programming in Emacs Lisp wasn't so difficult after all. In fact, Aspinall had already implemented an Emacs interface for Isabelle with bells and whistles, called Isamode (http://homepages.inf.ed.ac.uk/da/Isamode). Soon after, the package `lego-mode' was born. Users were able to develop proof scripts in one buffer. Support was provided to automatically send parts of the script to the proof process. The last official version with the name `lego-mode' (1.9) was released in May 1995. The interface project really took off the ground in November 1996. Yves Bertot had been working on a sophisticated user interface for the Coq system (CtCoq) based on the generic environment Centaur. He visited the Edinburgh LEGO group for a week to transfer proof-by-pointing technology. Even though proof-by-pointing is an inherently structure-conscious algorithm, within a week, Yves Bertot, Dilip Sequeira and Thomas Kleymann managed to implement a first prototype of proof-by-pointing in the Emacs interface for LEGO [BKS97]. Perhaps we could reuse even more of the CtCoq system. It being a structure editor did no longer seem to be such an obstacle. Moreover, to conveniently use proof-by-pointing in actual developments, one would need better support for script management. In 1997, Dilip Sequeira implemented script management in our Emacs interface for LEGO following the recipe in [BT98]. Inspired by the project CROAP, the implementation made some effort to be generic. A working prototype was demonstrated at UITP'97. In October 1997, Healfdene Goguen ported `lego-mode' to Coq. Part of the generic code in the `lego' package was outsourced (and made more generic) in a new package called `proof'. Dilip Sequeira provided some LEGO-specific support for handling multiple files and wrote a few manual pages. The system was reasonably robust and we shipped out the package to friends. In June 1998, David Aspinall reentered the picture by providing an instantiation for Isabelle. Actually, our previous version wasn't quite as generic as we had hoped. Whereas LEGO and Coq are similar systems in many ways, Isabelle was really a different beast. Fierce re-engineering and various usability improvements were provided by Aspinall and Kleymann to make it easier to instantiate to new proof systems. The major technical improvement was a truly generic extension of script management to work across multiple files. It was time to come up with a better name than just `proof' mode. David Aspinall suggested _Proof General_ and set about reorganizing the file structure to disentangle the Proof General project from LEGO at last. He cooked up some images and bolted on a toolbar, so a naive user can replay proofs without knowing a proof assistant language or even Emacs hot-keys. He also designed some web pages, and wrote most of this manual. Despite views of some detractors, we demonstrated that an interface both friendly and powerful can be built on top of Emacs. Proof General 2.0 was the first official release of the improved program, made in December 1998. Version 2.1 was released in August 1999. It was used at the Types Summer School held in Giens, France in September 1999 (see `http://www-sop.inria.fr/types-project/types-sum-school.html'). About 50 students learning Coq, Isabelle, and LEGO used Proof General for all three systems. This experience provided invaluable feedback and encouragement to make the improvements that went into Proof General 3.0. * Menu: * Old News for 3.0:: * Old News for 3.1:: * Old News for 3.2:: * Old News for 3.3:: * Old News for 3.4::  File: ProofGeneral.info, Node: Old News for 3.0, Next: Old News for 3.1, Up: History of Proof General Old News for 3.0 ================ Proof General 3.0 (released November 1999) has many improvements over 2.x releases. First, there are usability improvements. The toolbar was somewhat impoverished before. It now has twice as many buttons, and includes all of the useful functions used during proof which were previously hidden on the menu, or even only available as key-presses. Key-bindings have been re-organized, users of previous versions may notice. The menu has been redesigned and coordinated with the toolbar, and now gives easy access to more of the features of Proof General. Previously several features were only likely to be discovered by those keen enough to read this manual! Second, there are improvements, extensions, and bug fixes in the generic basis. Proofs which are unfinished and not explicitly closed by a "save" type command are supported by the core, if they are allowed by the prover. The design of switching the active scripting buffer has been streamlined. The management of the queue of commands waiting to be sent to the shell has been improved, so there are fewer unnecessary "Proof Process Busy!" messages. The support for scripting with multiple files was improved so that it behaves reliably with Isabelle99; file reading messages can be communicated in both directions now. The proof shell filter has been optimized to give hungry proof assistants a better share of CPU cycles. Proof-by-pointing has been resurrected; even though LEGO's implementation is incomplete, it seems worth maintaining the code in Proof General so that the implementors of other proof assistants are encouraged to provide support. For one example, we can certainly hope for support in Coq, since the CtCoq proof-by-pointing code has been moved into the Coq kernel lately. We need a volunteer from the Coq community to help to do this. An important new feature in Proof General 3.0 is support for X-Symbol (http://x-symbol.sourceforge.net/), which means that real logical symbols, Greek letters, etc can be displayed during proof development, instead of their ASCII approximations. This makes Proof General a more serious competitor to native graphical user interfaces. Finally, Proof General has become much easier to adapt to new provers -- it fails gracefully (or not at all!) when particular configuration variables are unset, and provides more default settings which work out-of-the-box. An example configuration for Isabelle is provided, which uses just 25 or so simple settings. This manual has been updated and extended for Proof General 3.0. Amongst other improvements, it has a better description of how to add support for a new prover. See the `CHANGES' file in the distribution for more information about the latest improvements in Proof General. Developers should check the `ChangeLog' in the developer's release for detailed comments on internal changes. Most of the work for Proof General 3.0 has been done by David Aspinall. Markus Wenzel helped with Isabelle support, and provided invaluable feedback and testing, especially for the improvements to multiple file handling. Pierre Courtieu took responsibility from Patrick Loiseleur for Coq support, although improvements in both Coq and LEGO instances for this release were made by David Aspinall. Markus Wenzel provided support for his Isar language, a new proof language for Isabelle. David von Oheimb helped to develop the generic version of his X-Symbol addition which he originally provided for Isabelle. A new instantiation of Proof General is being worked on for _Plastic_, a proof assistant being developed at the University of Durham.  File: ProofGeneral.info, Node: Old News for 3.1, Next: Old News for 3.2, Prev: Old News for 3.0, Up: History of Proof General Old News for 3.1 ================ Proof General 3.1 (released March 2000) is a bug-fix improvement over version 3.0. There are some minor cosmetic improvements, but large changes have been held back to ensure stability. This release solves a few minor problems which came to light since the final testing stages for 3.0. It also solves some compatibility problems, so now it works with various versions of Emacs which we hadn't tested with before (non-mule GNU Emacs, certain Japanese Emacs versions). We're also pleased to announce HOL Proof General, a new instance of Proof General for HOL98. This is supplied as a "technology demonstration" for HOL users in the hope that somebody from the HOL community will volunteer to adopt it and become a maintainer and developer. (Otherwise, work on HOL Proof General will not continue). Apart from that there are a few other small improvements. Check the CHANGES file in the distribution for full details. The HOL98 support and much of the work on Proof General 3.1 was undertaken by David Aspinall while he was visiting ETL, Osaka, Japan, supported by the British Council and ETL.  File: ProofGeneral.info, Node: Old News for 3.2, Next: Old News for 3.3, Prev: Old News for 3.1, Up: History of Proof General Old News for 3.2 ================ Proof General 3.2 introduced several new features and some bug fixes. One noticeable new feature is the addition of a prover-specific menu for each of the supported provers. This menu has a "favourites" feature that you can use to easily define new functions. Please contribute other useful functions (or suggestions) for things you would like to appear on these menus. Because of the new menus and to make room for more commands, we have made a new key map for prover specific functions. These now all begin with `C-c C-a'. This has changed a few key bindings slightly. Another new feature is the addition of prover-specific completion tables, to encourage the use of Emacs's completion facility, using `C-RET'. *Note Support for completion::, for full details. A less obvious new feature is support for turning the proof assistant output on and off internally, to improve efficiency when processing large scripts. This means that more of your CPU cycles can be spent on proving theorems. Adapting for new proof assistants continues to be made more flexible, and easier in several places. This has been motivated by adding experimental support for some new systems. One new system which had good support added in a very short space of time is PhoX (see the PhoX home page (http://www.lama.univ-savoie.fr/~RAFFALLI/af2.html) for more information). PhoX joins the rank of officially supported Proof General instances, thanks to its developer Christophe Raffalli. Breaking the manual into two pieces was overdue: now all details on adapting Proof General, and notes on its internals, are in the Adapting Proof General manual. You should find a copy of that second manual close to wherever you found this one; consult the Proof General home page if in doubt. The internal code of Proof General has been significantly overhauled for this version, which should make it more robust and readable. The generic code has an improved file structure, and there is support for automatic generation of autoload functions. There is also a new mechanism for defining prover-specific customization and instantiation settings which fits better with the customize library. These settings are named in the form `PA-setting-name' in the documentation; you replace PA by the symbol for the proof assistant you are interested in. *Note Customizing Proof General::, for details. Finally, important bug fixes include the robustification against `write-file' (`C-x C-w'), `revert-buffer', and friends. These are rather devious functions to use during script management, but Proof General now tries to do the right thing if you're deviant enough to try them out! Work on this release was undertaken by David Aspinall between May-September 2000, and includes contributions from Markus Wenzel, Pierre Courtieu, and Christophe Raffalli. Markus added some Isar documentation to this manual.  File: ProofGeneral.info, Node: Old News for 3.3, Next: Old News for 3.4, Prev: Old News for 3.2, Up: History of Proof General Old News for 3.3 ================ Proof General 3.3 includes a few feature additions, but mainly the focus has been on compatibility improvements for new versions of provers (in particular, Coq 7), and new versions of emacs (in particular, XEmacs 21.4). One new feature is control over visibility of completed proofs, *Note Visibility of completed proofs::. Another new feature is the tracking of theorem dependencies inside Isabelle. A context-sensitive menu (right-button on proof scripts) provides facility for browsing the ancestors and child theorems of a theorem, and highlighting them. The idea of this feature is that it can help you untangle and rearrange big proof scripts, by seeing which parts are interdependent. The implementation is provisional and not documented yet in the body of this manual. It only works for the "classic" version of Isabelle99-2.  File: ProofGeneral.info, Node: Old News for 3.4, Prev: Old News for 3.3, Up: History of Proof General Old News for 3.4 ================ Proof General 3.4 adds improvements and also compatibility fixes for new versions of Emacs, in particular, for GNU Emacs 21, which adds the remaining pretty features that have only been available to XEmacs users until now (the toolbar and X-Symbol support). One major improvement has been to provide better support for synchronization with Coq proof scripts; now Coq Proof General should be able to retract and replay most Coq proof scripts reliably. Credit is due to Pierre Courtieu, who also updated the documentation in this manual. As of version 3.4, Proof General is distributed under the GNU General Public License (GPL). Compared with the previous more restrictive license, this means the program can now be redistributed by third parties, and used in any context without applying for a special license. Despite these legal changes, we would still appreciate if you send us back any useful improvements you make to Proof General, and register your use of Proof General on the web site.  File: ProofGeneral.info, Node: Function Index, Next: Variable Index, Prev: History of Proof General, Up: Top Function and Command Index ************************** [index] * Menu: * add-completions-from-tags-table: Support for tags. (line 43) * complete: Support for completion. (line 39) * indent-for-tab-command: Script editing commands. (line 10) * isa-process-thy-file: Theory files. (line 32) * isa-retract-thy-file: Theory files. (line 36) * isar-strip-terminators: Specific commands for Isabelle/Isar. (line 90) * pg-goals-button-action: Goals buffer commands. (line 39) * pg-goals-yank-subterm: Goals buffer commands. (line 64) * pg-hide-all-proofs: Visibility of completed proofs. (line 38) * pg-response-clear-displays: Proof assistant commands. (line 69) * pg-show-all-proofs: Visibility of completed proofs. (line 35) * pg-toggle-visibility: Visibility of completed proofs. (line 32) * proof-assert-next-command-interactive: Script processing commands. (line 52) * proof-assert-until-point-interactive: Script processing commands. (line 87) * proof-ctxt: Proof assistant commands. (line 54) * proof-debug-message-face: Changing faces. (line 35) * proof-declaration-name-face: Changing faces. (line 38) * proof-display-some-buffers <1>: Display customization. (line 83) * proof-display-some-buffers: Proof assistant commands. (line 41) * proof-eager-annotation-face: Changing faces. (line 46) * proof-electric-terminator-toggle: Script processing commands. (line 81) * proof-error-face: Changing faces. (line 27) * proof-find-theorems: Proof assistant commands. (line 63) * proof-frob-locked-end: Escaping script management. (line 42) * proof-goto-command-end: Script editing commands. (line 32) * proof-goto-command-start: Script editing commands. (line 29) * proof-goto-end-of-locked: Script editing commands. (line 39) * proof-goto-point: Script processing commands. (line 69) * proof-help: Proof assistant commands. (line 58) * proof-interrupt-process: Proof assistant commands. (line 76) * proof-issue-goal: Toolbar commands. (line 13) * proof-issue-save: Toolbar commands. (line 18) * proof-layout-windows: Display customization. (line 91) * proof-locked-face: Changing faces. (line 24) * proof-minibuffer-cmd: Proof assistant commands. (line 88) * proof-mouse-track-insert: Script editing commands. (line 56) * proof-prf: Proof assistant commands. (line 49) * proof-process-buffer: Script processing commands. (line 74) * proof-queue-face: Changing faces. (line 21) * proof-retract-buffer: Script processing commands. (line 78) * proof-retract-until-point-interactive: Script processing commands. (line 93) * proof-shell-exit: Proof assistant commands. (line 106) * proof-shell-restart: Proof assistant commands. (line 112) * proof-shell-start: Proof assistant commands. (line 100) * proof-tacticals-name-face: Changing faces. (line 42) * proof-toggle-active-scripting: Active scripting buffer. (line 57) * proof-undo-and-delete-last-successful-command: Script processing commands. (line 59) * proof-undo-last-successful-command: Script processing commands. (line 56) * proof-warning-face: Changing faces. (line 30) * thy-find-other-file: Specific commands for Isabelle. (line 17)  File: ProofGeneral.info, Node: Variable Index, Next: Keystroke Index, Prev: Function Index, Up: Top Variable and User Option Index ****************************** [index] * Menu: * coq-mode-hooks: Syntax highlighting. (line 6) * isa-mode-hooks: Syntax highlighting. (line 6) * isabelle-web-page: Isabelle customizations. (line 10) * lego-mode-hooks: Syntax highlighting. (line 6) * lego-tags: LEGO customizations. (line 11) * lego-www-home-page: LEGO customizations. (line 16) * PA-completion-table: Support for completion. (line 28) * PA-script-indent: User options. (line 96) * PA-x-symbol-enable: User options. (line 40) * proof-assistant-home-page: Tweaking configuration settings. (line 25) * proof-auto-action-when-deactivating-scripting: User options. (line 169) * proof-delete-empty-windows: Display customization. (line 51) * proof-disappearing-proofs: Visibility of completed proofs. (line 41) * proof-electric-terminator-enable: User options. (line 24) * proof-experimental-features: Experimental features. (line 18) * proof-follow-mode: User options. (line 154) * proof-goal-with-hole-regexp: Imenu and Speedbar (and Function Menu). (line 6) * proof-goal-with-hole-result: Imenu and Speedbar (and Function Menu). (line 6) * proof-keep-response-history: User options. (line 136) * proof-multiple-frames-enable: Display customization. (line 69) * proof-one-command-per-line: User options. (line 101) * proof-output-fontify-enable: User options. (line 48) * proof-prog-name-ask: User options. (line 108) * proof-prog-name-guess: User options. (line 114) * proof-query-file-save-when-activating-scripting: User options. (line 80) * proof-rsh-command: User options. (line 197) * proof-script-command-separator: User options. (line 189) * proof-script-indent: Script editing commands. (line 10) * proof-show-debug-messages: User options. (line 145) * proof-splash-enable: User options. (line 19) * proof-strict-read-only: User options. (line 56) * proof-terminal-char: Script editing commands. (line 34) * proof-three-window-enable: Display customization. (line 27) * proof-tidy-response: User options. (line 122) * proof-toolbar-enable: User options. (line 35) * proof-toolbar-use-button-enablers: User options. (line 65) * thy-indent-level: Isabelle customizations. (line 21) * thy-sections: Isabelle customizations. (line 26) * thy-template: Isabelle customizations. (line 37) * thy-use-sml-mode: Isabelle customizations. (line 13)  File: ProofGeneral.info, Node: Keystroke Index, Next: Concept Index, Prev: Variable Index, Up: Top Keystroke Index *************** [index] * Menu: * C-button1: Script editing commands. (line 52) * C-c C-.: Script editing commands. (line 18) * C-c C-a: Script editing commands. (line 18) * C-c C-a C-a: Coq-specific commands. (line 6) * C-c C-a C-d: Specific commands for Isabelle/Isar. (line 6) * C-c C-a C-e: Coq-specific commands. (line 6) * C-c C-a C-i: Coq-specific commands. (line 6) * C-c C-a C-I: LEGO specific commands. (line 11) * C-c C-a C-i: LEGO specific commands. (line 11) * C-c C-a C-l: Specific commands for Isabelle/Isar. (line 61) * C-c C-a C-o: Coq-specific commands. (line 6) * C-c C-a C-q: Specific commands for Isabelle/Isar. (line 6) * C-c C-a C-R: LEGO specific commands. (line 11) * C-c C-a C-s: Coq-specific commands. (line 6) * C-c C-a C-u: Specific commands for Isabelle/Isar. (line 61) * C-c C-a C-w: Specific commands for Isabelle/Isar. (line 61) * C-c C-a h a: Specific commands for Isabelle/Isar. (line 6) * C-c C-a h A: Specific commands for Isabelle/Isar. (line 6) * C-c C-a h b: Specific commands for Isabelle/Isar. (line 6) * C-c C-a h c: Specific commands for Isabelle/Isar. (line 6) * C-c C-a h C: Specific commands for Isabelle/Isar. (line 6) * C-c C-a h f: Specific commands for Isabelle/Isar. (line 6) * C-c C-a h i: Specific commands for Isabelle/Isar. (line 6) * C-c C-a h I: Specific commands for Isabelle/Isar. (line 6) * C-c C-a h m: Specific commands for Isabelle/Isar. (line 6) * C-c C-a h o: Specific commands for Isabelle/Isar. (line 6) * C-c C-a h S: Specific commands for Isabelle/Isar. (line 6) * C-c C-a h t: Specific commands for Isabelle/Isar. (line 6) * C-c C-a h T: Specific commands for Isabelle/Isar. (line 6) * C-c C-a i: Specific commands for Isabelle/Isar. (line 61) * C-c C-a l: Specific commands for Isabelle/Isar. (line 61) * C-c C-a r: Specific commands for Isabelle/Isar. (line 6) * C-c C-a u: Specific commands for Isabelle/Isar. (line 61) * C-c C-b: Script processing commands. (line 6) * C-c C-BS: Script processing commands. (line 6) * C-c C-c: Proof assistant commands. (line 6) * C-c C-e: Script editing commands. (line 18) * C-c C-f: Proof assistant commands. (line 6) * C-c C-h: Proof assistant commands. (line 6) * C-c C-n: Script processing commands. (line 6) * C-c C-o: Specific commands for Isabelle. (line 9) * C-c C-p: Proof assistant commands. (line 6) * C-c C-r: Script processing commands. (line 6) * C-c C-RET: Script processing commands. (line 6) * C-c C-t: Proof assistant commands. (line 6) * C-c C-u: Script processing commands. (line 6) * C-c C-v: Proof assistant commands. (line 6) * coq-version-is-V8-0: Coq-specific variables. (line 6) * coq-version-is-V8-1: Coq-specific variables. (line 6)  File: ProofGeneral.info, Node: Concept Index, Prev: Keystroke Index, Up: Top Concept Index ************* [index] * Menu: * active scripting buffer: Active scripting buffer. (line 6) * Alt: Prerequisites for this manual. (line 6) * Assertion <1>: Asserting across files. (line 6) * Assertion: Locked queue and editing regions. (line 28) * blue text: Locked queue and editing regions. (line 6) * buffer display customization: Display customization. (line 6) * Centaur: History of Proof General. (line 19) * Classic Isabelle: Classic Isabelle. (line 6) * colour: Syntax highlighting. (line 6) * completion: Support for completion. (line 6) * CtCoq: History of Proof General. (line 19) * Customization: Customizing Proof General. (line 6) * Dedicated windows: User options. (line 6) * display customization: Display customization. (line 6) * Editing region: Locked queue and editing regions. (line 6) * Emacs customization library: How to customize. (line 6) * Features: Features of Proof General. (line 6) * file variables: Using file variables. (line 6) * font lock: Syntax highlighting. (line 6) * frames: Display customization. (line 6) * fume-func: Imenu and Speedbar (and Function Menu). (line 6) * func-menu: Imenu and Speedbar (and Function Menu). (line 6) * function menu: Imenu and Speedbar (and Function Menu). (line 6) * Future: Future. (line 6) * generic: History of Proof General. (line 33) * goal: Goal-save sequences. (line 6) * goal-save sequences: Goal-save sequences. (line 6) * goals buffer: Summary of Proof General buffers. (line 6) * Greek letters: X-Symbol support. (line 6) * history: History of Proof General. (line 6) * HOL Proof General: HOL Proof General. (line 6) * Imenu: Imenu and Speedbar (and Function Menu). (line 6) * Indentation: User options. (line 6) * index menu: Imenu and Speedbar (and Function Menu). (line 6) * Isabelle logic: Logics and Settings. (line 6) * Isabelle Proof General: Isabelle Proof General. (line 6) * Isabelle proof scripts: ML files. (line 6) * Isabelle/Isar: Isabelle/Isar. (line 6) * key sequences: Prerequisites for this manual. (line 6) * keybindings: Adding your own keybindings. (line 6) * LEGO Proof General: LEGO Proof General. (line 6) * lego-mode <1>: History of Proof General. (line 6) * lego-mode: Credits. (line 6) * Locked region: Locked queue and editing regions. (line 6) * logical symbols: X-Symbol support. (line 6) * maintenance: Credits. (line 6) * mathematical symbols: X-Symbol support. (line 6) * Meta: Prerequisites for this manual. (line 6) * ML files (in Isabelle) <1>: Theory files. (line 6) * ML files (in Isabelle): ML files. (line 6) * Multiple Files: Advanced Script Management. (line 6) * multiple frames: Display customization. (line 6) * multiple windows: Display customization. (line 6) * news <1>: Old News for 3.2. (line 6) * news <2>: Old News for 3.1. (line 6) * news: Latest news for 3.5 and 3.6. (line 6) * outline mode: Support for outline mode. (line 6) * pink text: Locked queue and editing regions. (line 6) * prefix argument: Script processing commands. (line 6) * proof assistant: Introducing Proof General. (line 6) * proof by pointing <1>: History of Proof General. (line 19) * proof by pointing: Summary of Proof General buffers. (line 6) * Proof General: Introducing Proof General. (line 6) * Proof General Kit: Future. (line 6) * proof script: Proof scripts. (line 6) * Proof script indentation: User options. (line 6) * proof script mode: Script buffers. (line 6) * Query program name: User options. (line 6) * Queue region: Locked queue and editing regions. (line 6) * real symbols: X-Symbol support. (line 6) * Remote host: User options. (line 6) * Remote shell: User options. (line 6) * response buffer: Summary of Proof General buffers. (line 6) * Retraction <1>: Retracting across files. (line 6) * Retraction: Locked queue and editing regions. (line 38) * Running proof assistant remotely: User options. (line 6) * save: Goal-save sequences. (line 6) * script buffer: Script buffers. (line 6) * script management: History of Proof General. (line 28) * scripting: Proof scripts. (line 6) * Shell: Escaping script management. (line 6) * shell buffer: Summary of Proof General buffers. (line 6) * Shell Proof General: Shell Proof General. (line 6) * Speedbar: Imenu and Speedbar (and Function Menu). (line 6) * Strict read-only: User options. (line 6) * structure editor: History of Proof General. (line 28) * Switching between proof scripts: Switching between proof scripts. (line 6) * Switching to theory files: Specific commands for Isabelle. (line 9) * tags: Support for tags. (line 6) * Theory files (in Isabelle): Theory files. (line 6) * three-buffer interaction: Display customization. (line 6) * Toolbar button enablers: User options. (line 6) * Toolbar disabling: User options. (line 6) * Toolbar follow mode: User options. (line 6) * User options: User options. (line 6) * Using Customize: How to customize. (line 6) * Visibility of proofs: Visibility of completed proofs. (line 6) * Why use Proof General?: Features of Proof General. (line 6) * X-Symbols: X-Symbol support. (line 6)  Tag Table: Node: Top201 Node: Preface1137 Node: Latest news for 3.5 and 3.61781 Node: Future3194 Node: Credits4772 Node: Introducing Proof General7965 Ref: Introducing Proof General-Footnote-19483 Ref: Introducing Proof General-Footnote-29714 Node: Quick start guide9815 Node: Features of Proof General12303 Node: Supported proof assistants16118 Node: Prerequisites for this manual18097 Node: Organization of this manual19731 Node: Basic Script Management20555 Node: Walkthrough example in Isabelle/Isar21225 Node: Proof scripts29398 Node: Script buffers31457 Node: Locked queue and editing regions32069 Node: Goal-save sequences34142 Node: Active scripting buffer35338 Ref: Active scripting buffer-Footnote-138452 Node: Summary of Proof General buffers38701 Node: Script editing commands40950 Node: Script processing commands43429 Ref: Script processing commands-Footnote-147758 Node: Proof assistant commands48122 Node: Toolbar commands52641 Node: Interrupting during trace output53607 Node: Subterm Activation and Proof by Pointing55508 Node: Goals buffer commands56143 Node: Advanced Script Management59287 Node: Visibility of completed proofs60538 Node: Switching between proof scripts62311 Ref: Switching between proof scripts-Footnote-164286 Node: View of processed files64413 Ref: View of processed files-Footnote-166884 Node: Retracting across files66984 Node: Asserting across files67744 Node: Automatic multiple file handling68448 Node: Escaping script management69626 Node: Experimental features71904 Node: Support for other Packages73136 Node: Syntax highlighting74064 Node: X-Symbol support75598 Node: Imenu and Speedbar (and Function Menu)77980 Node: Support for outline mode79968 Node: Support for completion81165 Node: Support for tags83311 Node: Customizing Proof General85507 Node: Basic options87140 Node: How to customize87970 Node: Display customization90003 Node: User options94979 Node: Changing faces103313 Node: Tweaking configuration settings105566 Node: Hints and Tips107933 Node: Adding your own keybindings108636 Node: Using file variables111239 Node: Using abbreviations113481 Node: LEGO Proof General114835 Ref: LEGO Proof General-Footnote-1116105 Node: LEGO specific commands116185 Node: LEGO tags116647 Node: LEGO customizations117001 Node: Coq Proof General117542 Node: Coq-specific commands118053 Node: Coq-specific variables118543 Node: Editing multiple proofs119258 Node: User-loaded tactics120487 Node: Holes feature122904 Node: Isabelle Proof General124144 Node: Classic Isabelle127411 Node: ML files127882 Node: Theory files130344 Node: General commands for Isabelle132258 Node: Specific commands for Isabelle132872 Node: Isabelle customizations133851 Node: Isabelle/Isar135489 Node: General commands for Isabelle/Isar136333 Node: Specific commands for Isabelle/Isar136704 Node: Logics and Settings139185 Node: HOL Proof General140761 Node: Shell Proof General142517 Node: Obtaining and Installing143927 Node: Obtaining Proof General144430 Node: Installing Proof General from tarball145678 Node: Installing Proof General from RPM package146603 Node: Setting the names of binaries147158 Node: Notes for syssies148201 Node: Known Bugs150778 Node: References151271 Node: History of Proof General152267 Node: Old News for 3.0156238 Node: Old News for 3.1159993 Node: Old News for 3.2161263 Node: Old News for 3.3164315 Node: Old News for 3.4165324 Node: Function Index166466 Node: Variable Index172831 Node: Keystroke Index177163 Node: Concept Index184415  End Tag Table