diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2010-09-29 12:15:41 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2010-09-29 12:15:41 +0000 |
commit | c6dc09f3633aa500c6f0d2924f5effd5e734d8ac (patch) | |
tree | 3efd50da4dec68a672eb440ee82c4558acfd3e7c /hol-light/README | |
parent | b225466ee703a1845f81bb3ae431e462b03d5533 (diff) |
Experimental hol-light version, not usable yet
Diffstat (limited to 'hol-light/README')
-rw-r--r-- | hol-light/README | 53 |
1 files changed, 53 insertions, 0 deletions
diff --git a/hol-light/README b/hol-light/README new file mode 100644 index 00000000..edcba896 --- /dev/null +++ b/hol-light/README @@ -0,0 +1,53 @@ +HOL Light in Proof General. + +Written by David Aspinall. + +Status: not officially supported yet +Maintainer: volunteer required +HOL-Ligh version: +HOL homepage: http://hol.sourceforge.net + +======================================== + + +This is a "technology demonstration" of Proof General for HOL-Light. + +It may work with other versions of HOL, but is untested (please let me +know if you try). Probably just a few settings need changing to +configure for different output formats. + +It has basic script management support, with a little bit of +decoration of scripts and output. + +There is support for Unicode Tokens. + +I have written this in the hope that somebody from the HOL-Light +community will adopt it, maintain and improve it, and thus turn it +into a proper instantiation of Proof General. + + +------------ + +Notes: + +There are some problems at the moment. HOL proof scripts often use +batch-oriented single step tactic proofs, but Proof General does not +offer an easy way to edit these kind of proofs. The "Boomburg-HOL" +Emacs interface by Koichi Takahashi and Masima Hagiya addressed this, +and to some extent so perhaps does the Emacs interface supplied with +HOL. Perhaps one of these could be embedded/reimplemented inside +Proof General. Implemented in a generic way, managing batch vs +interactive proofs might also be useful for other provers. + +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. This could be improved by taking a +better parser (e.g. from sml mode). + +These improvements would be worthwhile contributions to Proof General +and also provide the HOL community with a nice front end. +Please have a go! + + +$Id$ + |