Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Date: Fri, 25 Feb 94 9:32:33 EST
From: reetz <reetz@ira.uka.de>
To: info-hol@cs.uidaho.edu
Cc: schneide@ira.uka.de, eisen@fzi.de, dehof@ira.uka.de, kropf@ira.uka.de
Subject: HOL90.6 on a PC
Message-Id: <"i80fs2.ira.653:25.01.94.08.32.40"@ira.uka.de>

MOTIVATION

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:

1.) I first tried EDML with a 386-version for MS-DOS. It has no modules and
    no wildcard for exceptions, so it does not meet the requirements of 
    HOL90.6.

2.) I picked yp another ML for MS-DOS somewhere from scandinavia, I think.
    It was even more corish.

3.) I fetched a ML for Windows 3.0. The result of starting it: A Window 
    opened and closed immediately without any error message. I manipulated 
    Windows in every way - nothing worked.

4.) I didn't tried CAML for PC, I must grant, because I was really
    sceptical where its lazy evaluation will produce the same results
    as sml under any circumstances.

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.

6.) Finally I digged out an unsupported port of sml/nj 0.93 for Linux. The 
    only known problem was a bug in System.Directory.getWD(), but one can 
    circumvent it. Just a question of hacking a little bit. So I installed 
    Linux, reserving 100MB Swapspace (due to only 4 MB main memory), fixed the
    getWD-question and started make_hol. The first day (yes, day - look
    at the 4 MB main memory constraint), everything worked just fine. As far 
    as I have seen (I didn't sit the whole day there looking at my PC),
    at least everything from /src/0 was compiled successfully. The next
    day, I found my PC being lost in the software nirvana. After some
    checking, it just seems to be the case that Linux does not use more
    the 16MB Swapspace. I'm really not an expert on Linux, but this
    limit sounds familiar for PC users. However, 20 MB memory are
    clearly not enough to build HOL90. Even 32 MB (i.e. increasing
    my main memory up to 16 MB, Linux will get lost into DMA-trouble
    with my harddisk with more than 16 MB main memory) seems to be
    critical for HOL90, because the SPARC at my university needed
    80 MB heap size, divided it by 2 because of RISC(SPARC)/CISC(486) is still
    40 MB.

FUTURE WORK

I may try to get a mach- or bsd-unix for PC and then try it again, because 
there are supported versions of sml/nj for them. But the only unix-versions 
for free (yes, I even don't want to spend a lot of bucks on operation 
systems) I could found seems to have the same memory limitations as Linux.

:) Ralf

(*****************************************************************************)
(*                                                                           *)
(*  Ralf Reetz                            SFB 358 of the german research     *)
(*  reetz@informatik.uni-karlsruhe.de     society (DFG)                      *)
(*                                        University of Karlsruhe, Germany   *)
(*                                                                           *)
(*                "we prove around in a ring and suppose,                    *)
(*                 the goal sits right in the middle and knows."             *)
(*                                                                           *)
(*****************************************************************************)