Significant slowdown of HOL-ex and HOL-Codegenerator_Test

[Makarius]

There has been a significant slowdown of HOL-ex and HOL-Codegenerator_Test due 
to the following changeset:

changeset:   83131:7d6e6531de61
user:        paulson <lp15 at cam.ac.uk>
date:        Sun Sep 07 22:37:57 2025 +0100
files:       src/HOL/ROOT
description:
Removing "HOL-Library" as ancestor theory


The log message keeps the motivation (or justification) secret, but I can 
imagine certain situations where *removing* of intermediate session images 
generally improves the build process. In AFP. my standard log message is 
"build faster without intermediate session image", often with concrete 
indication about actually saved time.

Above this did not quite work, notably for HOL-ex and HOL-Codegenerator_Test, 
where a lot of material from the parent session is actually used. Here are 
some timings on my AMD Ryzen 9 7950X 16-Core Processor (with threads=8).

87c96d455992, which includes 7d6e6531de61:
Finished HOL (0:01:52 elapsed time, 0:06:04 cpu time, factor 3.23)
Finished HOL-Computational_Algebra (0:00:41 elapsed time, 0:02:20 cpu time, 
factor 3.38)
Finished HOL-Number_Theory (0:00:31 elapsed time, 0:02:13 cpu time, factor 4.22)
Finished HOL-ex (0:02:08 elapsed time, 0:11:03 cpu time, factor 5.15)
Finished HOL-Codegenerator_Test (0:04:22 elapsed time, 0:13:12 cpu time, 
factor 3.02)

87c96d455992, after "hg backout 7d6e6531de61":
Finished HOL (0:01:51 elapsed time, 0:05:57 cpu time, factor 3.20)
Finished HOL-Library (0:01:20 elapsed time, 0:05:43 cpu time, factor 4.28)
Finished HOL-Computational_Algebra (0:00:37 elapsed time, 0:01:58 cpu time, 
factor 3.19)
Finished HOL-Number_Theory (0:00:31 elapsed time, 0:02:05 cpu time, factor 3.97)
Finished HOL-ex (0:01:45 elapsed time, 0:07:39 cpu time, factor 4.34)
Finished HOL-Codegenerator_Test (0:03:20 elapsed time, 0:06:49 cpu time, 
factor 2.04)


After my new change 746983070fca the situation is mostly back to normal:

Finished HOL (0:01:54 elapsed time, 0:06:06 cpu time, factor 3.19)
Finished HOL-Library (0:01:20 elapsed time, 0:05:42 cpu time, factor 4.28)
Finished HOL-ex (0:01:50 elapsed time, 0:08:17 cpu time, factor 4.50)
Finished HOL-Codegenerator_Test (0:03:08 elapsed time, 0:07:11 cpu time, 
factor 2.28)


Thus the cluster build also becomes faster again, but it might be hard to 
measure exactly due to its persistent history of build times used for 
scheduling. On my local machine, a regular "isabelle build -j2 -a" is 
something like 26min vs. 25min.


Side-remark: for interactive development in Isabelle/jEdit, the session build 
hierarchy can be trimmed-down on the spot. For example:

   isabelle jedit -A HOL -R HOL-ex

or even:

   isabelle jedit -A Pure -R HOL-ex

Thus only one image is built in parallel with 8 threads:

Finished HOL-ex_requirements(Pure) (0:02:56 elapsed time, 0:13:07 cpu time, 
factor 4.45). That is 20s shorter than sequential HOL + HOL-Library.


	Makarius