Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Thu, 3 Nov 1994 10:01:08 +0000
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA11661;
          Thu, 3 Nov 1994 02:54:29 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from eagle.eng.warwick.ac.uk by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA11656;
          Thu, 3 Nov 1994 02:54:19 -0700
Received: from eng.warwick.ac.uk by eagle.eng.warwick.ac.uk with SMTP 
          id JAA21253; Thu, 3 Nov 1994 09:46:14 GMT
From: es774@eng.warwick.ac.uk
Message-Id: <27283.9411030946@eng.warwick.ac.uk>
Subject: Re: bhogan@bedlam: HOL90 on a PC
To: jug@itd.dsto.gov.au (Jim Grundy)
Date: Thu, 3 Nov 94 9:46:13 GMT
Cc: info-hol@leopard.cs.byu.edu (info-hol)
In-Reply-To: <9411022222.AA07588@itd0.dsto.gov.au>; from "Jim Grundy" at Nov 3, 94 8:52 am
X-Mailer: ELM [version 2.3 PL8]

Jim wrote:

>I think HOL90 is quite allright for such things except >when you are building HOL90 or loading a library, or doing an exportML, these
> are the things that throw my machine into a thrash frenzy.

Actually I have tried building HOL90 on FreeBSD and after five hours of
disk swapping it only build basic-hol. I am very happy with the performance of
HOL2.02 on Linux despite the fact that I only have 8 Megs of RAM.

Karim