Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 28 Mar 1995 05:59:54 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA218556216;
          Mon, 27 Mar 1995 21:50:16 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Received: from ipso.ips.oz.au by leopard.cs.byu.edu 
          with SMTP (1.37.109.15/16.2) id AA218476180;
          Mon, 27 Mar 1995 21:49:40 -0700
Received: from titan.UUCP by ipso.ips.oz.au with UUCP 5.65c/IDA-1.4.4/IPS-1.3;
          id AA21214;
          Tue, 28 Mar 1995 14:47:24 +1000 (from titan!renneber@sun1.alcatel.oz.AU 
          for info-hol@leopard.cs.byu.edu)
Received: from sun1 by titan.alcatel.oz.AU (5.61+/1.34:950217) id AA12093;
          Tue, 28 Mar 95 10:55:08 +1000
Received: from ipc2.alcatel.oz.au by sun1.alcatel.oz.au (4.1/SMI-4.1) 
          id AA07473; Tue, 28 Mar 95 10:55:12 EST
Date: Tue, 28 Mar 95 10:55:12 EST
From: renneber@sun1.alcatel.oz.AU (Carl Renneberg)
Message-Id: <9503280055.AA07473@sun1.alcatel.oz.au>
To: info-hol@leopard.cs.byu.edu
Subject: Re: lisps for HOL88


Malcolm Newey wrote:

> ...
> If you use HOL88, you might be interested in rebuilding it on your machine
> using gcl-1.1 and sharing your experience.  As a group we don't yet have
> a database of who uses which HOL and what machines have been successfully
> used.
> ...

In January this year I used gcl-1.1 to build HOL88 version 2.02 on my 486 PC
(Linux kernel 1.1.18, from the Slackware 2.0 distribution; 32 MB main memory,
and 16 MB swap space).

I seem to remember that the build took about 17 hours (but I can't be sure -
it may have been closer to 12 hours).

gcl-1.1 itself installs very easily. I compiled it with gcc, which comes with
Slackware.

After installation, you'll find that /usr/local/bin/gcl is a script file, and
the actual program lies in a subdirectory. Before building HOL, I edited its
Makefile so that it referred to akcl as the Lisp, then copied
/usr/local/bin/gcl to /usr/local/bin/akcl.

After I RTFM and edited the HOL Makefile accordingly, the HOL build and
installation proved to be problem-free.

Carl