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: <3682.9408020837@frogland.inmos.co.uk>
Subject: Re: HOL90 library loading
To: info-hol@cs.uidaho.edu (info-hol mailing list)
Date: Tue, 2 Aug 1994 09:37:26 +0100 (BST)
In-Reply-To: <"i80fs2.ira.687:02.07.94.07.13.57"@ira.uka.de> from "reetz" at Aug 2, 94 09:13:54 am
Content-Type: text
Content-Length: 1698

reetz has said:
  [[ question on library loading in hol90 vs hol88 ]]

> >Why all the warnings and GC's ?
>  
> Where is nothing unusual with it. GC are part of
> SML/NJ 0.93 and have nothing to do with HOL90.6.
> To put it frankly, SML/NJ 0.93 is ``well-known''
> for its GC in any sense.
>  
> I'm not familiar with classic ML, ....

I think you are missing the real reason here! There is a big difference
between hol88 and hol90 in that the lisp based hol88's are able to load
pre-compiled code while in the SML based hol90 you can't. As a result,
when you load a library the theories get loaded as before but the code
has to be compiled as it loads. This means (i) loading libraries is
much slower - you have to compile as well as load, and (ii) you can get
a whole load of diagnostic messages from the compiler.

On consequence of this is that on a slow machine (e.g. SparcStation 1)
its a real pain to have to load libraries - it can add 5-10 minutes
to the time it takes to restart a given HOL session ... on a SS10 it
was just about bearable. 

Pre-compiled modules are possible currently but, I'm told, would make
hol90 even larger :-) I think SMLofNJ v10x (i.e. the next release
whenver it comes out) is going to address the idea of seperate
compilation. Of course, the library code in hol90 would then, probably,
need rewriting to fit in with this, possibly making it even more
dependent on SMLofNJ.

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