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

[Florian Haftmann]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_0xA707172232CFA4E9.asc
Type: application/pgp-keys
Size: 22777 bytes
Desc: OpenPGP public key
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250807/74631de8/attachment.key>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250807/74631de8/attachment.sig>