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: <10103.9406071423@frogland.inmos.co.uk>
Subject: Re: Why HOL is so large?
To: wishnu@cs.ruu.nl (Wishnu Prasetya)
Date: Tue, 7 Jun 1994 15:23:39 +0100 (BST)
Cc: info-hol@cs.uidaho.edu
In-Reply-To: <199406071306.AA18994@relay.cs.ruu.nl> from "Wishnu Prasetya" at Jun 7, 94 03:06:33 pm
Content-Type: text
Content-Length: 1938

Wishnu Prasetya has said:
> I see two applications of HOL. As a theorem prover, mainly in a
> hardware design. And as a proof management system, mainly to assist
> scientists in writting correct proofs. Unfortunately we are still long
> from the day where when every one in the department can engineer his
> proof as he would his document with LaTeX now. One of the challange is
> the computing power requirement of HOL. Perhaps some one can kindly
> explain to me why, for example, HOL requires so much memory to run? Is
> this 4-9MB really the bottom line? Of course we can also hope that
> memory will become considerably cheaper in the future.

... I think its not HOL as such that's so large ... its Common Lisp or
NJML which bloats it. After all, I remember back in the good ole days
of sun3's and Franz Lisp that the binary there was only around 2.5Mb.

Part of the problem is, of course, that as well as the HOL system
you are also carrying a Lisp or SML compiler around with you - that
probably contributed to the Franz version being relatively compact.

As an example of this ... dumping sml-yacc from a standard SML
(i.e. like HOL) generates a 4-5Mb image. However, dumping from
a -noshare SML image produces an dumped image with all unused
stuff (i.e. the compiler) omitted and goes down to 800kb. However,
since we still need to compile library code we can't really do this for
HOL.

Once HOL loads then memory useage is another matter completely ... SML
just seems to love to claim more and more of it :-)

BTW, you mention LaTeX above ... do you realise that the FrameMaker
executable is around 10Mbs ... its not just HOL that's large.

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