Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Fri, 14 May 1993 03:04:37 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA20014;
          Thu, 13 May 93 18:54:43 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from elysium.cs.ucdavis.edu by ted.cs.uidaho.edu (16.6/1.34) 
          id AA20009; Thu, 13 May 93 18:54:38 -0700
Received: by elysium.cs.ucdavis.edu (5.65/UCD.CS.2.3) id AA13438;
          Thu, 13 May 1993 18:54:45 -0700
Date: Thu, 13 May 1993 18:54:45 -0700
From: benson@cs.ucdavis.edu (Gregory D. Benson)
Message-Id: <9305140154.AA13438@elysium.cs.ucdavis.edu>
To: info-hol@ted.cs.uidaho.edu
Subject: Building HOL 2.01 on DEC 5000/240 with AKCL


Hello,

Has anyone successfully built HOL 2.01 on a DECStation 5000/240 running
Ultrix V4.2A and AKCL?  I have been trying on and off for the last couple
of days with no luck.

I have tried AKCL 1-605, 1-609, and 1-615 ?  The closest I get is with
AKCL 1-615, but the make crashes in different places.  It seem to build
HOL-LCF ok, and even BASIC-HOL.  Then it tries to build the theories.
Here is example of where the last build crashed:

=======> basic-hol88 made
cd /usr/home/benson/pkg/hol/theories; rm -f tree.th; /usr/home/benson/pkg/hol/ba
sic-hol < /usr/home/benson/pkg/hol/theories/mk_tree.ml; cd /usr/home/benson/pkg/
hol

BASIC-HOL version 2.01 (MIPS/AKCL) created 12/5/93

#############################() : void

###Theory list loaded
() : void

#########evaluation failed     theorem -- list_INDUCT not found on theory list
Bye.
*** Error code 1

Stop.
*** Error code 1

Stop.


I have installed the new f-freadth.l.  Any help would be appreciated.

Greg Benson
Department of Computer Science
University of California, Davis
benson@cs.ucdavis.edu