Plans for Proof General on Eclipse

This is some ideas for GrahamDutton to do for ProofGeneralEclipse.

Timescale

Oct --> Dec 2006

Jan --> Mar 2006

Beyond

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

Combine:

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
   • 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

Next Steps

General

• 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...

Refactoring

• 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