Email Gateway (Jul 26 2025 at 16:12): Email Gateway (Jul 26 2025 at 16:12):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 07 2025 at 17:08):From: Florian Haftmann <florian.haftmann@cit.tum.de>
Am 26.07.25 um 18:11 schrieb Makarius:
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
This is not easy to pin down.
That session is very special: it provides monadic specifications
(presumably an error monad), and uses code_simp as a device to basically
unfold all (!) operations, leaving the resulting gigantic proof goal to
the mercy of the classical reasoner. The excessive use of the code_simp
also brings in a lot of things which are only intended for code
generation, e.g. class equal and a lot of auxiliary operations on lists.
When I had to visit that session during the reorganization, I had the
impression that any proper migration would require to rework the whole
session, starting with elementary rules to conduct proofs on monadic
expressions.
This is the reason why in AFP 4450de6d0858 I restric myself to remove
some simp rules in an ad-hoc manner to make things run again.
Maybe I could risk a blind shot and just remove the simp rules added in
the change above and see if this gains something.
Cheers,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Last updated: Aug 31 2025 at 20:21 UTC