Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Date: Wed, 2 Nov 94 09:50:46 DST
From: jug@itd.dsto.gov.au (Jim Grundy)
Message-Id: <9411012320.AA16776@itd0.dsto.gov.au>
To: info-hol@leopard.cs.byu.edu
Subject: Re: bhogan@bedlam: HOL90 on a PC
In-Reply-To: Mail from 'info-hol-request@lal.cs.byu.edu' dated: Tue, 1 Nov 1994 11:23:58 -0500

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.

There was one tiny problem with HOL90 in that the sml for Linux I found has
a bug where the getwd command does not work, so you have to pass the pathname
to the make process rather than letting it work it out for itsself.  Its not
much of a problem really, and it doesn't come up again once the system is
built. Does anyone know if this has been fixed in a later version of SML for
Linux?

Performance wise, HOL2.02 is definitely faster than HOL90, but both are
acceptable.  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
the library loading mechanism so that it works much faster on small memory
machines.  In the mean time, you can save your self a lot of bother by 
using exportML to save an image of the system with your favourite libraries
preloaded.

So,... my advice for which system to run on a PC would be to wait for HOL90.7
Why HOL90?
    Because I got the impression we were hoping the community will adopt it
    as the standard.
Why wait?
    Because the slowness of library loading in HOL90.6 is severe, and with 
    any luck it won't be a long wait.

Just my opinions

Jim