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.
Download and unpack the zip file for your architecture. The executable
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.
To add Proof General as an installation site to your running Eclipse platform:
Proof General Eclipse
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.