Email Gateway (Oct 01 2026 at 16:38): Email Gateway (Oct 01 2026 at 16:38):From: Kevin Kappelmann <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] memory leak(?): GC not reclaiming memory when an importing theory is open (affecting Isabelle2026-RC2 and Isabelle2025-2)
Dear list,
Below are instructions to create a memory leak(?), tested with
Isabelle2026-RC2 and Isabelle2025-2.
Summary: When an ML command in a theory is re-evaluated (with each
evaluation possibly allocating memory) while a theory importing it is
open, a subsequent full GC does not reclaim most of the memory. Without
the importing theory, a full GC brings the memory usage back to a normal
level.
Steps to reproduce (theories attached):
isabelle jedit -l Pure Base.thy (only open Base.thy).Open the jEdit Monitor window (double click on the ML usage bar,
bottom right) and run a full GC. The memory usage drops significantly.
Split the window (View -> Splitting) and open Importer.thy side by
side (having it open in the background is not sufficient).
Repeat steps 2 and 3. The full GC now leaves most of the memory in use.
I also reproduced the same behaviour with VSCode and a headless PIDE
session.
Background/how I discovered it: When developing an ML package, its ML
commands are repeatedly evaluated (due to me editing them), gradually
filling up my machine's memory until I have to restart Isabelle.
Best wishes,
Kevin
Email Gateway (Oct 01 2026 at 16:44):From: "Lammich, Peter (UT-EEMCS)" <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] memory leak(?): GC not reclaiming memory when an importing theory is open (affecting Isabelle2026-RC2 and Isabelle2025-2)
That fits an observation of mine: when working on refactoring jobs, I'd have a base theory and a dependent theory open at the same time in two buffers ( typically I use new view)... This regularly leads to responsiveness degrading until there's no other way than restarting the whole thing... I intuitively avoid this setup, and rather switch one buffer between the two theories.
Peter
Sent from Outlook for Android<https://aka.ms/AAb9ysg>
From: cl-isabelle-users-request@lists.cam.ac.uk <cl-isabelle-users-request@lists.cam.ac.uk> on behalf of Kevin Kappelmann <cl-isabelle-users@lists.cam.ac.uk>
Sent: Thursday, 01 October 2026 17:38:04
To: cl-isabelle-users@lists.cam.ac.uk <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] memory leak(?): GC not reclaiming memory when an importing theory is open (affecting Isabelle2026-RC2 and Isabelle2025-2)
Dear list,
Below are instructions to create a memory leak(?), tested with
Isabelle2026-RC2 and Isabelle2025-2.
Summary: When an ML command in a theory is re-evaluated (with each
evaluation possibly allocating memory) while a theory importing it is
open, a subsequent full GC does not reclaim most of the memory. Without
the importing theory, a full GC brings the memory usage back to a normal
level.
Steps to reproduce (theories attached):
isabelle jedit -l Pure Base.thy (only open Base.thy).Open the jEdit Monitor window (double click on the ML usage bar,
bottom right) and run a full GC. The memory usage drops significantly.
Split the window (View -> Splitting) and open Importer.thy side by
side (having it open in the background is not sufficient).
Repeat steps 2 and 3. The full GC now leaves most of the memory in use.
I also reproduced the same behaviour with VSCode and a headless PIDE
session.
Background/how I discovered it: When developing an ML package, its ML
commands are repeatedly evaluated (due to me editing them), gradually
filling up my machine's memory until I have to restart Isabelle.
Best wishes,
Kevin
Email Gateway (Oct 01 2026 at 16:49):From: Jan van Brügge <jan@vanbruegge.de>
Subject: [isabelle] memory leak(?): GC not reclaiming memory when an importing theory is open (affecting Isabelle2026-RC2 and Isabelle2025-2)
I have also noticed Isabelle crawling to after developing ML for a while now. I did not report it as I run a modified version of Isabelle and could not exclude that as the source of the issue.
Jan
01.10.2026 18:44:05 "Lammich, Peter (UT-EEMCS)" (via cl-isabelle-users Mailing List) <cl-isabelle-users@lists.cam.ac.uk>:
That fits an observation of mine: when working on refactoring jobs, I'd have a base theory and a dependent theory open at the same time in two buffers ( typically I use new view)... This regularly leads to responsiveness degrading until there's no other way than restarting the whole thing... I intuitively avoid this setup, and rather switch one buffer between the two theories.
Peter
Sent from Outlook for Android[https://aka.ms/AAb9ysg]
From: cl-isabelle-users-request@lists.cam.ac.uk <cl-isabelle-users-request@lists.cam.ac.uk> on behalf of Kevin Kappelmann <cl-isabelle-users@lists.cam.ac.uk>
Sent: Thursday, 01 October 2026 17:38:04
To: cl-isabelle-users@lists.cam.ac.uk <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] memory leak(?): GC not reclaiming memory when an importing theory is open (affecting Isabelle2026-RC2 and Isabelle2025-2)Dear list,
Below are instructions to create a memory leak(?), tested with
Isabelle2026-RC2 and Isabelle2025-2.Summary: When an ML command in a theory is re-evaluated (with each
evaluation possibly allocating memory) while a theory importing it is
open, a subsequent full GC does not reclaim most of the memory. Without
the importing theory, a full GC brings the memory usage back to a normal
level.Steps to reproduce (theories attached):
- Start
isabelle jedit -l Pure Base.thy(only openBase.thy).- Re-evaluate the ML command in Base a few times.
- Open the jEdit Monitor window (double click on the ML usage bar,
bottom right) and run a full GC. The memory usage drops significantly.- Split the window (View -> Splitting) and open
Importer.thyside by
side (having it open in the background is not sufficient).- Repeat steps 2 and 3. The full GC now leaves most of the memory in use.
I also reproduced the same behaviour with VSCode and a headless PIDE
session.Background/how I discovered it: When developing an ML package, its ML
commands are repeatedly evaluated (due to me editing them), gradually
filling up my machine's memory until I have to restart Isabelle.Best wishes,
Kevin
Email Gateway (Oct 05 2026 at 21:42):From: Makarius <makarius@sketis.net>
Subject: [isabelle] memory leak(?): GC not reclaiming memory when an importing theory is open (affecting Isabelle2026-RC2 and Isabelle2025-2)
On 01/10/2026 18:38, Kevin Kappelmann (via cl-isabelle-users Mailing List) wrote:
Below are instructions to create a memory leak(?), tested with Isabelle2026-
RC2 and Isabelle2025-2.Summary: When an ML command in a theory is re-evaluated (with each evaluation
possibly allocating memory) while a theory importing it is open, a subsequent
full GC does not reclaim most of the memory. Without the importing theory, a
full GC brings the memory usage back to a normal level.
I did not find time to look at this in time for Isabelle2026-RC3. It has to
wait until RC4.
Makarius
Email Gateway (Oct 06 2026 at 13:44):From: Makarius <makarius@sketis.net>
Subject: [isabelle] memory leak(?): GC not reclaiming memory when an importing theory is open (affecting Isabelle2026-RC2 and Isabelle2025-2)
On 01/10/2026 18:38, Kevin Kappelmann (via cl-isabelle-users Mailing List) wrote:
Below are instructions to create a memory leak(?), tested with Isabelle2026-
RC2 and Isabelle2025-2.Summary: When an ML command in a theory is re-evaluated (with each evaluation
possibly allocating memory) while a theory importing it is open, a subsequent
full GC does not reclaim most of the memory. Without the importing theory, a
full GC brings the memory usage back to a normal level.
I have experimented with many old releases, back to Isabelle2016 (February
2016). The behaviour is always the same. So this it is not a new problem, and
thus not relevant for the Isabelle2026 release.
Shortly after the release, I will revisit many PIDE details, providing more
robustness, removing ancient REPL legacy etc. This will be an opportunity to
look at this odd behaviour as well.
Makarius
Last updated: Oct 08 2026 at 21:07 UTC