Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
From: rahard@ee.umanitoba.ca (Budi Rahardjo)
Message-Id: <9507160501.AA11153@wine>
Subject: Re: Building HOL88-2.02 on Solaris with GCL-2.1
To: beckerb@cs.ucdavis.edu
Date: Sun, 16 Jul 1995 00:01:28 -0500 (CDT)
Cc: info-hol@leopard.cs.byu.edu
In-Reply-To: <9505120149.AA20209@roma-cafe> from "beckerb@cs.ucdavis.edu" at May 11, 95 06:49:52 pm
Mime-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit

> I've managed to compile GCL and HOL88 without too much difficulty.
> Unfortunately, the resultant HOL executable does not work:
...
>          HOL88 Version 2.02 (SUN4/AKCL), built on 11/5/95
...
> calling 'dl' function sun did not supply..exittingExit 1
> ----------------------------------------------------------------------
> Does anyone have any hints they could provide as to the cause of this
> error?

Here is a solution that I got a while ago from Malcolm Newey.
Maybe it should be in the FAQ?
PS: I also got HOL working on my 386 (SX/16MHz, a slow machine) running Linux. 
It took the machine two (or was it three) days to compile it!

Good luck.

-- budi

----- included messages -----
>From: Malcolm Newey <Malcolm.Newey@cs.anu.edu.au>
>To: brahardj@win.trlabs.ca


Hi Budi,
There are several places in the HOL distribution where `~/` is mentioned.
The one you need to hack out to avoid the problem we are having is
at about line 245 of the Makefile.
Alter it to read       'set_search_path[``; `${Theory}/`];;'\
Maybe the other occurrences lead to other modes of failure, but I have
not tried to uncover them.  (eg in lisp/f-tml.l and ml/gen.ml)

Malcolm


-- 
Budi Rahardjo
<rahard@ee.umanitoba.ca>                 <Budi_Rahardjo@UManitoba.CA>
Electrical and Computer Engineering - University of Manitoba - Canada