Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
To: David Shepherd <des@uk.co.inmos>
Cc: Wai.Wong@uk.ac.cam.cl (Wai Wong), info-hol@edu.uidaho.cs.ted, 
    Wai.Wong@uk.ac.cam.cl
Subject: Re: Theory loading
In-Reply-To: Your message of Fri, 05 Feb 93 14:01:54 +0000. <16142.9302051401@frogland.inmos.co.uk>
Date: Mon, 08 Feb 93 12:37:53 +0000
From: Wai Wong <Wai.Wong@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.372:08.02.93.12.38.43"@cl.cam.ac.uk>


In David Sheperd' message:

>Wai Wong has said:
>> 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.
>
> At one time this was because the a naive approach was taken which involved
> going recursively up the theory tree activating binders. However, this
> had big problems if you theory graph became "wide" in the middle
> - e.g. ig you had one theory with 8 parents each of which had the same
> parent (grandparent ?) as this theory would be activated 8 times + all its
> ancestors as the routine recursed through each parent of the the original
> theory. I think this one had been fixed now.

The problem of recursively up the theory tree activating binders
has NOT been fixed yet!!! This is still part of the reasons why loading
theories take so long.

Unlike infix, which is stored in the theory data part of a
theory, binders are stored in the theorem part. This means if you
want to find out whether there are any binders in a theory, you need
to load the whole theorem part. This takes most of the time. Once a
theory is loaded into the theory cache, it will take much less time
to access if it is needed again. However repeatedly activating binders
in the ancester thoeries still wastes time.

Unless we change the format of the theory file, which will
probably introduce incompatibility and not many people will like it,
this problem is difficult to solve.

>> Meanwhile, to speed up the loading witout recompile the
>> system, individuals can put the following into their hol-init.ml:
>
> This doesn't (always) work.
>
> Suppose theory A has theory B as parent. When you declare theory A as
> parent you need to activate binders in B as well.

You are right here.

I  think for the time being, if you realy want to speed up the
loading, AND you are SURE there is NO binders defined in all the
ancester theories including any libraries you may use, you can
redefine the theory loading functions in the way shown in my last
message. This saves the loading of  the complete contents of 
all the ancester theories.

A way to fix the recursively up the theory tree activating binders
problem without changing the theory file format
is to reimplement the activate_all_binders function in the system
which I have just done. In the new implementation, I first get the
names for all the ancesters of the theory whose binders are to be
activated and then activate the binders in each of them. I use a
global variable to store the names of all the theories which has
been visited to activate their binders. When next time
activate_all_binders is called again, this is consulted to prevent
repeatedly loading the theories. The theory loading functions call
this activate_all_binders function, while this function itself is
hidden and not available at the user level as the manual has said
what it should be.

Wai