Slowdown of AFP/SC_DOM_Components due to changes in "code-only operations"

Makarius makarius at sketis.net
Sat Jul 26 18:11:29 CEST 2025


Here is a notable slowdown of SC_DOM_Components from some months ago: 
AFP/42327343c286. "hg bisect" in the interval of Isabelle/b69e4da2604b .. 
32dd31062eaa says:

The first bad revision is:
changeset:   82692:8f0b2daa7eaa
user:        haftmann
date:        Thu Jun 12 08:03:05 2025 +0200
summary:     reorganized more code-only operations


Here are the timings on my local machine, before and after that change:

Finished HOL (0:01:51 elapsed time, 0:05:49 cpu time, factor 3.14)
Finished HOL-Library (0:01:21 elapsed time, 0:05:50 cpu time, factor 4.33)
Finished Core_SC_DOM (0:01:17 elapsed time, 0:04:43 cpu time, factor 3.63)
Finished Shadow_SC_DOM (0:03:24 elapsed time, 0:13:24 cpu time, factor 3.94)
Finished SC_DOM_Components (0:01:54 elapsed time, 0:09:45 cpu time, factor 5.11)

Finished HOL (0:01:49 elapsed time, 0:05:42 cpu time, factor 3.12)
Finished HOL-Library (0:01:21 elapsed time, 0:05:51 cpu time, factor 4.31)
Finished Core_SC_DOM (0:01:17 elapsed time, 0:04:39 cpu time, factor 3.62)
Finished Shadow_SC_DOM (0:03:22 elapsed time, 0:13:10 cpu time, factor 3.90)
Finished SC_DOM_Components (0:05:45 elapsed time, 0:14:29 cpu time, factor 2.52)


That also demonstrates my "cheap midrange workstation" from some months ago, 
with AMD Ryzen 9 7950X 16-Core Processor at almost 5.8 GHz. Only 8 threads 
have been used above.


	Makarius



More information about the isabelle-dev mailing list