[isabelle-dev] A better policy for the typerep class
florian.haftmann at informatik.tu-muenchen.de
Wed Feb 11 11:13:40 CET 2009
> I'm afraid I don't understand why reducing the number of merges by
> adding "wasp-waists" is beneficial. From what I understand, adding
> additional theory dependencies could only reduce opportunities for
> parallel execution. Is there another technical reason why the amount of
> merging needs to be limited?
The scene in parallelism has shifted: now also proofs are checked in
parallel, which reduces the relevance of parallel theory loading
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 252 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev