diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2003-09-24 23:56:17 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2003-09-24 23:56:17 +0000 |
| commit | 5d0dc57d27f1ab8da216032a6fd25541d39ca9ae (patch) | |
| tree | c54eeb0c255dad88563a6174b4a05ac727880dd4 /html | |
| parent | f26d9fd4b9886082435d076004eeebdfeea2ef4b (diff) | |
Describe work currrently underway; distribute some docs
Diffstat (limited to 'html')
| -rw-r--r-- | html/kit.php | 39 |
1 files 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 |