Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: info-hol@leopard.cs.byu.edu, reetz@ira.uka.de
Cc: kropf@ira.uka.de, schneide@ira.uka.de
In-Reply-To: <"irafs2.ira.312:17.03.95.08.42.53"@ira.uka.de> (message from reetz on Fri, 17 Mar 1995 09:42:49 +0100)
Subject: Re: memory consumption of load_theory in HOL90.7
Message-Id: <95Mar17.124543met.8081@sunbroy14.informatik.tu-muenchen.de>
Date: Fri, 17 Mar 1995 12:45:36 +0100


Ralph Reetz writes

> I generated a large hol theory (containing a semantics for
> a subset of VHDL), needing 80 MB heapsize. The stored
> theory size in ascii format was:
> 
> vhdl_semantics.holsig:  0.8 Mb
> vhdl_semantics.thms:   14.0 Mb
> 
> Sounds too much, but using a Sparc 10 with 128 MB main
> memory, everything worked fine. Even using this theory
> resisting in memory worked fine, too. No memory problems.
> But starting a `fresh' hol and naively using
> 
> load_theory "vhdl_semantics";
> 
> heap size was increasing and increasing. I stopped it
> after a heap size of 500 Mb. It never worked.

This is entirely a problem with the naive representation of hol90
theorems on disk and has nothing to do with consistency checking. I
intend to replace the current scheme with one that does a better job of
sharing common types and terms, but until then hol90 will have problems
with doing "load_theory" on large theories with many polymorphic
constants. As an ad-hoc replacement, use "save_hol" to take a snapshot
of your theory development - it's only when theories are exported that
their size can blow up.

> I really wonder whether current HOL90 with its unacceptable
> memory consumption for things with relativly low
> information content really fits for real word problems.

But isn't this a general problem of verification? For example, it is
well known that difficult theorems in mathematics, having exceeding high
"information content" if you will, may have very short statements.
Relatively mundane problems of large size and, presumably, redundancy,
require efficient yet tricky representation.

> Considering HOL2000, one might maybe through SML away as
> a meta language and use an efficient C implementation
> instead. Using the library concept of C, this can be
> as open to extentions as the current version in SML.
> (People may flame me:-)

OK, I will. As long as one is in a situation needing garbage collection,
one may as well stick with a language that already has a garbage
collector. "Efficient C implementations" in such cases usually turn out
to be slower and buggier.

Konrad.