Noteble slowdown of AFP/Native_Word

Florian Haftmann florian.haftmann at cit.tum.de
Sun Jul 27 19:25:39 CEST 2025


Hi Makarius,

> Isabelle/e4207dfa36b5 AFP/16cb1cb993ae
> Finished HOL (0:01:46 elapsed time, 0:05:36 cpu time, factor 3.16)
> Finished Word_Lib (0:00:26 elapsed time, 0:01:37 cpu time, factor 3.70)
> Finished Native_Word (0:01:36 elapsed time, 0:01:23 cpu time, factor 0.86)
> 
> Isabelle/3704717ed7bf AFP/ccc0b8182357
> Finished HOL (0:01:47 elapsed time, 0:05:41 cpu time, factor 3.17)
> Finished Word_Lib (0:00:25 elapsed time, 0:01:36 cpu time, factor 3.81)
> Finished Native_Word (0:03:27 elapsed time, 0:03:16 cpu time, factor 0.94)

thanks for figuring that out.

Honestely, these are things were I miss the plain old isatest with its 
generated charts.

Anyway, I will look after those issues, but it will take some time 
before I can actually dive into.

	Florian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_0xA707172232CFA4E9.asc
Type: application/pgp-keys
Size: 22777 bytes
Desc: OpenPGP public key
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250727/69781776/attachment.key>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250727/69781776/attachment.sig>


More information about the isabelle-dev mailing list