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

Makarius makarius at sketis.net
Sat Feb 28 16:23:26 CET 2009

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


More information about the isabelle-dev mailing list