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; Wed, 1 Jun 1994 18:51:28 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA18024;
          Wed, 1 Jun 1994 11:29:20 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from hope.twu.ca by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) 
          id AA18019; Wed, 1 Jun 1994 11:29:14 -0600
Received: by hope.twu.ca (4.0/SONY-4.0MX) id AA10672; Wed, 1 Jun 94 10:26:21 PDT
Date: Wed, 1 Jun 94 10:26:21 PDT
From: Benjamin Yu <byu@twu.ca>
Message-Id: <9406011726.AA10672@hope.twu.ca>
To: info-hol@leopard.cs.byu.edu
Subject: Linux and HOL

Hi all, I am new to HOL and am trying to install HOL on Linux.  I got
AKCL running and even built hol-lcf.  But I just cannot build basic-hol
and hol.  Can someone help me with the following questions:

1) Has anyone run HOL on Linux?
2) I can't make BASIC-HOL.th and from the Makefile, I don't see how this 
   is made but this is needed in building basic-hol.  Also I cannot generate
   the ml/*.o files needed for basic-hol.  Is hol-lcf responsible for 
   generating the ml/*.o files for basic-hol?  (More specifically, from 
   the Makefile, does 'compilet' generate .o files?  If so, and my hol-lcf 
   is not doing that, what could be wrong?

Thanks for all your help!
Dr. B. (Benjamin) Yu                              Trinity Western University
Assistant Professor                               7600 Glover Road
Department of Mathematical Science                Langley, B.C.
email: byu@twu.ca   phone: 888-7511 (ext. 2270)   Canada V3A 6H4