Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: David Shepherd <des@uk.co.inmos>
Message-Id: <16142.9302051401@frogland.inmos.co.uk>
Subject: Re: Theory loading
To: Wai.Wong@uk.ac.cam.cl (Wai Wong)
Date: Fri, 5 Feb 1993 14:01:54 +0000 (GMT)
Cc: info-hol@edu.uidaho.cs.ted
In-Reply-To: <"swan.cl.ca.656:05.02.93.13.39.26"@cl.cam.ac.uk> from "Wai Wong" at Feb 5, 93 01:39:14 pm
Content-Type: text
Content-Length: 1478

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.

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

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		Life doesn't imitate art, it imitates bad television
						      - Husbands and Wives