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; Wed, 2 Nov 1994 22:46:39 +0000
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA00933;
          Wed, 2 Nov 1994 15:31:44 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from itd0.dsto.gov.au by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA00929;
          Wed, 2 Nov 1994 15:31:35 -0700
Received: from tcs22.itd (tcs22.dsto.gov.au) by itd0.dsto.gov.au (4.1/SMI-4.1) 
          id AA07588; Thu, 3 Nov 94 08:52:41 DST
Date: Thu, 3 Nov 94 08:52:41 DST
From: jug@itd.dsto.gov.au (Jim Grundy)
Message-Id: <9411022222.AA07588@itd0.dsto.gov.au>
To: info-hol@leopard.cs.byu.edu
Subject: Re: bhogan@bedlam: HOL90 on a PC
In-Reply-To: Mail from 'es774@eng.warwick.ac.uk' dated: Wed, 2 Nov 94 9:51:23 GMT

I wrote:
> > Performance wise, HOL2.02 is definitely faster than HOL90, but both are
> > acceptable.

Karim wrote:
> It would be interesting to know the hardware configuration of your PC.

Its a 486DX2-66 with 20Mb of RAM and 2.5Mb of disk cache.  It started life
with 16Mb of RAM and 0.5Mb of disk cache, and I've been adding more memory
in an attempt to increase performance, so far with out making very much
difference.

When I said the performance as acceptable, I should state that I am also
a patient fellow.  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.  Most of the other
stuff is just me typing simple commands at it, and it evaluating them. I can't
type in that much stuff in one go, so it can only thrash so much.  I would
like to see a Linux SML port with the garbage flushing that des described,
it could be a big help.

Jim

