Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: David Shepherd <des@uk.co.inmos>
Message-Id: <2480.9301220943@frogland.inmos.co.uk>
Subject: Re: Conversion from HOL88 to HOL90
To: info-hol@edu.uidaho.cs.ted (info-hol mailing list)
Date: Fri, 22 Jan 1993 09:43:01 +0000 (GMT)
In-Reply-To: <9301212233.AA10731@maui.cs.ucla.edu> from "chou@cs.ucla.edu" at Jan 21, 93 02:33:54 pm
Content-Type: text
Content-Length: 1526

chou@cs.ucla.edu has said:
> 
> Seeing all the great benchmark figures about HOL90 and going to
> get bigger memory on my machine, I am rather tempted to switch
> to HOL90.  I'd like to hear about the experience of people who
> had done so.  How hard is it to convert from HOL88 to HOL90?
> Are there good reasons for doing so or not doing so?  And I
> am curious how widely used is HOL90 now, compared with HOL88.

WARNING: my benchmark figures turn  out to be highly innacurate
as I was comparing hol90 with hol88 v1.12 - there is a significant
performance gain between hol88 v1.12 and hol88 v2 which almost
matches the hol90 speed up I showed. Also, I turns out that AKCL
performance is much better now when John van Tassels allocation
directives are included (in ftp.cl.cam.ac.uk:hvg/contrib/AKCL????).

I am trying to sort out this situtation to get a more credible
set of figures! Until then I wouldn't make any switch on the
basis of what I have said so far!

Sorry for any confusion that I may have caused.

BTW. The one solid fact that I can give seems to be that if you're still
using a hol88 version before v2 (v2 was also once known as v1.13 I think)
then there is a significant benefit by doing so.

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		Life doesn't imitate art, it imitates bad television
						      - Husbands and Wives