Email Gateway (Sep 22 2023 at 19:21): Email Gateway (Sep 22 2023 at 19:21):From: hannobecker@posteo.de
Hi all,
In the context of a large Isabelle development, I noticed an occasional
yet
hefty performance degradation of Isabelle2023 compared to Isabelle2022.
The
behaviour is somewhat ephemeral and has escaped attempts to create a
minimal
example, but here's some context & symptoms:
The performance loss happens in a theory depending on many other
theories.
The entire body of the theory is within a locale context opened
immediately
after the theory preamble.
All definitions in the locale take a noticeable time (~1s each) to
process, while previously they were instantaneous.
System: MacBook Pro, 32GB RAM, Ventura 13.5.2
Now for the interesting bit:
The performance degradation goes away when inserting a dummy lemma
(lemma
dummy: shows <x=x> by simp, say) before opening the locale context.
In this case,
the lemma itself is processed slowly (~1s again), but all subsequent
commands are back
to normal speed, including those happening in the context of the
locale.
Even when removing the dummy lemma afterwards, the re-processing of
the theory body
will still happen at normal speed.
Some speculations:
Perhaps some normalization or lazy evaluation step is happening the
first time a lemma or definition
is processed in a theory, but this step does not happen for commands
inside a locale?
Concretely, I got the impression that it may be related to local vs
global syntax, and how global syntax
is cached: When issuing aSyntax.read_typ prior to opening the locale,
the slowdown disappears, while it
doesn't with a Syntax.read_typ within the locale.
Anyway, this is all I found so far. Any ideas?
Cheers,
Hanno
Email Gateway (Oct 18 2023 at 05:12):From: hannobecker@posteo.de
Ping. Any thoughts on the issue below?
Email Gateway (Apr 03 2024 at 14:51):From: Makarius <makarius@sketis.net>
Hi Hanno,
we can pick up this thread again, now that the Isabelle2024 release process
has officially started with RC1:
https://isabelle-dev.sketis.net/phame/post/view/76/release_candidates_for_isabelle2024
This window of opportunity will be open for approx. 6 weeks, when the release
becomes final, unchangeable, and by definition perfect. Isabelle has no
"branches", "patches", "fixes" and thus avoids a huge overhead in the
development process. In practice this merely means that test versions need to
be tested before they converge to the final release.
For Isabelle2024-RC1, I have produced the following change to the newly
introduced inner syntax cache of Isabelle2023:
https://isabelle-dev.sketis.net/rISABELLE40f5ddeda2b4
My guess from a distance is that your application has very large syntax tables
and overall rather big ML heap demands. Thus the cache (weak reference cell)
was purged a bit too often (at GC time). In Isabelle2024-RC1 the memory
management should again closer to Isabelle2022, but only in PIDE interaction,
not in batch builds.
Makarius
Email Gateway (Apr 23 2024 at 03:38):From: hannobecker@posteo.de
Hi Makarius,
I have tested our application on Isabelle2024-RC2 and can report that
the problem has gone away, which is great. Thank you for your work.
Last updated: Apr 28 2024 at 20:16 UTC