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

[Florian Haftmann]

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

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.

	Florian

-- 

Home:
http://wwwbroy.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

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