Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: des@inmos.co.uk, info-hol@leopard.cs.byu.edu
In-Reply-To: <8049.9411021048@frogland.inmos.co.uk> (message from David Shepherd on Wed, 2 Nov 1994 11:48:39 +0100)
Subject: Re: bhogan@bedlam: HOL90 on a PC
Message-Id: <94Nov2.130228met.8082@sunbroy14.informatik.tu-muenchen.de>
Date: Wed, 2 Nov 1994 13:02:25 +0100


>>   In my opinion it does not matter what version of HOL you are running 
>>   as long as you have plenty of RAM everything runs much faster. I never 
>>   thought it would be possible to run HOL on a system with 8 Meg RAM but 
>>   it is if you use HOL2.02 not HOL90.
>
>back in the days of franz lisp compiled HOL's I'm sure you could manage
>with 4Mbs if really pushed :-)

Maybe somebody should try the experiment of porting hol90 to Moscow ML. 
When Moscow ML was released, I ported gtt (a very small implementation of
the kernel of HOL) to it in an hour or so. To get a useful hol90 port would
take a bit of work, most of it straightforward:

   1. Usage of the ML module system would have to be stripped out.

   2. Parsers for types, terms, theories, and library descriptions would
      have to be hand-written if the bulky implementation of ML-Yacc was 
      not desired.

   3. Automatic prettyprinting of types, terms, and theorems ought to be
      available, but Moscow ML doesn't supply these sorts of hooks (in the
      interest of purity).

   4. Support for quotations would be nice, although Moscow ML doesn't 
      supply them. Probably running it piped through a filter that expands
      quotations out would suffice.


John Harrison has done some work in this vein, using CAML-Light.


Konrad.