Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Date: Tue, 27 Sep 94 17:35:01 CST
From: jug@itd.dsto.gov.au (Jim Grundy)
Message-Id: <9409270805.AA27739@itd0.dsto.gov.au>
To: reetz@ira.uka.de
Subject: RE: HOL90 on PC / Moscow ML
In-Reply-To: Mail from 'info-hol-request@lal.cs.byu.edu' dated: Tue, 27 Sep 94 8:46:47 EST
Cc: info-hol@lal.cs.byu.edu

Hmmm

> >to get it.  Then ftp down the latest HOL90 and make it using explicit 
> >path names rather than letting it figure out the current directory for
> >itsself

> In my experience, there is also a problem with loading libraries. I
> finally did it manually once and saved it into an image file.

I haven't had any problem loading libraries in my build.  Perhaps you are
using relative pathnames rather than absolute ones in the library definition.
(I don't know if that would do it, I am just guessing).

> As far as I know, Moscow ML does currently not have modules, and it is
> expected take another year to get modules implemented in Moscow ML.
> Without modules, I personally can`t see how to get a HOL90.x Version
> on Moscow ML in an easy way (see faq comp.lang.ml).

[rumors on]
I heard that Konrad and John had a CAML (also sans modules) port of the "core"
of HOL90.   I don't know how small a fraction the "core" is though.
[rumors off]

> >Be warned, most fast PCs  will run HOL88 quite well, but few peole 
> >(including me with 20M of RAM) have a PC with enough memory to run HOL90
> >effectively
> 
> I`ve 20Mb of RAM, too, but I'm still unsatisfied. I recommend even more
> memory, if you are doing ``big'' things, e.g. heavily use of libraries,...
> Regarding speed, I own an outdated 486/33Mhz and that`s roughly the same
> as SPARC IPX, so IMHO speed is not the problem.

I didn't construct that sentence very well.  What I meant to say is that
even with 20M of RAM I (like Ralph) am very unsatisfied with the performance
of the HOL90.  Its not the CPU, the CPU don't get a chance, the system thrashes
like crazy when loading a big library. I don't know how much memory is enough,
but its more thatn 20 (I think the next step up for most PCs is 32 - anyone
with 32 got any comments - 32 better be enough because thats all you can fit
in my machine - not that I can afford it).

Jim