Email Gateway (Oct 28 2026 at 08:48): Email Gateway (Oct 28 2026 at 08:48):From: Kevin Kappelmann <cl-isabelle-users@lists.cam.ac.uk>
Hi all,
Markup_Tree.cumulate (and hence Document.Snapshot.select/cumulate)
throws a StackOverflowError when a range contains many matching
elements, e.g. all entities of HOL.List. A reproducible example for
Isabelle2026 is shown below.
I think this exists since d29bf6db8a2d ("more elementary list structures
for markup tree traversal", Isabelle2013-1), which replaced lazy streams
with strict lists. Maybe the function can be made tail-recursive?
Best wishes,
Kevin
Example that can be run with isabelle scala Overflow.scala (requires a
HOL session build):
import isabelle._
object Overflow {
def main(args: Array[String]): Unit = {
val store = Store(Options.init())
using(Export.open_session_context0(store, "HOL")) { session_context =>
val snapshot =
Build.read_theory(session_context.theory("HOL.List")).get
val range = Text.Range(0, snapshot.node.source.length)
val entities = snapshot.select(range,
Markup.Elements(Markup.ENTITY), _ => _ => Some(()))
println(entities.length)
}
}
}
From: Makarius <makarius@sketis.net>
On 28/10/2026 09:48, Kevin Kappelmann (via cl-isabelle-users Mailing List) wrote:
Markup_Tree.cumulate (and hence Document.Snapshot.select/cumulate) throws a
StackOverflowError when a range contains many matching elements, e.g. all
entities of HOL.List. A reproducible example for Isabelle2026 is shown below.
Stackoverflow is a normal reality on the Java Virtual Machine. It is your own
responsibility to provide a sufficiently large stack limit beforehand, e.g in
$ISABELLE_HOME_USER/etc/settings like this:
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms256m -Xmx8g -Xss32m"
The precise settings variable to be used depends on how the underlying JVM is
actually started. E.g. in "isabelle jedit" it is JEDIT_JAVA_OPTIONS. In the
desktop application this works again differently, depending on the platform.
Maybe the function can be made tail-recursive?
No. Sources need to say as clearly as possible what really happens. The
Markup_Tree module is as important as Thm for the overall correctness of the
system.
The problem should disappear spontaneously, when the distinction of PIDE
processing vs. batch builds has made more progress --- because the granularity
of markup trees will be that of a single command, not all commands together as
one unit.
Makarius
Email Gateway (Oct 28 2026 at 10:46):From: Kevin Kappelmann <cl-isabelle-users@lists.cam.ac.uk>
Seems reasonable.
The problem should disappear spontaneously, when the distinction of PIDE
processing vs. batch builds has made more progress
Looking forward to it!
Kevin
On 28.10.26 11:27, Makarius wrote:
On 28/10/2026 09:48, Kevin Kappelmann (via cl-isabelle-users Mailing
List) wrote:Markup_Tree.cumulate (and hence Document.Snapshot.select/cumulate)
throws a
StackOverflowError when a range contains many matching elements, e.g.
all
entities of HOL.List. A reproducible example for Isabelle2026 is
shown below.Stackoverflow is a normal reality on the Java Virtual Machine. It is
your own responsibility to provide a sufficiently large stack limit
beforehand, e.g in $ISABELLE_HOME_USER/etc/settings like this:ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms256m -Xmx8g
-Xss32m"The precise settings variable to be used depends on how the underlying
JVM is actually started. E.g. in "isabelle jedit" it is
JEDIT_JAVA_OPTIONS. In the desktop application this works again
differently, depending on the platform.Maybe the function can be made tail-recursive?
No. Sources need to say as clearly as possible what really happens. The
Markup_Tree module is as important as Thm for the overall correctness of
the system.The problem should disappear spontaneously, when the distinction of PIDE
processing vs. batch builds has made more progress --- because the
granularity of markup trees will be that of a single command, not all
commands together as one unit.Makarius
Last updated: Oct 29 2026 at 04:52 UTC