Plans for Proof General on Eclipse
This is some ideas for
GrahamDutton to do for
ProofGeneralEclipse.
Timescale
Oct --> Dec 2006
Work will now more closely resemble
PGEclipseFixesNeeded
Jan --> Mar 2006
Work on the
HiGraph interface will take place here.
Beyond
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
Combine:
- Ahsan's branch with Dan's branch
- Port fixes from Dan's branch to Ahsan's
- Any other work from Bremen -- probably not -- only if it's there
- Elina Timiriassova's GEF work, if useful/good enough -- _ not in CVS _
- 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.
- Anything fixes/contributions Alex Heneveld may have on his tree
Pending discussion with those involved -- these are less important
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