Email Gateway (Jan 26 2026 at 16:05): Email Gateway (Jan 26 2026 at 16:05):From: Gergely Buday <cl-isabelle-users@lists.cam.ac.uk>
Hi there,
I use Isabelle 2025-2 for a moderately large theory. With previous
versions I did not have any problem. Now Isabelle/jEdit crashed
several times when I invoked Sledgehammer. When viewing with top
afterwards, two or three veriT processes were there, running on 100%,
I had to kill them manually.
This was on an Ubuntu 22.04.
Is there any setting so that I could mitigate this problem?
Email Gateway (Jan 27 2026 at 12:24):From: Makarius <makarius@sketis.net>
On 26/01/2026 16:23, Gergely Buday (via cl-isabelle-users Mailing List) wrote:
I use Isabelle 2025-2 for a moderately large theory. With previous
versions I did not have any problem. Now Isabelle/jEdit crashed
several times when I invoked Sledgehammer. When viewing with top
afterwards, two or three veriT processes were there, running on 100%,
I had to kill them manually.This was on an Ubuntu 22.04.
What do you mean by "crashed"? Did the Java process actually crash? Or was it
merely the Java GUI that became non-responsive?
veriT processes hanging in the background were observed by a few people just
before the Isabelle2025-1 release, see Nov/Dec-2025 on the isabelle-dev
mailing list. At that point
https://mailman46.in.tum.de/pipermail/isabelle-dev/2025-November/018270.html I
concluded, that the problem has happened before in Isabelle2025, so there is
nothing further to do right now.
Is there any setting so that I could mitigate this problem?
How much RAM do you actually have?
Makarius
Email Gateway (Jan 27 2026 at 12:31):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Just to add to this, for what it's worth I have observed (with Isabelle 2025-1)
a 'veriT' process to go unstable and consume unbounded amounts of memory.
On my system, this typically causes the Linux OOM killer to nuke the 'poly'
process, which typically is using more memory, though it would actually be
better if it would nuke 'veriT' instead.
My system has 128GB of RAM. I limit the PolyML heap to 64GB and the Java heap
to 16GB. When veriT goes unstable, it will consume the rest.
- Gene Stark
On 1/27/26 07:24, Makarius wrote:
On 26/01/2026 16:23, Gergely Buday (via cl-isabelle-users Mailing List) wrote:
I use Isabelle 2025-2 for a moderately large theory. With previous
versions I did not have any problem. Now Isabelle/jEdit crashed
several times when I invoked Sledgehammer. When viewing with top
afterwards, two or three veriT processes were there, running on 100%,
I had to kill them manually.This was on an Ubuntu 22.04.
What do you mean by "crashed"? Did the Java process actually crash? Or was it merely the Java GUI that became non-
responsive?veriT processes hanging in the background were observed by a few people just before the Isabelle2025-1 release, see Nov/
Dec-2025 on the isabelle-dev mailing list. At that point https://mailman46.in.tum.de/pipermail/isabelle-dev/2025-
November/018270.html I concluded, that the problem has happened before in Isabelle2025, so there is nothing further to
do right now.Is there any setting so that I could mitigate this problem?
How much RAM do you actually have?
Makarius
Email Gateway (Jan 27 2026 at 12:47):From: Bryan Alexander Ford <cl-isabelle-users@lists.cam.ac.uk>
I can confirm that I have been experiencing this problem intermittently and nondeterministically, but quite regularly, throughout most of 2025 at least, using Isabelle2025 for Mac. (I can’t remember for sure if I experienced it with Isabelle2024 before the upgrade from that.). The problem became frequent enough that I have been habitually keeping an Activity Monitor window open alongside Isabelle, in order to notice when there are veriT threads still crunching on something when all sledgehammer activity is supposed to be stopped. Quitting and restarting Isabelle entirely in that case always proved to be an easy workaround so I assumed it was a well-known issue and didn’t pay much attention to it.
Although the issue is certainly highly nondeterministic and I couldn’t promise to reproduce it reliably “on demand”, if there is some debug tooling anyone would like to suggest I enable in order to “catch it in the act” and get better information about what’s going on when this happens in the future, I’d be happy to do that.
Thanks
Bryan
On 27 Jan 2026, at 13:24, Makarius <makarius@sketis.net> wrote:
On 26/01/2026 16:23, Gergely Buday (via cl-isabelle-users Mailing List) wrote:
I use Isabelle 2025-2 for a moderately large theory. With previous
versions I did not have any problem. Now Isabelle/jEdit crashed
several times when I invoked Sledgehammer. When viewing with top
afterwards, two or three veriT processes were there, running on 100%,
I had to kill them manually.
This was on an Ubuntu 22.04.What do you mean by "crashed"? Did the Java process actually crash? Or was it merely the Java GUI that became non-responsive?
veriT processes hanging in the background were observed by a few people just before the Isabelle2025-1 release, see Nov/Dec-2025 on the isabelle-dev mailing list. At that point https://mailman46.in.tum.de/pipermail/isabelle-dev/2025-November/018270.html I concluded, that the problem has happened before in Isabelle2025, so there is nothing further to do right now.
Is there any setting so that I could mitigate this problem?
How much RAM do you actually have?
Makarius
Email Gateway (Jan 27 2026 at 13:38):From: Makarius <makarius@sketis.net>
On 27/01/2026 13:46, Bryan Alexander Ford wrote:
I can confirm that I have been experiencing this problem intermittently and nondeterministically, but quite regularly, throughout most of 2025 at least, using Isabelle2025 for Mac.
Thanks for the report. I take this as another confirmation that it is an old
problem from Isabelle2025 (March 2025) at the least, so I was right not to
attempt any changes in the last minute before Isabelle2025-1 (December 2025),
which is now superseded by Isabelle2025-2 (Jan-2026).
The window of opportunity to address old problems on the spot is usually
between RC0 (4 weeks before RC1), actual RC1, sometimes until RC2 (2 weeks
after RC1). Between the releases, it is up to maintainers of Isabelle
subsystems to do or not do anything --- eventually or later.
Here is the timetable for the next release:
https://sketis.net/2025/plan-for-isabelle2026-october-2026
Generally note, that the Isabelle infrastructure does provide some means to
manage process groups via the "session id" from POSIX/BSD, but processes may
choose to leave that context later on, and can no longer be controlled. This
approach is not bullet-proof: generic POSIX cannot do any better.
In contrast, we do see proper process tree management in Docker (on Linux,
macOS, Windows), so there must be platform-specific mechanisms to implement
that properly.
Maybe someone has some hints on that, or some example applications with
external processes where this is done successfully.
Makarius
Email Gateway (Jan 27 2026 at 19:05):From: Makarius <makarius@sketis.net>
On 27/01/2026 14:37, Makarius wrote:
In contrast, we do see proper process tree management in Docker (on Linux,
macOS, Windows), so there must be platform-specific mechanisms to implement
that properly.Maybe someone has some hints on that, or some example applications with
external processes where this is done successfully.
Just to answer my own question, after browsing the web for approx. 2h: The
Bazel code base (version 3ad9562ae006) has some notable implementations. E.g.
linux-sandbox:
https://github.com/bazelbuild/bazel/blob/master/src/main/tools/linux-sandbox-pid1.cc
https://github.com/bazelbuild/bazel/blob/master/src/main/tools/linux-sandbox.cc
That looks promising due to the "PID namespace" of the Linux kernel. It is
lacking portability, though. The macOS situation is much weaker:
https://github.com/bazelbuild/bazel/blob/master/src/main/tools/process-tools-darwin.cc
https://github.com/bazelbuild/bazel/blob/master/src/main/tools/process-tools-linux.cc
The Windows situation is totally unclear to me: maybe that platform has its
own (better?) ways to manage process trees.
Anyway, we better stick with our good old bash_process wrapper for now, and
sort out the problems of veriT before the next Isabelle release.
Makarius
Email Gateway (Jan 27 2026 at 20:24):From: Makarius <makarius@sketis.net>
On 27/01/2026 20:05, Makarius wrote:
That looks promising due to the "PID namespace" of the Linux kernel. It is
lacking portability, though. The macOS situation is much weaker:https://github.com/bazelbuild/bazel/blob/master/src/main/tools/process-tools-
darwin.cc
https://github.com/bazelbuild/bazel/blob/master/src/main/tools/process-tools-
linux.cc
Here is a blog entry (from 2019) that appears to be related to the above
sources: https://jmmv.dev/2019/11/wait-for-process-group-darwin.html
Quote from the bottom:
"""
However, be aware that this solution is not bullet-proof: if a subprocess
creates a new process group, it will escape our algorithm and there is nothing
we can do about it. (It looks like FreeBSD has a NOTE_TRACK event that could
let us track those processes… but of course this doesn’t exist on Darwin.)
Anyway, in the context of Bazel’s process wrapper, we are willing to live with
this limitation.
"""
That sounds familiar. We have been living with these process group limitations
for decades.
The Windows situation is totally unclear to me: maybe that platform has its
own (better?) ways to manage process trees.
I have briefly tried the Windows Sysinternals Process Explorer
https://learn.microsoft.com/en-us/sysinternals/downloads/process-explorer
The result on running Isabelle.exe: various bash and poly processes show up as
independent roots, with their own subtrees. So it looks like the model on
Windows is as bad as generic Unix.
Anyway, we better stick with our good old bash_process wrapper for now, and
sort out the problems of veriT before the next Isabelle release.
Conclusion unchanged.
Makarius
Email Gateway (Jan 28 2026 at 09:10):From: Fabian Huch <huch@in.tum.de>
On 1/27/26 20:05, Makarius wrote:
On 27/01/2026 14:37, Makarius wrote:
In contrast, we do see proper process tree management in Docker (on
Linux, macOS, Windows), so there must be platform-specific mechanisms
to implement that properly.Maybe someone has some hints on that, or some example applications
with external processes where this is done successfully.Just to answer my own question, after browsing the web for approx. 2h:
The Bazel code base (version 3ad9562ae006) has some notable
implementations. E.g. linux-sandbox:https://github.com/bazelbuild/bazel/blob/master/src/main/tools/linux-sandbox-pid1.cc
https://github.com/bazelbuild/bazel/blob/master/src/main/tools/linux-sandbox.cc
That looks promising due to the "PID namespace" of the Linux kernel.
It is lacking portability, though.
There are also portability problems within Linux: PID namespaces alone
(CLONE_NEWPID) can only be created by a privileged process. Hence we
need to create them as user namespace (CLONE_NEWUSER) -- like in the
example -- but this may be a problem with some older linux versions: The
feature was introduced in Kernel 3.8.0, but some distributions used to
not have them enabled by default (kernel flag CONFIG_USER_NS) due to
security concerns.
Fabian
Email Gateway (Jan 28 2026 at 09:39):From: Gergely Buday <cl-isabelle-users@lists.cam.ac.uk>
Sorry, I did not include this from my terminal, which is displayed at
crashing. And yes, crashing as the whole Isabelle/jEdit was shut down.
environment: line 1: 5788 Killed "$JAVA_HOME/bin/$PRG" "$@"
On Tue, 27 Jan 2026 at 12:24, Makarius <makarius@sketis.net> wrote:
On 26/01/2026 16:23, Gergely Buday (via cl-isabelle-users Mailing List) wrote:
I use Isabelle 2025-2 for a moderately large theory. With previous
versions I did not have any problem. Now Isabelle/jEdit crashed
several times when I invoked Sledgehammer. When viewing with top
afterwards, two or three veriT processes were there, running on 100%,
I had to kill them manually.This was on an Ubuntu 22.04.
What do you mean by "crashed"? Did the Java process actually crash? Or was it
merely the Java GUI that became non-responsive?veriT processes hanging in the background were observed by a few people just
before the Isabelle2025-1 release, see Nov/Dec-2025 on the isabelle-dev
mailing list. At that point
https://mailman46.in.tum.de/pipermail/isabelle-dev/2025-November/018270.html I
concluded, that the problem has happened before in Isabelle2025, so there is
nothing further to do right now.Is there any setting so that I could mitigate this problem?
How much RAM do you actually have?
Makarius
Email Gateway (Jan 28 2026 at 09:40):From: Makarius <makarius@sketis.net>
On 28/01/2026 10:38, Gergely Buday (via cl-isabelle-users Mailing List) wrote:
Sorry, I did not include this from my terminal, which is displayed at
crashing. And yes, crashing as the whole Isabelle/jEdit was shut down.environment: line 1: 5788 Killed "$JAVA_HOME/bin/$PRG" "$@"
Thanks.
That is the usual "out-of-memory kill" on Linux, and thus not really a crash.
Makarius
Email Gateway (Jan 28 2026 at 10:02):From: Gergely Buday <cl-isabelle-users@lists.cam.ac.uk>
On Tue, 27 Jan 2026 at 12:24, Makarius <makarius@sketis.net> wrote:
On 26/01/2026 16:23, Gergely Buday (via cl-isabelle-users Mailing List) wrote:
Is there any setting so that I could mitigate this problem?
How much RAM do you actually have?
16 Gigabytes.
Email Gateway (Jan 28 2026 at 12:11):From: Makarius <makarius@sketis.net>
On 28/01/2026 11:01, Gergely Buday (via cl-isabelle-users Mailing List) wrote:
On Tue, 27 Jan 2026 at 12:24, Makarius <makarius@sketis.net> wrote:
On 26/01/2026 16:23, Gergely Buday (via cl-isabelle-users Mailing List) wrote:
Is there any setting so that I could mitigate this problem?
How much RAM do you actually have?
16 Gigabytes.
OK. It is the standard size for current Isabelle, so it needs to work
properly, i.e. we need to improve the veriT situation.
Makarius
Last updated: Jan 31 2026 at 12:53 UTC