Proof General Home

Proof General Eclipse (Update Site and Product Download)

Proof General Eclipse is an application based on the Eclipse IDE which supports interactive theorem provers.

At the moment this release is very unstable. It supports recent versions of Isabelle, or the current development version. For best results we recommend building Isabelle 2009-2 or later.
See the wiki for full installation instructions. Please note that this is an early beta prototype and not yet recommended for real use. There are issues documented here which we are working to fix. If you're undeterred, please fill the registration form so we can get an idea of interest.

Please help us improve Proof General! You can suggest ideas and contribute documentation and discussion on the wiki and trac project management system. If you know Java you can help with development.

Proof General Eclipse is part of the Proof General Kit project which is providing a suite of tools and novel techniques to support proof development, replacing the current Emacs-based Proof General.

PGEclipse standalone Eclipse product (recommended)

Download and unpack the zip file for your architecture. The executable is called PGEclipse. It requires JRE 5.0. To get the latest updates (or in progress plugins for other provers), go to Help -> Software Updates -> Find and Install.

Update Site: Proof General Plugin Feature

To add Proof General as an installation site to your running Eclipse platform:

  1. Select in the menu 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
  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.

We do not recommend extending your own Eclipse installation as it is more likely to throw up compatibility problems which we cannot test for. Using our standalone product is simpler. Nonetheless, please report any problems you have if you follow this route.

Web pages by David Aspinall. Please report issues on PG trac.