     START-INFO-DIR-ENTRY
     * ProofGeneral::Organize your proofs with Emacs!
     END-INFO-DIR-ENTRY

Proof General
*************

This file documents version 2.0 of Proof General, a generic Emacs interface for proof assistants.

Proof General 2.0 has been tested with XEmacs 20.4 and FSF GNU Emacs 20.2.  It is supplied ready customized for the proof assistants Coq, Lego, and Isabelle.

Introducing Proof General
*************************

Proof General is a generic Emacs interface for proof assistants, developed at the LFCS in the University of Edinburgh.

Proof General works best under XEmacs, but can also be used with FSF 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 in place rather than line-by-line in a shell using cut-and-paste to reassemble 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.

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, 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 keys for the current mode.

The proof assistant is automatically started inside Emacs when you ask for some of the proof script to be processed.  To follow an example use of Proof General on a LEGO proof, see Walkthrough example in LEGO.

If Proof General has not already been installed, you should insert the line:

             (load "PROOFGENERAL/generic/proof-site.el")

into your ~/.emacs file, where PROOFGENERAL is the directory that Proof General was unpacked in.

For more details on obtaining and installing Proof General, see Obtaining and Installing Proof General.

Features of Proof General
=========================

Here is an outline of the main features of Proof General.

  * Simplified communication
     The proof assistant's shell is normally hidden from the user. Communication takes place via two or 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 assistants. This means that the user only sees the output from the most recent proof step, rather than a screen full of output from the proof assistant.

     For more details, see The buffer model.

  * Script management
     Proof General colours proof script regions blue when they have already 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.

     For more details, see Basic Script Management and see 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. Special editing functions send lines of proof script to the proof assistant, or undo previous proof steps.

     For more details, see Script editing commands and see 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, see Toolbar commands, see Other commands, and see Customizing Proof General.

Supported proof assistants
==========================

Proof General comes ready-customised for these proof assistants:

  * LEGO Proof General for LEGO Version 1.3.1

     LEGO Proof General supports all of the generic features of Proof General.

     See LEGO Proof General for more details.

  * Coq Proof General for Coq Version 6.2

     Coq Proof General supports all of the generic features of Proof General except multiple files.

     See Coq Proof General for more details.

  * Isabelle Proof General for Isabelle 98-1

     Isabelle Proof General supports all of the generic features of Proof General, excepting the external tags program.   It handles theory files as well as ML (proof script files), and has an extensive theory file editing mode taken from Isamode.

     See Isabelle Proof General for more details.

Proof General is designed to be generic, so you can adapt it to other proof assistants if you know a little bit of Emacs Lisp. See Adapting Proof General to New Provers for more details of how to do this.

Basic Script Management
***********************

Proof scripts
=============

A proof script is a sequence of commands to a proof assistant used to construct a proof.  Proof General is designed to work with interactive proof assistants, where the mode of working is usually a dialogue between the user and the proof assistant.

Primitive interfaces for proof assistants simply present a shell-like view of this dialogue: the user repeatedly types commands to the shell until the proof is completed.  The system responds at each step, maybe with a new list of subgoals to be solved, or maybe with a failure report.

Often we want to keep a record of the proof commands used to prove a theorem, in the form of a proof script kept in a file.  Then we can replay the proof later on to reprove the theorem, without having to type in all the commands again.

Using only a primitive shell interface, it can be tedious to construct proof scripts with cut-and-paste.  Proof General helps organize interactive proofs by issuing commands directly from a proof script file, while it is written and edited.

Goals and saves
---------------

A proof script contains a sequence of commands used to prove one or more theorems.  In general we assume that for each proved theorem, a  proof script contains a goal .. save  pair of commands which look something like this:

        goal T is G
        ...
        save theorem T

          Proof General recognizes goal .. save pairs in proof scripts.
          The name T can appear in the definitions menu for the proof
          script see Script definitions menu, and once
          a goal .. save pair is completed it is treated
          as atomic when undoing proof steps see Undo.

The buffer model
================

Proof General runs your proof assistant in a shell buffer in Emacs. This proof shell buffer is usually hidden from view. (Occasionally you want to find it, see Finding the proof shell). When Proof General sees an error in the shell buffer, it will highlight the error and display the buffer automatically.

Communication with the proof shell takes place via two or three intermediate buffers.

The script buffer holds input destined for the proof shell, in the form of a proof script.  Normally this is a buffer visiting a file, which can be later loaded directly by the prover to replay the proof.

The goals buffer displays the current list of subgoals to be solved for a proof in progress.  This is normally displayed at the same time as the script buffer.

The response buffer displays other output from the proof assistant, for example warning or informative messages.

Optionally, the goals buffer and script buffer can be identified see Identify goals and response.  The disadvantage of this is that the goals display can be replaced by other messages, so you must ask for it to be refreshed.  The advantage is that it is simpler to deal with fewer Emacs buffers.

Regions in a proof script
=========================

Script editing commands
=======================

Script processing commands
==========================

Toolbar commands
================

Other commands
==============

Walkthrough example in LEGO
===========================

Advanced Script Management
**************************

Finding the proof shell
=======================

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.

Although the proof shell is usually hidden from view, it is run in an buffer which provides the usual full editing and history facilities of Emacs shells, see Comint

If you're running Isabelle, the proof shell buffer will be called something like *Inferior Isabelle*.  You can switch to it using C-x b (switch-to-buffer).

Warning: you can probably cause confusion by typing in the shell buffer!  Proof General may lose track of the state of the proof assistant.

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, but it may not be guaranteed when the restricted interface is by-passed.  What happens depends on how complete the communication is between Proof General and the prover (which depends on the particular instantion of Proof General).

View of processed files
=======================

Switching between proof scripts
===============================

Retracting across files
=======================

Customizing Proof General
*************************

Setting user options
====================

Running on another machine
==========================

Tweaking configuration settings
===============================

LEGO Proof General
******************

LEGO specific commands
======================

LEGO customizations
===================

Coq Proof General
*****************

Coq specific commands
=====================

Coq customizations
==================

Isabelle Proof General
**********************

Isabelle specific commands
==========================

Isabelle customizations
=======================

Adapting Proof General to New Provers
*************************************

Skeleton example
================

Proof script settings
=====================

Proof shell settings
====================

Special annotations
-------------------

Internals of Proof General
**************************

Proof script mode
=================

Proof shell mode
================

Credits and References
**********************

Credits
=======

LEGO Proof General was written by Thomas Kleymann and Dilip Sequeira.

Coq Proof General was written by Healfdene Goguen.

Isabelle Proof General was written by David Aspinall.

The generic base for Proof General was developed by all four of us.

Thomas Kleymann provided the impetus to develop a generic Emacs interface, following ideas used in Projet CROAP, and with the help of Yves Bertot.  David Aspinall provided the Proof General name and images.

An early version of this manual was written by Thomas Kleymann and Dilip Sequeira.  The present version was prepared by David Aspinall and Thomas Kleymann.

References
==========

Script management as used in Proof General is described in the paper:

  * Yves Bertot and Laurent Théry. A generic approach to building user interfaces for theorem provers. To appear in Journal of Symbolic Computation.

Proof General has the beginnings of support for proof by pointing, as described in the document:

  * 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

Obtaining and Installing Proof General
**************************************

Known bugs and workarounds
**************************

Plans and ideas
***************