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 kit@proofgeneral.org

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).

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