Return-Path: Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <14962-0@swan.cl.cam.ac.uk>; Wed, 22 Jan 1992 09:40:13 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA20014; Wed, 22 Jan 92 01:27:54 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA20010; Wed, 22 Jan 92 01:27:39 -0800 Received: from guillemot.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <14652-0@swan.cl.cam.ac.uk>; Wed, 22 Jan 1992 09:29:28 +0000 To: akarkare@edu.wsu.eecs.yoda (Ashish Karkare) Cc: info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl Subject: Re: Installing HOL. In-Reply-To: Your message of Tue, 21 Jan 92 10:41:10 -0800. <9201211841.AA16368@yoda.eecs.wsu.edu> Date: Wed, 22 Jan 92 09:29:25 +0000 From: Tom.Melham@uk.ac.cam.cl Message-Id: <"swan.cl.ca.654:22.00.92.09.29.30"@cl.cam.ac.uk> > 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. I have successfully built HOL using Ibuki. It requires some minor changes to the lisp sources, which I will post soon. Tom