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

  • Parsing proof scripts in Isabelle is unreliable and incomplete.
    • 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.
    • 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.
Topic revision: r29 - 19 Aug 2007 - 12:05:28 - DavidAspinall
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
This Wiki uses Cookies