Installing Proof General for Eclipse

At the moment we aren't ready for prime time. The interface is usable for basic proof
replay and simple editing. Compared with the Emacs version,
there are some annoying glitches and missing features (see
PGEclipseFixesNeeded).
The version here is based on an old
architecture that does not yet use the PGBroker; if you are interested in
development please see
PGEclipseSources.

: Installing is now much easier than before. We've updated the releases to
builds based on Eclipse 3.2.1 and the latest CVS and added an Eclipse update
site at
http://proofgeneral.inf.ed.ac.uk/eclipse.
Prerequisites
- You need Java, JRE v1.5 or above. If you are not sure what java you have installed, type
java -version
to check.
Visit http://java.sun.com to download if necessary.
- You will need a PGIP enabled theorem prover to use Proof General with.
Currently, Proof General Eclipse only runs properly with the latest versions of Isabelle:
If you are not sure what version of Isabelle you have installed, type 'isabelle -I -X'. This should produce a stream of xml output ending
with the string "</ready>". If not, you don't have PGIP-enabled Isabelle.
Download Proof General for Eclipse
Your choices are:
- use the PGEclipse standalone product which provides a complete, basic environment in one install;
- install the Proof General feature into a running Eclipse Platform;
- compile and run from sources: see PGEclipseSources.
The first two options are easy. The third option is less easy and you'll have several more choices to make.
It's only recommended for those interested in Proof General development.
PGEclipse, a standalone Eclipse product
This is the recommended way to use Proof General if you are
not already an Eclipse user or you don't want to mess with
an existing Eclipse installation. It gives you a slightly simpler interface and
a single (but big!) download.
Download and unpack the zip file for your architecture. The executable
is called
PGEclipse
.
We won't rebuild PGEclipse often but you can automatically update
it using the menu Help -> Software Updates.
You can also extend it by adding extra Eclipse Project or other third-party features
(e.g. LaTeX editing via
Texlipse).
Proof General feature for existing Eclipse Platform
This allows you to install Proof General as a plugin in an existing Eclipse installation.
You will need to have installed Eclipse v3.2.1 first
(v3.2 is probably OK too: please confirm on
PGEclipseSuccessesAndFailures).
You can use the default
Eclipse SDK download or instead (if you're not interested in Java
development), start from the pared down
Platform Runtime Binary which does not include the Eclipse Java environments
or source files. This will give you a similar system to the
PGEclipse distribution above.
To install Proof General, you need to add the Proof General Eclipse web site as an
installation site:
- Help -> Software Updates -> Find and Install
- Select "search for new features to install" and click Next
- Click on "New Remote Site" and add the update site for Proof General:
- Name
-
Proof General Eclipse
- URL
-
http://proofgeneral.inf.ed.ac.uk/eclipse
- Then enable the new site, and install the Proof General Eclipse feature you are offered and follow the instructions.
After this you will have Proof General available in your Eclipse install.
You will be able to update it via the same menu, or disable or uninstall it
via
Help -> Software Updates -> Manage configuration.
Running Proof General
- Assuming a PGIP-enabled Isabelle is already installed on your system, you are almost ready to run. You just need to change some of the settings in the preference pages (see Proof General->System Isabelle under the Window->Preferences menu).
- Once in Eclipse, you'll probably want to open the Proof General Perspective (via the menu Window->Open Persepctive->Other, or using the new perspective button). You may also want to open the views Outline, Bookmarks, Current Prover State and Error Log. The Session Log view is probably of less interest, except when debugging.
- There isn't much documentation at the moment, please help us extend PGEclipseUserDocumentation
Using Isabelle remotely from a Windows machine
Here's how you can run Isabelle remotely from another machine:
- Install putty on your Windows machine
- PuTTY is available from http://www.chiark.greenend.org.uk/~sgtatham/putty/
- Set up putty to do port forwarding
- Category: Connection -> SSH -> tunnels
- Source port: 7777, Destination: [Isabelle host]:7777
- On the machine which has Isabelle, launch TPWrapper
- cd into the ProofGeneral bin directory (.../ed.inf.proofgeneral/bin)
- There, run:
java ed.inf.proofgeneral.tpwrapper.TPWrapper 7777 isabelle -I -X &
- (alternatively run
ant tpwrapper
in the ed.inf.proofgeneral directory, if you have ant)
- In the Proof General Preferences, tick 'use remote version', and fill in the port number 7777
Notes: there are problems with this, for example, Isabelle will be sent CD commands with
Windows-style paths that probably do not exist or give errors on the remote machine. This will
probably stop Isabelle from loading dependent theories automatically.
TODO: Allow PGEclipse to distinguish between important and spurious errors when in remote mode.
Feedback
Thank you for trying out the early version of Proof General for Eclipse. Please let us know how you get on by adding questions and comments to this wiki: