You are here

Proof General Eclipse Improvements

Project ID: 
Current stage: 

Description: Further improvements to the Proof General Eclipse system.

Deliverables: A number of items, as required, from the Proof General Trac system. Non-specifically, to leave Proof General Eclipse a more useable system than when the project began.


Customer: David Aspinall, for CISA.

Case statement: The new Proof General Eclipse system is a promising replacement for the existing Proof General, and also has the potential to provide useful new facilities. One of these is as an *integration platform* for proof tools developed within the Mathematical Reasoning Group and beyond.


Status: This project has been 'pre-approved' by grant.

This will be an 'ongoing' project whose status is difficult to measure. See milestones.

Timescales: The project has been approved to take 3 months of CO time, spread over
12 months from July 2007. The timescale of each task is undefined; I anticipate a tradeoff between importance and number of tasks completed within this fixed period of time.

Priority: As this work is defined as 3 months' CO time, to be spread over 12 months, it can take as low a priority is required to deal with regular CO duties. Its priority will likely rise as the period draws to a close and 'tidy-up' work is performed.

Time: The project has been approved to take 3 months of CO time, spread over
12 months from July 2007.


Proposal: The implementation work involved for this plan includes some refactoring and fixes to the existing Proof General Eclipse system, as well as an extension of the document model and connection to additional tools within Eclipse. The changes required are conceptually straightforward, but technically involved.

Resources: This project requires only a standard DICE environment, and a CO, preferably one who is familiar with the Proof General system.

Plan: The plan is to tackle one or two items from Trac at any one time, reporting back to David Aspinall. As the nature of these items is unknown until specified, there is no longer-term plan.


Dependencies: This project may depend on latest and changing builds of Isabelle.

Risks: As this project is based largely on as-yet undefined work, the only risk is that the specified tasks are so large or complex that only a small number of tasks are completed within the timescale. The risk of CO duties overriding the project is very small due to the extended timeframe within which the work can take place.



Proposed date Achieved date Name Description
2007-08-10 2007-07-01 Establish goals At this point, the Eclipse IDE should be updated with the latest Mylar plugin, and the environment optimised for work on an Eclipse Plug-in project. Registration with Trac will be required. First tasks should be selected from the Trac alongside discussion with DA.
2007-08-15 2007-08-01 Work Begins Part-time implementation of the project begins. New items should be selected from Trac as previous ones are completed, or as specified by DA.
2009-01-15 Wind-up Nearing the end of the project period, final goals should be specified such that nothing is left in an unusable state.
2009-01-31 Completion Project is complete, with 'handover' of final work performed.
2008-12-20 2008-12-20 Work Continues Fix as many Trac items as possible within the available time.
2009-05-31 Residual effort Remaining effort to be spent as directed.