PG Eclipse: Summary of current Issues

This is a list of issues with PG Eclipse which may be show-stopper problems for users.

Fixing these will allow Proof General Eclipse to present a real alternative to the current Emacs Proof General.

Many issues and bugs have been fixed since September 2006 (interesting if you're using an older version of the plugin): see PGEclipseFixesMade for outlines of these.

The most up-to-date bug and enhancement information (at a more technical level) is on the Proof General trac. We welcome contributions and improvements from others; please see PGEclipseDevelopment.

Potential show stoppers

• Only Isabelle is supported (fully) at present; code uses PGIP but still contains hard-wired specifics.
  See http://proofgeneral.inf.ed.ac.uk/trac/ticket/42

• Parsing proof scripts in Isabelle is unreliable and incomplete.
  See http://proofgeneral.inf.ed.ac.uk/trac/ticket/83
  • You may see warnings about unrecognised theory elements; some files may even fail to parse.
  • It is hoped that this can be fixed in time for Isabelle2007.

• Symbol handling is not equivalent to X-Symbol in Emacs
  • Many Unicode glyphs supported, but some X-Symbols may be missing
  • Subscript or superscript aren't currently supported.
    See http://proofgeneral.inf.ed.ac.uk/trac/ticket/80
  • On the plus side, glyph/HTML output is extensible using HTML, Unicode and style sheets

• Efficiency and performance
  • Eclipse itself requires more resources than Emacs
  • There are some efficiency problems which require more work.

• Code and usability quality is being improved gradually; various intermittent bugs and usability flaws still remain.

Important note for users new to Eclipse

• Eclipse requires that all its files are stored in a Project in the Eclipse workspace
  • Existing files must be imported (i.e. copied or linked) into the Eclipse workspace
  • This does not impact on usability, but is important to understand, and is unlikely to change in future.