You are here

Development of Proof General for Eclipse

Project ID: 
18
Current stage: 
Manager: 
Unit: 
What: 

Description:

Proof General is a generic interface for proof assistants (such as Isabelle, developed by LFCS and with a worldwide user base. Its interface is currently based on, and runs in XEmacs or GNU Emacs, but development has begun on porting this system to the IDE / development 'Platform' Eclipse.

Development of this software has so far been extensive but uncoordinated, and has been hampered by Eclipse's internals changing during development. The current version of Eclipse is 3.2, and this is the version which the proposed development effort will target.

The project is to create a usable product from the existing code, and a workable, single code base for future development on the project.

Deliverables: To fix a number of bugs and outstanding issues with the new Proof General platform. To update the Proof General codebase to be fully compatible with the latest version of Eclipse. To produce a product of at least beta quality. To create a framework of code tests and documentation.

Why: 

Customer: This project has been requested by Alan Bundy for CISA, and is funded by a grant provided to the institute.

Case statement: As CISA have specifically requested and funded this support, the development is to be performed as 'paid support'.

When: 

Status: This project has been allocated extra time, at the expense of the HiGraph project. It is now due for completion on 9-Feb-2007.

Timescales:

The entire project has a limited timescale of Oct - Dec 2006, as its time is constrained by the HiGraph development project and CISA's grant period.

It is desired that project should be complete by the end of 2006 (see status for update)

Priority:

This project is the only one scheduled during this timeframe, though as computing officer it is possible that operational matters might take priority, should any responsibilities require urgent attention.

At present there is no expectation that any other task should take a significant proportion of the allocated time.

Time:

This project is the only one scheduled during this timeframe, though as computing officer it is possible that operational matters might take priority, should any responsibilities require urgent attention.

At present there is no expectation that any other task should take a significant proportion of the allocated time.

How: 

Proposal: The existing Proof General Eclipse code base should be improved to a packaged, distributable product for the considerable existing base of users of Proof General (Emacs). The work should also leave a workable (single) code base for future development on the project.

Resources:

The project will require the development time of one CO.

This is a straightforward software development project with no exceptional computing demands, therefore no additional resources will be required.

Plan:

pending discussion with da, re new priorities.

  1. Familiarisation with existing code (ongoing)
  2. Make a packeagable product
  3. Fix most critical bugs
  4. Add testing framework
  5. Add user documentation
  6. Improve programmer documentation
  7. Implement more generic structure
  8. Merge code
Other: 

Dependencies:

The timescale for this project depends on the grant period, which ends in March and means that this project is sharing effort with the HiGraph project.

The project's development depends on external components which are also being developed; in particular work on the newer development branch involves working with the Proof General 'Broker', which is still under development, as is its communication protocol.

As these elements of the software are not guaranteed to be reliable, but which are outwith the scope of this project, it is important to note the project's dependency on this.

Risks: As this project involves a significant amount of familiarisation and refactoring of code, it carries with it a higher than average risk of becoming a larger task than specified. This risk resolves to one of two scenarios; either later milestones will not be reached, or the project will overrun into time allocated to CISA's HiGraphProject.

URL: https://wiki.inf.ed.ac.uk/DICE/ProofGenEclipseProject

Milestones

Proposed date Achieved date Name Description
2007-12-01 2006-11-17 package Make a packageable product
2007-02-05 2006-12-01 fix bugs Fix most critical bugs -- this continue after project completion, but a number of high-priority bugs have been fixed as of February 07, sufficient to allow several new releases.
2007-02-05 2006-12-08 testing Add testing framework
this has not been completed, having instead been handed to an external developer as of 05-Feb-2007.
2007-01-20 2006-12-15 documentation Add user documentation
2006-12-22 2006-12-22 developer docs Create programmer documentation
2006-11-30 2006-12-15 merge Merge code
this was partially performed, but deemed unnecessary as code structure underwent large changes.
2007-02-09 2007-02-09 complete Document completed work and remaining tasks for further development of Proof General.