Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
To: info-hol@leopard.cs.byu.edu
Cc: kropf@ira.uka.de, schneide@ira.uka.de
Subject: memory consumption of load_theory in HOL90.7
Date: Fri, 17 Mar 1995 09:42:49 +0100
From: reetz <reetz@ira.uka.de>
Message-Id: <"irafs2.ira.312:17.03.95.08.42.53"@ira.uka.de>


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.

I really wonder: is this necessary? The GENERATION of
the theory needed 80 MB heap size and generation already
means checking consistency with already existing
definitions. But just LOADING (which may incorporate
AT MOST the same consistency checking, I think) needs
500 MB + X MB, whatever X may be. I never got it.

What is the problem?

a) the size of the theory?
I used "gzip vhdl_semantics.thms" to get a hint about
the ``real information content'' and I got
vhdl_semantics.thms.gz: 0.25 MB. Not that large.
Generation worked, as I said.

b) the size of the file?
I did not test binary format for theories...I do not
want to generate all theories here.

c) bad implementation of load_theory?
maybe somebody knowing the source code better than I
can give an answer here.


[general_doubt:=on;]
I really wonder whether current HOL90 with its unacceptable
memory consumption for things with relativly low
information content really fits for real word problems.
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:-):take a look at the model--checker:
they squeeze out every bit using effizient data
structures and C. There is much less
overhead than in HOL, as it seems to me on the first look.
Considering the example on load_theory above, I can not
believe that such an huch memory is needed for higher
order logic theorems provers.
[general_doubt:=off;]

Ralf.

(*******************************************************************)
(*                                                                 *)
(*  Ralf Reetz                                                     *)
(*                                                                 *)
(*  University of Karlsruhe                                        *)
(*  Institut fuer Rechnerentwurf und Fehlertoleranz                *)
(*  76128 Karlsruhe, Zirkel 2, Postfach 6980, Germany              *)
(*                                                                 *)
(*  e-mail: reetz@informatik.uni-karlsruhe.de or reetz@ira.uka.de  *)
(*  WWW:    http://goethe.ira.uka.de/people/reetz/reetz.html       *)
(*                                                                 *)
(*******************************************************************)