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.

See:

• General Information
  • NotesAboutEclipse - some useful notes and pointers on PGEclipse for Proof General users
  • PGEclipseScreenshots - showing the new product in action
• User Assistance
  • PGEclipseInstall (and PGEclipseInstallProbs)- installation instructions
  • PGEclipseUserDocumentation - user documentation
  • (also on the main Proof General pages in less detail).
  • GripesAboutEclipse - some complaints about Eclipse, particularly from those moving from Emacs
• Development documentation
  • PGEclipseFixesNeeded - current problems with the system
  • PGEclipseFutureIdeas - ideas for future functionality
  • PGEclipseFixesMade - problems solved in the latest releases
  • PGEclipseDevelopment - help with developing Proof General