Email Gateway (Sep 13 2025 at 20:12): Email Gateway (Sep 13 2025 at 20:12):From: Makarius <makarius@sketis.net>
There has been a significant slowdown of HOL-ex and HOL-Codegenerator_Test due
to the following changeset:
changeset: 83131:7d6e6531de61
user: paulson <lp15@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
Email Gateway (Sep 14 2025 at 16:23):From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
Feel free to revert, at least for those two. The original impetus was HOL-Computational_Algebra, which was taking forever to build when importing the whole of HOL-Library.
On 13 Sep 2025, at 21:11, Makarius <makarius@sketis.net> wrote:
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).
Last updated: Sep 15 2025 at 08:27 UTC