[ << ] [ >> ] [Top] [Contents] [Index] [ ? ]

13. HOL Light Proof General

HOL Light Proof General is a "technology demonstration" of Proof General for HOL Light. This means that only a basic instantiation has been provided, and that it is not yet supported as a maintained instantiation of Proof General.

HOL Light Proof General has basic script management support, with a little bit of decoration of scripts and output. It does not rely on a modified version of HOL Light, so the pattern matching may be fragile in certain cases.

See the ‘example.ml’ file for a demonstration proof script which works with Proof General.

Note that HOL Light Proof Script proof scripts often use batch-oriented single step tactic proofs, but Proof General does not (yet) offer an easy way to edit these kind of proofs. They will replay simply as a single step proof and you will need to convert from the interactive to batch form as usual if you wish to obtain batch proofs. Also note that Proof General does not contain an SML parser, so there can be problems if you write complex ML in proof scripts.

HOL Light is the most recently tested version of HOL with Proof General, but the Proof General distribution also contains experimental support for HOL 4 (aka HOL 98). To improve this older version, or to support a new HOL variant, a few of the settings probably need to be tweaked to cope with small differences in output between the systems. Please let us know if you try this out and want help. We welcome any interested collaborators from the HOL communities to help improve Proof General as an interface for HOL provers.


[ << ] [ >> ] [Top] [Contents] [Index] [ ? ]

This document was generated by Erik Martin-Dorel on June 2, 2019 using texi2html 1.82.