Plans for Proof General on Eclipse

This is some ideas for GrahamDutton to do for ProofGeneralEclipse.


Oct --> Dec 2006
Work will now more closely resemble PGEclipseFixesNeeded

Jan --> Mar 2006
Work on the HiGraph interface will take place here.

Work on integrating HiGraph into this platform..?

Todo list

Please see PGEclipseFixesNeeded.

The following is in (rough) priority order. My commentary of the tasks is highlighted.

First tasks

Familiarisation work

  • Eclipse plugin/product development structure
  • the Proof General broker system (in practice)
  • Existing code structure (both branches will require investigation)
  • Meet with ex- and prospective developers

Stability and compatibility fixes with existing code

  • Port standalone version fully to Eclipse 3.2 release
    • build packaged versions in the framework instead of Dan's scripts
    • hopefully: plugin plus multiple-architecture ECP

Merge multiple branches and contributions to code


  1. Ahsan's branch with Dan's branch
    • Port fixes from Dan's branch to Ahsan's
  2. Any other work from Bremen -- probably not -- only if it's there
  3. Elina Timiriassova's GEF work, if useful/good enough -- _ not in CVS _
  4. Hua's code folding contribution * Code folding to view/hide bodies of proofs, using PGIP markup. class ProofScriptDocument
    • DONE This has been done by HuaYang , although not yet in CVS
    • I will presumably be responsible for integrating this 'missing' code, if it is complete but not present.
  5. Anything fixes/contributions Alex Heneveld may have on his tree
Pending discussion with those involved -- these are less important

Next Steps


  • Fix most annoying bugs so is useful for at least basic users

This will be a long-term goal; I will split this into sub-tasks as they become apparent.

  • Make tested packages available to users

* Add test suite infrastructure using JUnit

This is important and will probably come 'for free' as I understand the constituent classes in more depth.

Extensions to existing code

  • Esp symbol handling with PGML

See also my HiGraphToDo page.

  • Use PGIP configuration for syntax highlighting and shallow parsing

This appears to be an important goal, but seems quite involved. I estimate a couple of weeks, even once familiarised, for this.

  • Drag-and-drop for opening files, especially for HTML files (in TeacherView).

This may become 'simple' once I have familiarised myself with Eclipse development, but it might yet move down the list...


  • Change variable names, move proofs and theory steps around. Some things could be done with PGIP markup and using embedded name attributes.

I anticipate that this is important and feasible to complete, to some extent. However probably shouldn't be undertaken until I am very familiar with the code.

Visual browsing/design of theories

* One of the ProofEngineering ideas is to support visual construction and browsing of theories. We plan research into a graphical language for doing this, inspired by existing work such as IsaPlanner's hiproof navigator.

I would expect that I could provide some starting points for this, from my work with HiGraph. However this is a fairly low-priority task (speaking with my HiGraph hat on).

Unknown Tasks

I would welcome any input on the following:

* Use latest PGIP features for syntax

  • Consider removing/PGIP-supporting current non-PGIP features
  • Use interfaces ''IProofScriptDocument'' and ''IProofScriptEditor'' instead of ProofScriptDocument and ProofScriptEditor, respectively. This will allow externally created documents (implementing those interfaces) to work with Proof General Eclipse. Status: partly done.

  • Extend DefaultSymbolTable.sym in config/ directory to include standard PGML symbols (FIXME: link to doc here)

  • [ Try to get preferences table for prover created dynamically from PGIP (NB: probably need update button and then restart, otherwise Eclipse hacking) | preferences, how to dynamically extend with prover stuff. ]
    • NB: config directory has a README file in it

* IsaPlanner would benefit from interface support within Proof General. We need to design PGIP extensions to support tools like it.

I suspect that this is beyond the scope of my work.

-- GrahamDutton - 06 Sep 2006

Topic revision: r10 - 27 Nov 2006 - 08:58:55 - GrahamDutton
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