Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) outside ac.uk; Fri, 5 Feb 1993 13:51:22 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA15283;
          Fri, 5 Feb 93 05:39:58 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA15278;
          Fri, 5 Feb 93 05:39:51 -0800
Received: from heron.cl.cam.ac.uk (user ww (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) to cl; Fri, 5 Feb 1993 13:39:23 +0000
To: info-hol@edu.uidaho.cs.ted
Subject: Theory loading
Date: Fri, 05 Feb 93 13:39:14 +0000
From: Wai Wong <Wai.Wong@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.656:05.02.93.13.39.26"@cl.cam.ac.uk>


In a message from David Shepherd sometimes ago, he said:
> Sometimes ago there was some discussion on the length of time that HOL
> takes to read in theory files. Part of this can be attributed to the
> way in which HOL has to unwind all the SHARETYPES and other type
> information that gets folded out of the theorems in the theory file.

This is certainly true. But, I've found there is other factor which
causes the loading of theory very slow, especialy if you have a lot
of theories in the ancestry. The reason is the theory loading
functions call an (internal) function to activate the binders in all
ancester theories unnecessarily. This takes a long time.
This problem will be fixed in the next version of HOL.

Meanwhile, to speed up the loading witout recompile the
system, individuals can put the following into their hol-init.ml:

% --------------------------------------------------------- %

lisp `(declare-ml-fun 
    (quote |nnew_parent|)
    (quote 1) 
    (quote ml-new_parent)
    (quote (|string| -> |void|)))`;;

lisp `(declare-ml-fun
    (quote |lload_theory|)
    (quote 1)
    (quote ml-load_theory)
    (quote (|string| -> |void|)))`;;

lisp `(declare-ml-fun
    (quote |eextend_theory|)
    (quote 1)
    (quote ml-extend_theory)
    (quote (|string| -> |void|)))`;;

let load_theory =
     \thy. (lload_theory thy; activate_binders thy; ());;

let extend_theory =
    \thy. (eextend_theory thy;
           activate_binders thy;
           list_of_binders := binders thy;
           ((delete_thm thy `LIST_OF_BINDERS`; ()) ? ());
           ());;

let new_parent thy =
    (new_parent thy;
     activate_binders thy; ());;

% --------------------------------------------------------- %


Wai