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.0) 
          id <00219-0@swan.cl.cam.ac.uk>; Mon, 6 Jul 1992 11:37:55 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA01569;
          Mon, 6 Jul 92 03:26:52 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from [130.89.10.247] by ted.cs.uidaho.edu (16.6/1.34) id AA01564;
          Mon, 6 Jul 92 03:26:41 -0700
Received: from perseus.cs.utwente.nl by utrhcs.cs.utwente.nl (4.1/RBCS-2.3mx) 
          id AA06433; Mon, 6 Jul 92 12:27:41 +0200
Received: from utis143.cs.utwente.nl by perseus.cs.utwente.nl (4.1/RBCS-2.0) 
          id AA12424; Mon, 6 Jul 92 12:27:39 +0200
Date: Mon, 6 Jul 92 12:27:39 +0200
From: vdvoort@nl.utwente.cs (Mark van de Voort)
Message-Id: <9207061027.AA12424@perseus.cs.utwente.nl>
To: info-hol@edu.uidaho.cs.ted
Subject: building HOL on SUN4/AKCL

I' m trying to build HOL on a SUN-4 using AKCL-1.615.

This fails resulting in the error-message given below. I seem to 
recall a discussion about what version of AKCL to use, as higher
versions wouldn't compile correctly. I do not know what version
to use.

Can anyone help me out on this?

Thanks in advance,

Mark.

Transcript of session:
|>  
|>  echo 'set_search_path[``; `/home/fp/vdvoort/tp/sparchol/theories/`];;'\
|>       'load_theory `bool`;;'\
|>       'compilet `ml/drul`;;'\
|>       'quit();;'\
|>       | hol-lcf
|>  
|>  HOL-LCF version 2.0 created 6/7/92
|>  
|>  #() : void
|>  
|>  Theory bool loaded
|>  () : void
|>  
|>  
|>  () : void
|>  
|>  GEN_ALL = - : (thm -> thm)
|>  
|>  DISCH_ALL = - : (thm -> thm)
|>  
|>  SPEC_VAR = - : (thm -> (term # thm))
|>  
|>  UNDISCH_ALL = - : (thm -> thm)
|>  
|>  SPEC_ALL = - : (thm -> thm)
|>  
|>  PROVE_HYP = - : (thm -> thm -> thm)
|>  
|>  CONJ_PAIR = - : (thm -> (thm # thm))
|>  
|>  LIST_CONJ = - : (thm list -> thm)
|>  
|>  CONJ_LIST = - : (int -> thm -> thm list)
|>  
|>  CONJUNCTS = - : (thm -> thm list)
|>  
|>  BODY_CONJUNCTS = - : (thm -> thm list)
|>  
|>  IMP_CANON = - : (thm -> thm list)
|>  
|>  LIST_MP = - : (thm list -> thm -> thm)
|>  
|>  CONTRAPOS = - : (thm -> thm)
|>  
|>  DISJ_IMP = - : (thm -> thm)
|>  
|>  IMP_ELIM = - : (thm -> thm)
|>  
|>  NOT_CLAUSES = |- (!t. ~~t = t) /\ (~T = F) /\ (~F = T)
|>  
|>  DISJ_CASES_UNION = - : (thm -> thm -> thm -> thm)
|>  
|>  EQ_REFL = |- !x. x = x
|>  
|>  REFL_CLAUSE = |- !x. (x = x) = T
|>  
|>  EQ_SYM = |- !x y. (x = y) ==> (y = x)
|>  
|>  EQ_SYM_EQ = |- !x y. (x = y) = (y = x)
|>  
|>  EQ_EXT = |- !f g. (!x. f x = g x) ==> (f = g)
|>  
|>  EQ_TRANS = |- !x y z. (x = y) /\ (y = z) ==> (x = z)
|>  
|>  BOOL_EQ_DISTINCT = |- ~(T = F) /\ ~(F = T)
|>  
|>  EQ_CLAUSES = 
|>  |- !t.
|>  
|>  Error: CONCATENATE [or a callee] requires less than sixty-eight arguments.
|>  Fast links are on: do (use-fast-links nil) for debugging
|>  Error signalled by CONCATENATE.
|>  Backtrace:  > funcall > lambda > fun%3666%82 > CONCATENATE
|>  evaluation failed     lisp error
|>  Bye.
|>  *** Error code 1
|>  make: Fatal error: Command failed for target `ml/drul_ml.o'
|>  Current working directory /tmp_mnt/home/fp/vdvoort/tp/sparchol
|>  *** Error code 1
|>  make: Fatal error: Command failed for target `all'