Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
To: hishikaw@unity.ncsu.edu
Cc: info-hol@leopard.cs.byu.edu, tfm@dcs.gla.ac.uk
Subject: Re: Is anybody know how to install HOL via Lucid Lisp ?
In-Reply-To: Your message of "Mon, 11 Dec 1995 18:23:31 EST." <199512112323.SAA14539@dialup.math.ncsu.edu>
Date: Thu, 14 Dec 1995 16:08:19 +0000
From: Tom Melham <tfm@dcs.gla.ac.uk>
Message-Id: <E0tQH6P-0008MY-00@bescot.cl.cam.ac.uk>


>         Hello. I am a new member of this HOL user community. From the first
>  mail, ...
> ... My problem is "Lucid Lisp" (I think). For building "hol-lcf" ...

One of the first things to try is a total rebuild from a clean
directory.  Do "make clobber" first, and then try a rebuild.
But beyond that all I can suggest is that Phil Windley
(windley@leopard.cs.byu.edu) has had quite a bit of experience
with Lucid Lisp (see, for example, the attached message).  You
might ask him.

However, if you're a beginning user, I really would suggest
using the SML version (hol90).  This will be undergoing a lot
of new development over the next little while, with some
really very useful new tools -- as well, perhaps, as some
experimental features that might be interesting for new
research.

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

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
=====================================================================