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