General plans for Proof General on Eclipse

Here are our plans for some next things to implement in ProofGeneralEclipse. For a higher-level view on our goals, see PGEclipseFutureIdeas.

For more details at a lower level and most up-to-date, please see information in trac.

Merge multiple branches and contributions to code

We need to amalgamate:

  1. Ahsan's branch: updated Broker support, event and preference page improvements
  2. Elina Timiriassova's GEF work, if useful/good enough
  3. Fixes/contributions Alex Heneveld may have (standalone, features)

Improvements to existing code

  • Add test suite infrastructure using JUnit
  • Use latest PGIP features for syntax (keyword configuration, etc)
  • Use PGIP features for content generation (objtypes)
  • Try to get preferences table for prover created dynamically from PGIP (NB: probably need update button and then restart, otherwise Eclipse hacking)

More advanced extensions

  • Handling multiple provers
  • Refactoring and other high-level operations
  • Interfacing to IsaPlanner
  • Interfacing to HiProof browser
  • Further visualisations
Topic revision: r8 - 08 Jul 2007 - 16:15:32 - DavidAspinall
Main.PGEclipsePlans moved from Main.PGEclipseToDo on 27 Sep 2006 - 12:02 by 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