Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <7993.9403021015@frogland.inmos.co.uk>
Subject: HOL90.6 on a PC
To: info-hol@cs.uidaho.edu (info-hol mailing list)
Date: Wed, 2 Mar 1994 10:15:00 +0000 (GMT)
Content-Type: text
Content-Length: 2003

reetz has said:
> Dear all,
> I want to report about unsuccessfully trying to get HOL90.6 running on my
> (private) PC with 486 processor, 4MB main memory and 420MB Harddisk. Someone
> might ask whether it makes any sense to run HOL90 with 4MB main memory on
> a PC. First, I would like know something like |-?HOL90.it_runs_on_a_pc HOL90
> before I spend my hard--earned bucks on memory. Second, I can't afford to
> buy a workstation. Third, sometimes it might be useful to be able to work
> at home, too. Maybe somebody else is interested in this topic and wants to 
> share her/his experiences.
> 
> RESULTS
> 
> The biggest problem seemed to be getting an implementation of SML, which
> is good enough for compiling HOL90. That's what I have seen so far:
> 
> 5.) A student here got an unsupported port of sml/nj 0.93 for OS/2. He ran 
>     into serious problems with / and \ within filenames. There seemed to
>     be a lot of confusion with the naming convention used by HOL90
>     (i.e. unix) and used by OS/2. He couldn't fix the problem up to now. So I
>     didn't want to buy an OS/2 on my own.

I run OS/2 on my PC at home and grabbed this SML "port" and had a go at
compiling up hol90. I have 8Mb of memory which is grossly too small so
the system spent all its time swapping! As you mention I had some
problems with sorting out \'s and /'s but after a few runs and
correction of problems that I ran up against (at several hours a run!)
I eventually managed to get as far as dumping hol90.01 and it was
starting to rebuild theories when I decided that I'd demonstrated that
it was (a) possible, but (b) not at all desirable in 8Mb memory.
If/when I decide to upgrade to 16Mb I might have another look!

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