The commonly quoted length of time expected for users to become well acquainted with Isabelle is a minimum of nine months. This is considerably longer than I have had time to spend. To remedy this, I selected the most abstract programming interface for a Isabelle (and in fact any other proof assistant) that was available. This minimised the need to learn complex details of the prover, and allowed me to focus on higher level concepts. A minimal set of features have been implemented, but these have been enough to proof simple theorems.
A working version of Isabelle with PGIP support was only made available to me by David Aspinall relatively late in the year. In order to continue making progress without a working system to practice on, I resorted to generating a range of valid PGIP messages by hand, and implementing as much of the classes involved in parsing that message as needed. In the meantime, I was able to go about the task of designing and redesigning GUI templates.
By the time I managed to get Isabelle talking PGIP, I had a reasonably large amount of code parsing most of the messages being received. It was then only a small step to producing code that built PGIP messages to be sent back to Isabelle. The task remaining at that point was to fit the operation of the GUI to the mediator class. This was sufficient to get Igloo up to the task of proving simple theorems such as the one in §A.2.
Working with an application programming interface (API) can be tough when that API is a moving target. A number of times I have encountered problems due to the code and documentation of PGIP being out of sync. Towards the end of the project, the amount of fluctuation in the API had lowered, and I was able to continue to work on my own code without worrying about updates to the API.
An added complication has been the incompleteness of PGIP. Some of my time has been spent documenting exactly where the incompleteness lies, sometimes with the purpose of avoiding the incomplete area, and sometimes with the aim to propose amendments that cover some of the lacking areas.
A working prototype is in itself quite an achievement for the time I have had to piece everything together. Had PGIP been more complete when I had started, I suspect that the project would not have been nearly as interesting. Once again I must thank David Aspinall and Christoph Lüth for help with their code.
The technical (rather than user-centered) direction the project has taken, has prevented significant user testing from taking place. Igloo has not had enough time to mature into a stable product suitable for in depth user testing. Without formal user feedback, I have had to make do with suggestions arising from demonstrations of Igloo to my supervisors, and to a few other willing guinea pigs.
Most of this feedback has been positive, with most finding the use of Igloo fairly simple to use, once the theorems have been specified. I have aimed to design a simple and elegant interface, and the Proof Window in particular being my largest success.
|
|
|