Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
From: akarkare@edu.wsu.eecs.yoda (Ashish Karkare)
Message-Id: <9201211841.AA16368@yoda.eecs.wsu.edu>
Subject: Installing HOL.
To: info-hol@edu.uidaho.cs.ted
Date: Tue, 21 Jan 92 10:41:10 PST

Hello,

I have been trying to install  HOL on a DEC 3100 running Ultrix.
I am using Ibuki Common Lisp for compiling the HOL source. However, the
make crashes at some point for reasons that I can't figure out.

Has anyone out there tried to install HOL in this environment? I would
appreciate any help in getting HOL up and running.

I have enclosed a transcript of the relevant make session.

Thanks in anticipation.

Ashish.

------------------------Make transcript------------------------------
Finished compiling lisp/f-ol-net.l.

>Bye.

IBUKI Common Lisp  Version 2 release 01.027.

>Loading lisp/mk-ml.o
Loading lisp/f-cl.o
Finished loading lisp/f-cl.o
Loading lisp/f-system.o
Finished loading lisp/f-system.o
Loading lisp/f-constants.o
Finished loading lisp/f-constants.o
Loading lisp/f-site.o
Finished loading lisp/f-site.o
Loading lisp/f-gp.o
Finished loading lisp/f-gp.o
Loading lisp/f-parser.o
Finished loading lisp/f-parser.o
Loading lisp/f-parsml.o
Finished loading lisp/f-parsml.o
Loading lisp/f-mlprin.o
Finished loading lisp/f-mlprin.o
Loading lisp/f-typeml.o
Finished loading lisp/f-typeml.o
Loading lisp/f-dml.o
Finished loading lisp/f-dml.o
Loading lisp/f-format.o
Finished loading lisp/f-format.o
Loading lisp/f-tran.o
Finished loading lisp/f-tran.o
Loading lisp/f-iox-stand.o
Finished loading lisp/f-iox-stand.o
Loading lisp/f-writml.o
Finished loading lisp/f-writml.o
Loading lisp/f-tml.o
Finished loading lisp/f-tml.o
Loading lisp/f-lis.o
Finished loading lisp/f-lis.o
Loading lisp/f-ol-rec.o
Finished loading lisp/f-ol-rec.o
Loading lisp/f-help.o
Finished loading lisp/f-help.o
Finished loading lisp/mk-ml.o
0

>Loading lisp/mk-hol-lcf.o
Loading lisp/f-parsol.o
Finished loading lisp/f-parsol.o
Loading lisp/f-typeol.o
Finished loading lisp/f-typeol.o
Loading lisp/f-help.o
Finished loading lisp/f-help.o
Loading lisp/f-format.o
Finished loading lisp/f-format.o
Loading lisp/f-writol.o
Finished loading lisp/f-writol.o
Loading lisp/f-thyfns.o
Finished loading lisp/f-thyfns.o
Loading lisp/f-freadth.o
Warning:
lisp/f-freadth.l is redefining function THY-READ
>>Error: The variable |256| is unbound.
 NIL                          (IHS[13])
Arg 0: (MAKE-STRING |256|)
Arg 1: #<compiled-function MAKE-STRING>
Restart options (Type :C <number>):
     0: Provide a value to store as the value of |256|
     1: Retry getting the value of |256|
:Q,  2: Lisp Top Level
 Version 201  Delta 27
 Type :H for a list of debugger commands.
 ->
"HOL-LCF"
 ->
""
 ->
"2.0"
 ->
NIL
 ->
HOL-LCF version 2.0 created 16/1/92

#
mem = - : (* -> * list -> bool)

map = - : ((* -> **) -> * list -> ** list)

exists = - : ((* -> bool) -> * list -> bool)

forall = - : ((* -> bool) -> * list -> bool)

find = - : ((* -> bool) -> * list -> *)

tryfind = - : ((* -> **) -> * list -> **)

filter = - : ((* -> bool) -> * list -> * list)

mapfilter = - : ((* -> **) -> * list -> ** list)

rev_itlist = - : ((* -> ** -> **) -> * list -> ** -> **)

compiling = false : bool

compiling_stack = [] : bool list

load = - : ((string # bool) -> void)

compile = - : ((string # bool) -> void)

Calling Lisp compiler

File ml/ml-curry compiled
() : void
>>Error: Signal 11 caught.
The internal memory may be broken.
You should check the signal and exit from Lisp.
 NIL                          (IHS[35])
Restart options (Type :C <number>):
:Q,  0: Debugger Level 1
     1: Provide a value to store as the value of |256|
     2: Retry getting the value of |256|
:Q!, 3: Lisp Top Level
 ->>>>Error: The variable QUIT is unbound.
 EVALHOOK                     (IHS[54])
Arg 0: QUIT
Arg 1: NIL
Arg 2: NIL
Arg 3: NIL
Restart options (Type :C <number>):
     0: Provide a value to store as the value of QUIT
     1: Retry getting the value of QUIT
:Q,  2: Debugger Level 2
     3: Debugger Level 1
     4: Provide a value to store as the value of |256|
     5: Retry getting the value of |256|
:Q!, 6: Lisp Top Level
 ->>>
NIL