Proof General Eclipse

Eclipse is an open source IDE originally developed by IBM. It started as a Java development environment, but has been re-engineered to be a general-purpose development environment. Plugins are available that provide state-of-the-art tools for working with a wide range of systems and projects. The Proof General Eclipse plugin supports theorem provers using the PGIP protocol.

Proof General Emacs is not yet as robust as PGEmacs but is now suitable for early adopters and small-scale use. Please help us by reporting problems and contributing improvements.

See:

• Download and Installation
  • Downloads and brief instructions are on the main Proof General pages
  • Further details on this wiki: PGEclipseInstall and PGEclipseInstallProbs
• General Information
  • PGEclipseFixesNeeded - current problems with the system; consult this before considering for serious use
  • NotesAboutEclipse - some useful notes and pointers on PGEclipse for Proof General users
  • PGEclipseScreenshots - showing the new product in action
  • PGEclipseUserDocumentation - user documentation.
  • GripesAboutEclipse - some warnings about Eclipse, particularly from those moving from Emacs
• Development documentation
  • PGEclipseFutureIdeas - ideas for future functionality
  • PGEclipseFixesMade - problems solved in the latest releases
  • PGEclipseDevelopment - help us with developing Proof General
  • Bugs, enhancements and project planning on Proof General Trac