Noteble slowdown of AFP/Native_Word
Makarius
makarius at sketis.net
Sat Jul 26 19:57:22 CEST 2025
There is a notable slowdown AFP/Native_Word:
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)
In the above changeset intervals, I see many changes on words and code
generation setup by Florian Haftmann, both in Isabelle and AFP.
He needs to say if the effect on Native_Word is to be expected, or if this a
problem that has been overlooked.
Makarius
More information about the isabelle-dev
mailing list