Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <3497.9409270922@frogland.inmos.co.uk>
Subject: Re: HOL90 on PC / Moscow ML
To: reetz@ira.uka.de (reetz)
Date: Tue, 27 Sep 1994 10:22:34 +0100 (BST)
Cc: info-hol@lal.cs.byu.edu
In-Reply-To: <"i80fs2.ira.275:27.09.94.07.46.53"@ira.uka.de> from "reetz" at Sep 27, 94 08:46:47 am
Content-Type: text
Content-Length: 3358

reetz has said:
> >There are also CAML and Moscow ML ports for Linux, it would be nice to see
> >a re-implementation of HOL90 in one of these light-weight MLs.
> 
> 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`ve heard that a beta-version of SML/NJ is now running under Windows (NT?).
> That might be an alternative for people who do not want to have DOS/Windows
> AND Linux on their PC (as me ;-)
> [rumors off]

There's already a version of SML/NJ v93 that runs under OS/2.

I had a go at compiling HOL under this when it first came out about a
year ago. Things seemed to be working, but very very slowly as I only
have 8Mb on my PC at home and it was swapping constantly so that the build
was taking 24 hours (I soon abandoned the idea after getting as far
as the "proof of concept" stage!). Also, there were some problems with
HOL90 using some of the system interface bits that weren't
fully implemented. I don't think I ever had the patience to complete
the build (I gave up half way through reproving the basic theories :-)
as the 24 hour run/debug/rerun cycle was a bit much!

Since then there's been a second release of the OS/2 SML which, I seem
to think, addresses some of these problems. The run time system uses some
trick developed for the MACH port to prevent OS/2's VM system swapping
as much + lots of the missing bits have been filled in.

> >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

This is the real problem with anything using SML/NJ ... it needs huge
amounts of memory. BTW, I can remember being shocked at how much memory
HOL88 needed when I moved from Franz Lisp to AKCL or ACL as well!

> 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.


> 
> Ralf
> 
> (**************************************************************)
> (*                                                            *)
> (*  Ralf Reetz                                                *)
> (*                                                            *)
> (*  University of Karlsruhe                                   *)
> (*  Institut fuer Rechnerentwurf und Fehlertoleranz           *)
> (*  76128 Karlsruhe, Zirkel 2, Postfach 6980, Germany         *)
> (*                                                            *)
> (*  e-mail: reetz@ira.uka.de                                  *)
> (*  WWW:    http://goethe.ira.uka.de/people/reetz/reetz.html  *)
> (*                                                            *)
> (**************************************************************)
> 

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 638
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"I  am  not  a  nut      ---      I  am  a  human  being."