From 5d0dc57d27f1ab8da216032a6fd25541d39ca9ae Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 24 Sep 2003 23:56:17 +0000
Subject: Describe work currrently underway; distribute some docs

---
 html/kit.php | 39 +++++++++++++++++++++++++++++----------
 1 file changed, 29 insertions(+), 10 deletions(-)

diff --git a/html/kit.php b/html/kit.php
index 0aa4015e..b41317c9 100644
--- a/html/kit.php
+++ b/html/kit.php
@@ -4,7 +4,7 @@
   ?>
 
 <p>
-The Proof General Kit project is in an early pre-experimental stage at
+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
 <a href="mailto:kit@proofgeneral.org"><tt>kit@proofgeneral.org</tt></a>
@@ -29,18 +29,37 @@ Ideas for the future of Proof General are described in these papers:
 
 <h3>Development</h3>
 <p>
-Not much has been started yet.
-<br>
-But you can download the DTDs for PGIP and PGML, here:
-</p>
+Work which is currently in progress includes:
 <ul>
-<li><?php download_link("Kit/dtd/pgip.dtd") ?>
-</li>
-<li><?php download_link("Kit/dtd/pgml.dtd") ?>
-</li>
+ <li>The definition of PGIP and PGML, as 
+     <a href="http://www.relaxng.org">RELAX NG</a> schemas.<br>
+     Recent versions: 
+      <?php download_link("Kit/dtd/pgip.rnc") ?>,
+      <?php download_link("Kit/dtd/pgml.rnc") ?>.
+     <br/>
+     The derived DTDs are:
+      <?php download_link("Kit/dtd/pgip.dtd") ?>,
+      <?php download_link("Kit/dtd/pgml.dtd") ?>.
+     <br/>
+     There is also a <b>draft</b> commentary available,
+      <?php download_link("Kit/docs/commentary.pdf") ?>.
+     <br/>
+     This updates the white paper mentioned above.
+
+ </li>
+ <li>Together with <a href="http://www.informatik.uni-bremen.de/~cxl/">Christoph Lüth</a>:
+     a Haskell front-end and PGIP mediator, described in a
+       <a href="http://www.informatik.uni-bremen.de/uitp03/">UITP '03</a>
+       paper <a href="Kit/docs/uitp03.pdf">here</a>.
+ <li>With assistance from Isabelle developers at Munich:
+     a PGIP-enabled version of Isabelle/Isar
+     (patch available soon).
+ </li>
 </ul>
+</p>
 <p>
-Comments and contributions welcomed!
+We hope to make an alpha version of some software available in the
+not-<em>too</em>-distant future. 
 </p>
 
 <?php
-- 
cgit v1.2.3