Email Gateway (Feb 05 2026 at 11:51): Email Gateway (Feb 05 2026 at 11:51):From: 伊藤洋介 <glacier345@gmail.com>
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.
Does anyone know how to fix this issue?
My current workaround is to directly enter (by hand) the tactic generated
by sledgehammer;
If I avoid clicking the generated tactic, the jEdit remains stable.
However, I would like to fix the root cause of the problem because my
workaround is quite inconvenient.
For reference, I am using a MacBook Air (M1, 2020) with 8 GB of memory.
The macOS is Tahoe 26.2.
--
伊藤 洋介
Yosuke ITO
+81 80-5057-6931
glacier345@gmail.com
Email Gateway (Feb 07 2026 at 13:23):From: Makarius <makarius@sketis.net>
On 05/02/2026 12:51, 伊藤洋介 wrote:
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.Does anyone know how to fix this issue?
For reference, I am using a MacBook Air (M1, 2020) with 8 GB of memory.
The macOS is Tahoe 26.2.
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.
Makarius
Email Gateway (Feb 08 2026 at 05:42):From: 伊藤洋介 <glacier345@gmail.com>
Dear Makarius,
Thank you for the detailed advice.
All right, I'll consider purchasing a new MacBook.
In fact, my project is becoming bigger recently.
Best regards,
2026年2月7日(土) 22:23 Makarius <makarius@sketis.net>:
On 05/02/2026 12:51, 伊藤洋介 wrote:
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.Does anyone know how to fix this issue?
For reference, I am using a MacBook Air (M1, 2020) with 8 GB of memory.
The macOS is Tahoe 26.2.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.htmlQuote:
"""
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.Makarius
--
伊藤 洋介
Yosuke ITO
+81 80-5057-6931
glacier345@gmail.com
Last updated: Feb 22 2026 at 05:16 UTC