From 390a659861192ebf98811438f61c4f992ecad25a Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Mon, 13 Mar 2000 04:21:14 +0000 Subject: New/updated information files --- hol98/README | 21 +++++++++++++++------ hol98/todo | 16 +++++++++++----- 2 files changed, 26 insertions(+), 11 deletions(-) (limited to 'hol98') diff --git a/hol98/README b/hol98/README index 84e4cc5a..a88902f5 100644 --- a/hol98/README +++ b/hol98/README @@ -4,6 +4,14 @@ Written by David Aspinall. $Id$ +Status: not officially supported yet +Maintainer: volunteer required +HOL version: HOL 98, tested with Taupo 2 +HOL homepage: http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html + +======================================== + + This is a "technology demonstration" of Proof General for HOL 98. It may work with other versions of HOL, but is untested (please let me @@ -12,16 +20,17 @@ know if you try). It has basic script management support, with a little bit of decoration of scripts and output. -There is support for x-symbols, but not using a proper token -language. Try writing "philosophy" ! +There is support for X Symbol, but not using a proper token language. +Try writing "philosophy" ! 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. ------------------- -Note: +------------ + +Notes: There are some problems at the moment. HOL proof scripts often use batch-oriented single step tactic proofs, but Proof General does not @@ -34,8 +43,8 @@ interactive proofs 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. Again, this could be improved by -taking a better parser (e.g. from sml mode). +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. diff --git a/hol98/todo b/hol98/todo index 44179369..359c1195 100644 --- a/hol98/todo +++ b/hol98/todo @@ -1,12 +1,18 @@ -*- mode:outline -*- -* See also ../todo for generic things to do, priority codes. - * Things to do for HOL -====================== -A Problem with displaying long help message: causes loop in PG +See also ../todo for generic things to do, priority codes. + +** A Problem with displaying long help message: causes loop in PG filtering, why? Process also takes a long time to kill off. -B Improve display to strip ugly val it's. +** B Improve display to strip ugly val it and spurious >'s. + +** B Add special markup to improve robustness + +** B Add support for multiple files + +** B Add support for proof by pointing. + -- cgit v1.2.3