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:
  • Development snapshots, at http://isabelle.in.tum.de/devel
  • CVS version, at

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:

1. use the PGEclipse standalone product which provides a complete, basic environment in one install;
2. install the Proof General feature into a running Eclipse Platform;
3. 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.

• Visit: http://proofgeneral.inf.ed.ac.uk/eclipse/products

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).

• Eclipse is available from: http://www.eclipse.org/downloads

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:

1. Help -> Software Updates -> Find and Install
2. Select "search for new features to install" and click Next
3. 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

4. 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:

1. Install putty on your Windows machine
   1. PuTTY is available from http://www.chiark.greenend.org.uk/~sgtatham/putty/
2. Set up putty to do port forwarding
   1. Category: Connection -> SSH -> tunnels
   2. Source port: 7777, Destination: [Isabelle host]:7777
3. On the machine which has Isabelle, launch TPWrapper
   1. cd into the ProofGeneral bin directory (.../ed.inf.proofgeneral/bin)
   2. There, run: java ed.inf.proofgeneral.tpwrapper.TPWrapper 7777 isabelle -I -X &
   3. (alternatively run ant tpwrapper in the ed.inf.proofgeneral directory, if you have ant)
4. 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:

• Success and failure reports: see PGEclipseSuccessesAndFailures
• Installation issues: see PGEclipseInstallProbs
• Bugs: see PGEclipseBugs