-It is fairly easy to get basic support for Proof General for -HOL, 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. -
--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-HOL Emacs -interface by Koichi Takahashi and Masima Hagiya addressed this -problem, as well as providing support for proof-by-pointing to HOL. -Their interface could perhaps be reinterpreted or reimplemented inside -Proof General. Implemented in a generic way, batch script editing -would also be useful for Isabelle. -
--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). -
--Finally, to fully support the current Proof General feature set, -it would be useful to extend HOL with support for communicating -file-dependency information to Proof General, and term-structure -markup for proof by pointing. -
-Skills: -Some Standard ML, some Emacs Lisp. Basic understanding of -proof assistant behaviour, interest in HOL. -
-Proposer: -David Aspinall. -
-- cgit v1.2.3