Instructions for installing Proof General
=========================================

This file describes what to do to be able to run Proof General.
Please let us know if you have any problems in trying to install it.

Unpack this distribution in some <directory>.  Put this line in your
.emacs file:

    (load-file "<directory>/generic/proof-site.el")

This will set the Emacs load path and add auto-loads for the
assistants below:

  .v	    Coq files
  .l	    LEGO files
  .thy,.ML  Isabelle files

When you load a file with one of these extensions, the corresponding
Proof General mode will be entered.

You cannot run more than one instance of Proof General at a time: so
if you're using Coq, don't edit .ML files!  If there are some assistants
supported that you never want to use, you can remove them from
the variable `proof-assistants` in proof-site.el to solve this problem.

The easiest way to do this (and most other customization of Proof
General) is via the Customize mechanism, see the menu:

  Options -> Customize -> Emacs -> External -> Proof General

or, after loading Proof General, in a proof script buffer

  Proof-General -> Customize

You may need extra customization depending on the proof assistant (for
example, the name of the proof assistant binary).  See the menu

  Proof-General -> Customize -> <Name of Assistant>

and the notes below for more details.

If you are installing Proof General site-wide, you can put the
components in separate directories, providing the variables in
proof-site.el are adjusted accordingly.  Make sure that the generic
and assistant-specific elisp files are kept in subdirectories of
proof-home so that the autoload directory calculations are correct.


   In case of difficulty, please contact us via the address below.
   
   Proof General maintainer <proofgen@dcs.ed.ac.uk>
   School of Computer Science,
   Division Of Informatics,
   University of Edinburgh.
   Edinburgh.
   
   http://www.dcs.ed.ac.uk/home/proofgen


----------------------------------------------------------------------

Notes for Coq
=============

If you want to use this mode for Coq, you need to make sure you have
an appropriate version, which is from later than 1 March 1998.

Check the values of coq-tags and coq-prog-name in coq.el to see that
they correspond to the paths for coqtop and the library on your system.

Install coqtags in a standard place or add <proof-home>/coq to your PATH.
NB: You may need to change the path to perl at the top of the file.

If you are running Coq, generate a TAGS file for the library by running
	coqtags `find . -name \*.v -print`
in the root directory of the library, $COQTOP/theories.  If you are
running LEGO, do the same using legotags in the appropriate directory.


----------------------------------------------------------------------

Notes for LEGO
==============

Install legotags in a standard place or add <proof-home>/lego 
to your PATH.
NB: You may need to change the path to perl at the top of the file.


----------------------------------------------------------------------

Notes for Isabelle
==================

Check the value of isabelle-prog-name.

The distribution includes a version of Isamode's theory file mode.
Use C-h m to check on the features available.

Notice that because Isabelle automatically loads .ML with the same
names as theory files, a sensible way of working with script
management may be to develop your proofs in another file first.
At the moment the interface has no way of knowning that a particular
ML file has been automatically loaded.