Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 4 Nov 1994 07:36:54 +0000 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA02770; Fri, 4 Nov 1994 00:33:06 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from tango.rahul.net by leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA02766; Fri, 4 Nov 1994 00:32:33 -0700 Received: from bolero.rahul.net by tango.rahul.net with SMTP id AA09308 (5.67b8/IDA-1.5 for ); Thu, 3 Nov 1994 23:24:05 -0800 Received: by bolero.rahul.net id AA17797 (5.67b8/IDA-1.5); Thu, 3 Nov 1994 23:24:04 -0800 Date: Thu, 3 Nov 1994 23:24:02 -0800 (PST) From: Bill Hogan Subject: Re: bhogan@bedlam: HOL90 on a PC To: es774@eng.warwick.ac.uk Cc: Jim Grundy , info-hol In-Reply-To: <27283.9411030946@eng.warwick.ac.uk> Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII On Thu, 3 Nov 1994 es774@eng.warwick.ac.uk wrote: > 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 > As an utter newcomer to HOL, I backed away from hol90.6 as soon as I discovered that it departs from HOL as set forth by the documentation on lal.cs.byu.edu in ways that would have made it needlessly difficult to use that documentation. I have since removed hol90.6 from my Linux setup, installed gcl-1.0, and built HOL 2.02. Bill