Email Gateway (Jul 03 2026 at 13:15): Email Gateway (Jul 03 2026 at 13:15):From: Tobias Nipkow <nipkow@in.tum.de>
Hi,
I have started to nortice that sledgehammer creates these non-terminating veriT
processes on my Mac (MacOS 15.6.1). I had not noticed this before, although I am
using 2025-2 and have not updated my OS for some time now. I may just have
missed them, although that would be strange. In any case, I had always thought I
don't have this well-known problem, which is the only reason I am reporting it
here now.
Tobias
Email Gateway (Jul 03 2026 at 18:13):From: Makarius <makarius@sketis.net>
On 03/07/2026 15:15, Tobias Nipkow wrote:
I have started to nortice that sledgehammer creates these non-terminating
veriT processes on my Mac (MacOS 15.6.1). I had not noticed this before,
although I am using 2025-2 and have not updated my OS for some time now. I may
just have missed them, although that would be strange. In any case, I had
always thought I don't have this well-known problem, which is the only reason
I am reporting it here now.
It is indeed odd that we hardly ever encountered this problem in the past, but
see it more and more often now.
There will be definitely a change for the next release, Isabelle2026 (October
2026).
I have already had a brief look at the actual implementation, and found the
treatment of timeout a bit fragile.
Makarius
Email Gateway (Jul 03 2026 at 18:23):From: "\"Lammich, Peter (UT-EEMCS)\"" <cl-isabelle-users@lists.cam.ac.uk>
I'm also seeing the problem of spurious veriT processes on Ubuntu. They take one full core of compute, and I usually realise that my fan doesn't stop or the processor usage stays high even if I'm doing nothing. A killall veriT then 'solves' the problem quickly.
I remember that we had that topic some time ago already on this list.
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 Makarius <makarius@sketis.net>
Sent: Friday, 03 July 2026 20:12:06
To: Tobias Nipkow <nipkow@in.tum.de>; Isabelle Users List <cl-isabelle-users@lists.cam.ac.uk>
Subject: Re: [isabelle] veriT
On 03/07/2026 15:15, Tobias Nipkow wrote:
I have started to nortice that sledgehammer creates these non-terminating
veriT processes on my Mac (MacOS 15.6.1). I had not noticed this before,
although I am using 2025-2 and have not updated my OS for some time now. I may
just have missed them, although that would be strange. In any case, I had
always thought I don't have this well-known problem, which is the only reason
I am reporting it here now.
It is indeed odd that we hardly ever encountered this problem in the past, but
see it more and more often now.
There will be definitely a change for the next release, Isabelle2026 (October
2026).
I have already had a brief look at the actual implementation, and found the
treatment of timeout a bit fragile.
Makarius
Email Gateway (Jul 03 2026 at 18:26):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
They also have a tendency to go unstable, resulting of an invocation of the OOM killer.
Often poly ends up being the victim, forcing a restart of Isabelle.
On 7/3/26 14:23, "Lammich, Peter (UT-EEMCS)" (via cl-isabelle-users Mailing List) wrote:
I'm also seeing the problem of spurious veriT processes on Ubuntu. They take one full core of compute, and I usually
realise that my fan doesn't stop or the processor usage stays high even if I'm doing nothing. A killall veriT then
'solves' the problem quickly.I remember that we had that topic some time ago already on this list.
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 Makarius
<makarius@sketis.net>
Sent: Friday, 03 July 2026 20:12:06
To: Tobias Nipkow <nipkow@in.tum.de>; Isabelle Users List <cl-isabelle-users@lists.cam.ac.uk>
Subject: Re: [isabelle] veriTOn 03/07/2026 15:15, Tobias Nipkow wrote:
I have started to nortice that sledgehammer creates these non-terminating
veriT processes on my Mac (MacOS 15.6.1). I had not noticed this before,
although I am using 2025-2 and have not updated my OS for some time now. I may
just have missed them, although that would be strange. In any case, I had
always thought I don't have this well-known problem, which is the only reason
I am reporting it here now.It is indeed odd that we hardly ever encountered this problem in the past, but
see it more and more often now.There will be definitely a change for the next release, Isabelle2026 (October
2026).I have already had a brief look at the actual implementation, and found the
treatment of timeout a bit fragile.Makarius
Email Gateway (Jul 03 2026 at 18:34):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi all,
I don't know why killing does not work (I never managed to reproduce the
problem), but you could try to ask veriT to kill itself after 30s with:
declare [[verit_options = "--max-time=30"]]
This just adds the option to veriT without changing its solving
behavior. So it is compatible with Isabelle2025-2 and you could simply
remove the line for the upcoming Isabelle2026.
Mathias
On 7/3/26 20:26, Eugene W. Stark wrote:
They also have a tendency to go unstable, resulting of an invocation of the OOM killer.
Often poly ends up being the victim, forcing a restart of Isabelle.On 7/3/26 14:23, "Lammich, Peter (UT-EEMCS)" (via cl-isabelle-users Mailing List) wrote:
I'm also seeing the problem of spurious veriT processes on Ubuntu. They take one full core of compute, and I usually
realise that my fan doesn't stop or the processor usage stays high even if I'm doing nothing. A killall veriT then
'solves' the problem quickly.I remember that we had that topic some time ago already on this list.
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 Makarius
<makarius@sketis.net>
Sent: Friday, 03 July 2026 20:12:06
To: Tobias Nipkow <nipkow@in.tum.de>; Isabelle Users List <cl-isabelle-users@lists.cam.ac.uk>
Subject: Re: [isabelle] veriTOn 03/07/2026 15:15, Tobias Nipkow wrote:
I have started to nortice that sledgehammer creates these non-terminating
veriT processes on my Mac (MacOS 15.6.1). I had not noticed this before,
although I am using 2025-2 and have not updated my OS for some time now. I may
just have missed them, although that would be strange. In any case, I had
always thought I don't have this well-known problem, which is the only reason
I am reporting it here now.
It is indeed odd that we hardly ever encountered this problem in the past, but
see it more and more often now.There will be definitely a change for the next release, Isabelle2026 (October
2026).I have already had a brief look at the actual implementation, and found the
treatment of timeout a bit fragile.Makarius
Email Gateway (Jul 03 2026 at 18:37):From: Tobias Nipkow <nipkow@in.tum.de>
Peter, Just for the record: I was aware of your and Eugene's problems and had
only posted my problem because I wanted to add another OS to the collection
(having gotten the feeling macOS was immune).
Tobias
On 03/07/2026 20:23, Lammich, Peter (UT-EEMCS) wrote:
I'm also seeing the problem of spurious veriT processes on Ubuntu. They take one
full core of compute, and I usually realise that my fan doesn't stop or the
processor usage stays high even if I'm doing nothing. A killall veriT then
'solves' the problem quickly.I remember that we had that topic some time ago already on this list.
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 Makarius <makarius@sketis.net>
Sent: Friday, 03 July 2026 20:12:06
To: Tobias Nipkow <nipkow@in.tum.de>; Isabelle Users List <cl-isabelle-
users@lists.cam.ac.uk>
Subject: Re: [isabelle] veriT
On 03/07/2026 15:15, Tobias Nipkow wrote:I have started to nortice that sledgehammer creates these non-terminating
veriT processes on my Mac (MacOS 15.6.1). I had not noticed this before,
although I am using 2025-2 and have not updated my OS for some time now. I may
just have missed them, although that would be strange. In any case, I had
always thought I don't have this well-known problem, which is the only reason
I am reporting it here now.It is indeed odd that we hardly ever encountered this problem in the past, but
see it more and more often now.There will be definitely a change for the next release, Isabelle2026 (October
2026).I have already had a brief look at the actual implementation, and found the
treatment of timeout a bit fragile.Makarius
Last updated: Jul 22 2026 at 14:00 UTC