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 <23030-0@swan.cl.cam.ac.uk>; Tue, 28 Jul 1992 21:13:13 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA00548;
          Tue, 28 Jul 92 12:59:21 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from leopard.cs.uidaho.edu by ted.cs.uidaho.edu (16.6/1.34) 
          id AA00543; Tue, 28 Jul 92 12:59:15 -0700
Received: by leopard.cs.uidaho.edu (16.7/1.34) id AA00497;
          Tue, 28 Jul 92 12:49:27 -0700
From: hall@edu.uidaho.cs.leopard (Kelly Hall)
Message-Id: <9207281949.AA00497@leopard.cs.uidaho.edu>
Subject: Problems with AKCL HOL HP9000/700
To: info-hol@edu.uidaho.cs.ted
Date: Tue, 28 Jul 92 12:49:27 PDT
Mailer: Elm [revision: 66.33]

Hi all,

Myabe some kind soul could help me with my current problem?  I'm in
the process of building HOL 2.0 on our HP 9000/730.  Now that AKCL
is working (thanks, Albert) I'm having problems with the HOL build.

It seems like there's a problem in the pretty-printer someplace that
is causing AKCL to barf and die.  Here's a transcript:
[---start transcript---]
        echo 'set_search_path[``; `/usr/pkg/hol2/hol/theories/`];;'\
             'load_theory `bool`;;'\
             'lisp `(proclaim (quote (optimize (speed 3))))`;;'\
             'compilet `ml/drul`;;'\
             'quit();;'\
             | hol-lcf

HOL-LCF version 2.0 created 7/24/92
#() : void
Theory bool loaded
() : void
() : void
() : void
GEN_ALL = - : (thm -> thm)
[...stuff deleted...]
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%7515%31 > CONCATENATE
evaluation failed     lisp error
Bye.
*** Error code 1

Stop.
[---Stop transcript---]

I've tried putting the old code back in f-cl.l (the Common Lisp compatibility code)
where 'concat was modified, but I get the same problem.  If I change the Makefile
to compilef (instead of compilet) everything works fine.  I could keep using compilef
but I'll need to modify most of the Makefiles for the libraries, too, and I'd rather
not do that.  Any ideas?

Thanks in advance,
--
Kelly Hall == hall@leopard.cs.uidaho.edu
no disclaimer, no cute quotes