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

[Makarius]

On Wed, 11 Feb 2009, Florian Haftmann wrote:

> Concerning the number of merges, it is just - as far as I know - an 
> observation that in presence of parallel proofs less merges increase 
> speed.  But perhaps Makarius can tell further details regarding this.

In principle you do not have to care much, as far as parallel theory and 
proof checking is concerned.  When arranging theories, the structure of 
the content should be the main issue -- i.e. things that are independent 
of each other should be on independent paths in the graph.

Nonetheless, bootstrapping in HOL introduces many quantum effects, some of 
them related to parallel checking.  The full HOL image (with full proof 
terms) is already close to the limit of what the 32 bit platform can 
manage, sometimes even beyond that limit.  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.)


	Makarius