Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2);
          Mon, 14 Sep 1992 20:10:51 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA00608;
          Mon, 14 Sep 92 09:47:39 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from ens.ens-lyon.fr by ted.cs.uidaho.edu (16.6/1.34) id AA00603;
          Mon, 14 Sep 92 09:47:19 -0700
Received: from lip.ens-lyon.fr by ens.ens-lyon.fr (4.1/SMI-4.1) id AA02436;
          Mon, 14 Sep 92 18:45:53 +0200
Received: from chartreuse.ens-lyon.fr by lip.ens-lyon.fr (4.1/SMI-4.1) 
          id AA20456; Mon, 14 Sep 92 18:45:51 +0200
Date: Mon, 14 Sep 92 18:45:51 +0200
From: Laurent.Mounier@fr.ens-lyon.lip (Laurent Mounier)
Message-Id: <9209141645.AA20456@lip.ens-lyon.fr>
X-Mailer: Mail User's Shell (6.4 2/14/89)
To: info-hol@edu.uidaho.cs.ted
Subject: Problem when building hol from AKCL

Hi, 

I am attempting to build the HOL system using AKCL 1.605 on
a Sparc machine, and I get a problem when it tries to start compiling the
built-in theories of basic-hol. Here is what happens:


	... [stuff deleted] ...


cd /home/lip/lmounier/Hol/Distribution/hol_88/theories; rm -f PPLAMB.th;\
/home/lip/lmounier/Hol/Distribution/hol_88/hol-lcf < /home/lip/lmounier/Hol/Distribution/hol_88/theories/mk_PPLAMB.ml;\
cd /home/lip/lmounier/Hol/Distribution/hol_88

HOL-LCF version 2.0 created 14/9/92

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

##() : void

##() : void

##Bye.
=======> theory PPLAMB built
cd /home/lip/lmounier/Hol/Distribution/hol_88/theories; rm -f bool.th;\
/home/lip/lmounier/Hol/Distribution/hol_88/hol-lcf < /home/lip/lmounier/Hol/Distribution/hol_88/theories/mk_bool.ml;\
cd /home/lip/lmounier/Hol/Distribution/hol_88

HOL-LCF version 2.0 created 14/9/92

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

##
Error: (PARENTS) cannot be coerced to a string.
Fast links are on: do (use-fast-links nil) for debugging
Error signalled by FUNCALL.
Backtrace:  > funcall > lambda > ml-new_parent > funcall
evaluation failed     new_parent -- PPLAMB theory damaged
Bye.
*** Error code 1
make: Fatal error: Command failed for target `/home/lip/lmounier/Hol/Distribution/hol_88/theories/bool.th'
Current working directory /tmp_mnt/home/lip/lmounier/Hol/Distribution/hol_88
*** Error code 1
make: Fatal error: Command failed for target `all'

And here is the code of the file PPLAMB.th I got just before the error occurs :

(SETQ %THEORYDATA (QUOTE ((PARENTS) (TYPES (2 . |fun|)) (NAMETYPES) (OPERATORS) (PAIRED-INFIXES) (CURRIED-INFIXES) (PREDICATES) (VERSION . "2.0") (STAMP . 2925474965)))) 

(SETQ %THEOREMS (QUOTE ((SHARETYPES 0) (AXIOM) (FACT)))) 

All the sources I use (for HOL and AKCL) have been transfered from 
the host gannet.cl.cam.ac.uk.

Any help would be greatly appreciated !

Laurent Mounier.