Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Message-Id: <14093.9306241539@rough.dcs.ed.ac.uk>
To: info-hol@ted.cs.uidaho.edu
Subject: HOL portability
Date: Thu, 24 Jun 93 16:39:07 +0100
From: Michael Fourman <mikef@dcs.ed.ac.uk>


 Konrad Slind writes:
> I think Larry is not completely precise when he talks of the efficiency
> of PolyML; PolyML is relatively quick at compiling, but is benchmarked
> as being 2 to 3 times slower than SML/NJ when running compiled code.

Oh dear!  When the relative efficiency of HOL88 and HOL90 was being
discussed here a short while ago, some sane commentator pointed out
that it depends what you're doing and what machine you are doing it 
on. The same goes for different ML compilers.

I can certainly find examples of code for which SML/NJ is 2 to 3 times
faster than Poly/ML (reals are handled differently). However,
we use Poly/ML for our undergraduate teaching at Edinburgh because we
believe it performs better on the machines we have available.

Last time we were able to make a direct comparison at AHL, HOL90
performance on our 32Mbyte Sparc machines under Poly and NJ was 
roughly comparable. If Konrad had been able to keep HOL90 compatible 
with *Standard* ML, then users could easily determine what works best 
for them.

It is a pity if HOL90 only works with one particular implementation of
Standard ML, since other implementations (available now or under
development) may be more efficient.

For anyone who doesn't know, I declare an interest: I am a Director of
Abstract Hardware Limited (who develop and market Poly/ML).

Mike

-------------------------------------------------------------------------------
Prof. Michael P. Fourman, Laboratory for Foundations of Computer Science,
University of Edinburgh, Scotland, UK.  email:Michael.Fourman@lfcs.ed.ac.uk