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

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Wed Feb 11 11:13:40 CET 2009

Hi Brian,

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




PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20090211/f90ee5b0/attachment.sig>

More information about the isabelle-dev mailing list