The Proof General Kit project is in an early experimental stage at the moment. If you are interested in collaborating, or have ideas or suggestions to contribute, please send a note to da+pg-kit@inf.ed.ac.uk

Planning

Ideas for the future of Proof General are described in these papers:

• David Aspinall. Protocols for Interactive e-Proof. Draft version, see here.
• David Aspinall. Proof General Kit (white paper). Draft version, see here.

Development

Work which is currently in progress includes:

• The definition of PGIP and PGML, as RELAX NG schemas.
  Recent versions: , .
  The derived DTDs are: , .
  There is also a draft commentary available, .
  This updates the white paper mentioned above.
• Together with Christoph Lüth: a Haskell front-end and PGIP mediator, described in a UITP '03 paper here.
• With assistance from Isabelle developers at Munich: a PGIP-enabled version of Isabelle/Isar (patch available soon).
• Work on Eclipse Proof General, an Eclipse front end for Proof General (new project sponsored by IBM award).

We hope to make an alpha version of some software available in the not-too-distant future.