Message-Id: <9103160116.AA05051@cheetah.cs.uidaho.edu>
To: info-hol@edu.uidaho.cs.ted
Cc: John Van Tassel <jvt@uk.co.sri>
Subject: HOL112 fix for Lucid CL
Date: Fri, 15 Mar 91 17:16:52 -0800
From: Phil Windley <windley@edu.uidaho.cs.cheetah>


There are several problems with the original distribution of HOL 1.12 when
compiled using Lucid CL 3.0 and above.  The most serious was that it
couldn't read theories (after all, what good is a theorem prover that can't
read theories? ;-).  Other problems: (1) didn't correctly read and compile
files in the ml directory, (2) quit is already defined in Lucid and
redefining it broke it, (3) the Makefile ALWAYS rebuilt everything,
regardless.

As far as I know, these problems only occur when using Lucid CL.  There is
no need to get either the patch or a new version if you have 1.12 and it
compiled without problems.  

I have done the following:

1.) The distribution on CS.UIDAHO.EDU has been patched so that it will work
with Lucid CL.  I used compiler switches whereever possible so it shouldn't
break anything else.  If it does, please let me know as soon as possible.
I only have Lucid and AKCL available to me, so I can't test it on
everything. 

2.) The three files that have been patched (Makefile, lisp/f-cl.l, and
lisp/f-freadth.l) are in a compressed tar file called hol.fix.tar.Z.
Untarring this file in the same directory that holds the Makefile will
patch your distribution.  You only need to patch the distribution if you
got it before today and had problems compiling it.  You might want to save
the originals before you apply the patch (no guaratees here ;-).

If you have any further problems, let me know;  I'll try to fix what I can.
After all, we are a *valued added retailer*.

--phil--

Phil Windley                          |  windley@cs.uidaho.edu
Department of Computer Science        |
University of Idaho                   |  Phone: 208.885.6501  
Moscow, ID 83843                      |  Fax:   208.885.6645