[isabelle-dev] A better policy for the typerep class

[Makarius]

On Sat, 28 Feb 2009, Brian Huffman wrote:

> Quoting Makarius <makarius at sketis.net>:
> 
> >In particular, merging
> >ATP_Linkup is a bit critical: if it is done via several unrelated paths,
> >then some internal derivations are duplicated unnecessarily.  (In fact, it
> >used to crash here in the past, now it only wastes resources.)
> 
> I remember a comment that used to be in ATP_Linkup.thy, saying that it was
> required to be either a descendant or ancestor of every other theory. I guess
> this is no longer a requirement, but it seems like you are saying it is still
> strongly recommended.

At least inside the full HOL image, with full proofs, otherwise lots of 
duplicate proof terms will be produced.

The HOL performance bottleneck shows up, because the whole session is held 
in an unfinished state, with almost all proofs running potentially in 
parallel.  This eats up 2-4 GB of memory; afterwards everything is 
compressed to that "tiny" heap image of 110 MB (Poly/ML does maximal 
sharing of values here; but that process also requires extra memory.)

In regular "user sessions" based on the HOL image the situation is never 
that critical.


> If this is so, then maybe it is a good idea to move ATP_Linkup so that 
> it is imported by Plain? I know that some library theories import only 
> Plain and Presburger, for example; if ATP_Linkup were included with 
> Plain, it might avoid wasting resources in those cases.

I've discussed that with Florian to some degree.  He made a good job in 
reorganizing the HOL theory graph, without having to include ATP_Linkup in 
Plain.

Concerning the library, I am always puzzled why anything other than Plain 
or Main (or Complex_Main) is ever taken as a basis.  Many years ago, when 
we've introduce the "Main" checkpoint of Isabelle/HOL, the main idea was 
to relieve applications from bootstrapping issues of HOL.  Yes, even 10 
years ago, we've had such problems already.  Maybe they only show up 
again, because the strict policy of including main HOL checkpoints only 
has been forgotten.  (Complex_Main might be a slightly different issue; 
after Main there are probably no serious problem luring.)


	Makarius