diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-03-09 11:08:10 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-03-09 11:08:10 +0000 |
| commit | d6a021df262590c8ec79834e3019ae34eb7c3e7e (patch) | |
| tree | 13bec934f62393295e1da568730d19ce06b832c7 /html | |
| parent | f2d1f72dc8bb8239f2deb41d5d022a99c4dbbb42 (diff) | |
Added project for HOL PG
Diffstat (limited to 'html')
| -rw-r--r-- | html/projects.phtml | 1 | ||||
| -rw-r--r-- | html/projects/hol.html | 34 |
2 files changed, 35 insertions, 0 deletions
diff --git a/html/projects.phtml b/html/projects.phtml index e46ca495..debd1385 100644 --- a/html/projects.phtml +++ b/html/projects.phtml @@ -30,6 +30,7 @@ title. <li><?php pgproject("pgip","A New Protocol for Interactive Proof in Proof General") ?></li> <li><?php pgproject("webreplay","A Web-based Proof Replayer for Proof General") ?></li> <li><?php pgproject("test","A Test Harness and Test Suite for Proof General") ?></li> +<li><?php pgproject("hol","An instance of Proof General for HOL") ?></li> </ol> <h2>B. Projects not directly involving Proof General</h2> diff --git a/html/projects/hol.html b/html/projects/hol.html new file mode 100644 index 00000000..80e9e208 --- /dev/null +++ b/html/projects/hol.html @@ -0,0 +1,34 @@ +<h2>Proof General for HOL</h2> +<p> +It is fairly easy to get basic support for Proof General for +<a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html">HOL</a>, and +this has recently been tried for HOL 98. However, it would be a bigger +and more interesting project to get proper and complete support for +HOL working. There are a couple of problems unique to HOL. +</p> +<p> +Much more than Isabelle, HOL relies on its meta language, ML. HOL +proof scripts often use batch-oriented single step tactic proofs +constructed in ML, but Proof General does not offer an easy way to +edit these kind of proofs (as opposed to multi-step interactive +proofs). The "Boomburg" Emacs interface by Koichi Takahashi and +Masima Hagiya addressed this problem, as well as providing support for +proof-by-pointing to HOL. Their interface (which is no longer +maintained) could perhaps be embedded or reimplemented inside Proof +General. Implemented in a generic way, batch script editing would +also be useful for Isabelle. +</p> +<p> +Another problem is that HOL scripts sometimes use SML structures, +which can cause confusion because Proof General does not really parse +SML, it just looks for semicolons. Again, this could be improved by +taking a better parser (e.g. from sml mode). +</p> +<p> +<b>Skills:</b> +Some Standard ML, some Emacs Lisp. Basic understanding of +proof assistant behaviour. +</p><p> +<b>Proposer:</b> +<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>. +</p> |