Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: es774@eng.warwick.ac.uk
Message-Id: <17102.9411020951@eng.warwick.ac.uk>
Subject: Re: bhogan@bedlam: HOL90 on a PC
To: jug@itd.dsto.gov.au (Jim Grundy)
Date: Wed, 2 Nov 94 9:51:23 GMT
Cc: info-hol@leopard.cs.byu.edu (info-hol)
In-Reply-To: <9411012320.AA16776@itd0.dsto.gov.au>; from "Jim Grundy" at Nov 2, 94 9:50 am

>
> Hi
>
> I'd just like to add my own opinions to the HOL for PC's discussion.  I am
> running both HOL90.6 and HOL2.02 on my PC with Linux.  They both built
> very easily.  For HOL2.02, I used the last verion of AKCL which I understand
> is now gcl.
.........................


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

It would be interesting to know the hardware configuration of your PC. What
Megs of RAM it has? Is it a 486 or pentium machine. I have tried building
HOL90 on FreeBSD 1.1.5.1 using SML 93 and found it much too slow. The SML
93 runtime system has been simplified at expense of larger memory requirement.
I also found that under FreeBSD hol2.02 is faster than under Linux. I believe
FreeBSD kernel is more optimised to run this sort of application.

> The singular exeption to this is that loading libraries under
> HOL90 is much much to slow.  However, don't be discouraged.  HOL90.7 is
> (hopefully) just around the corner, and Konrad tells me that he has modified

  In my opinion it does not matter what version of HOL you are running as long
as you have plenty of RAM everything runs much faster. I never thought it
would be possible to run HOL on a system with 8 Meg RAM but it is if you
use HOL2.02 not HOL90.

Karim


>