Stream: General

Topic: Isabelle/jEdit becomes unstable after sledgehammer

Yosuke Ito (Jan 29 2026 at 23:53):

Hello,
After updating to Isabelle2025-2, I noticed that Isabelle/jEdit becomes unstable after using sledgehammer. By "unstable" I mean the following:

• The continuous checking of Isabelle/jEdit freezes for about 10 seconds.
• After that, the continuous checking restarts from the beginning of the theory.

Has anyone experienced a similar issue?
If so, I would appreciate any workaround or suggestions.
For reference, I am using MacBook Air (M1, 2020) with 8 GB of memory.

Yosuke Ito (Jan 31 2026 at 08:09):

I reinstalled Isabelle2025-2, but the situation did not change.

Yosuke Ito (Feb 07 2026 at 02:19):

@Max Lang
Do you have the same issue?

Max Lang (Feb 07 2026 at 02:27):

I think my issue is different, but similar enough that I would be interested if a solution to your problem also applies.

• For me, it happens in Isabelle-2025
• It's not only sledgehammer, but also try0
• Isabelle/jEdit (usually) does not start checking again, so a full restart is required. Syntax highlighting, editing, etc. still works as usual, just no output.

It's been a few months since I worked in Isabelle, so I don't remember all the specifics unfortunately. I had written it off as having perhaps too little memory (although 16 GB should probably be sufficient) or some system mis-configuration on my end.

Yosuke Ito (Feb 07 2026 at 02:42):

OK. Thanks for the reply.
I'm not sure if my solution would be applicable to your issue, but I will report when I find a workaround.

Yosuke Ito (Feb 09 2026 at 04:54):

I got a reply from Makarius on the mailing list.
He said that 8GB was too small for Isabelle.
I ordered a new MacBook yesterday...

This is my guess from a distance:

• 8GB is too little to use Isabelle + addon tools seriously. You may get around by trimming some heap options of Java and/or Poly/ML, if you invest time on it (which I won't).
• macOS in particular has "compressed memory". I don't understand the details, but high-end Isabelle users on macOS keep telling me, that it is in conflict with the dynamic heap management of Java and/or Poly/ML, which are essentially big LISP machines.

Here is a blog article on the topic:
https://blog.greggant.com/posts/2024/07/03/macos-memory-management.html
Quote:
"""
How Memory Works in macOS (why Apple can get away with shipping computers with 8 GB of RAM).
"""
I would say that it is futile to try Isabelle with 8GB: 16GB or 32GB is more
realistic. My regular workstation at home has 64GB, my mobile presentation
machine 32GB -- it is a very light and "airy" Linux machine.

Alex Mobius (Feb 24 2026 at 16:22):

I've definitely noticed some sort of memory leak in 2025-2 after using try - the JVM memory consumption keeps climbing up then GCing, and the problem seems to persist until restart. Upgrading machine is not an option ATM, and it feels like this didn't use to happen on 2025-1.

Yosuke Ito (Feb 25 2026 at 00:04):

@Alex Mobius
Thanks for your comment.
I actually bought a new MacBook with 32 GB of RAM, and the problem seems almost gone now. However, if that is the case, the issue may still remain, since I usually do not use try.

Alex Mobius (Feb 25 2026 at 02:48):

It seems that after several uses of either try or sledgehammer panel the lower bound for ML memory climbs up - for me it starts at around 200 MB but eventually climbed to 3GB while working in the same theory file, and at that point constant GC renders the system unusable and necessitates a restart. If that's not a memory leak qua memory leak, there's at least some aggressive caching going on.

Fabian Huch (Feb 25 2026 at 08:22):

Can you check whether there are veriT processes that don't terminate? That is a known problem, but other than maybe disabling the solver altogether, there is not much we can do on the Isabelle side.

Last updated: Feb 27 2026 at 20:31 UTC