[isabelle-dev] Slowdown of ConcurrentGC

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu May 17 10:55:41 CEST 2018


Hi Makarius,

> I have studied this a bit further. The interval
> 75130777ece4:d45b78cb86cf contains more than just the string type
> change, but it is still the main thing. Here are also other sessions in
> similar intervals 75130777ece4:0a6d6ba383dc, 75130777ece4:f76e8180c498:
> 
>   * faster: HOL-IMP, HOL-Quickcheck_Examples,
>     Network_Security_Policy_Verification, Pre_Perron_Frobenius,
>     JiveDataStoreModel, Partial_Function_MR
> 
>   * slower: Tarskis_Geometry, XML, Cauchy

distangling the ancient misunderstaning of char in Isabelle vs. various
character-related types in several target languages may indeed come at a
certain price in exotic situations; anyway I will have a look at those
sessions whether something meaningful can be derived from them.

Cheers,
	Florian

-- 

PGP available:
http://isabelle.in.tum.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: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180517/71e4a980/attachment.sig>


More information about the isabelle-dev mailing list