blob: 8462763cbbea43b4fc8f703d9134de74c9e94402 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
HOL Proof General, for HOL98.
Written by David Aspinall.
Status: not officially supported yet
Maintainer: volunteer required
HOL version: HOL4/HOL98, tested with HOL 4 Kananaskis 2
HOL homepage: http://hol.sourceforge.net
========================================
This is a "technology demonstration" of Proof General for HOL4.
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 X Symbol, but not using a proper token language.
I have written this in the hope that somebody from the HOL 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$
|
