Email Gateway (Nov 06 2025 at 18:25): Email Gateway (Nov 06 2025 at 18:25):From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
While we are thinking about the next release, I thought I would bring up an intermittent issue. I use sledgehammer quite a lot, and sometimes things grind to a halt. Then I check the process monitor and find many copies of veriT seemingly looping. It's okay to just kill them. But I imagine this annoys a lot of people and I wonder if there is a way of preventing it. Does anybody else experience this?
Larry
Email Gateway (Nov 06 2025 at 18:50):From: Manuel Eberl <manuel@pruvisto.org>
When I taught the Concrete Semantics course in Innsbruck this summer a
lot of my students had this problem on Windows, often to the extent that
they had to frequently reboot their laptops because they would be
rendered unusable. I don't remember whether it was Isabelle 2024 or 2025
that caused that issue though.
I for one have not encountered that problem on Linux. It's possible that
my machine is just beefy enough that a few veriT processes running amok
isn't even noticeable, so not sure. But I did definitely get the
impression that the problem is much more pronounced on Windows.
Manuel
On 06/11/2025 19:24, Lawrence Paulson via isabelle-dev wrote:
While we are thinking about the next release, I thought I would bring up an intermittent issue. I use sledgehammer quite a lot, and sometimes things grind to a halt. Then I check the process monitor and find many copies of veriT seemingly looping. It's okay to just kill them. But I imagine this annoys a lot of people and I wonder if there is a way of preventing it. Does anybody else experience this?
Larry
Email Gateway (Nov 06 2025 at 19:18):From: Makarius <makarius@sketis.net>
On 06/11/2025 19:50, Manuel Eberl wrote:
When I taught the Concrete Semantics course in Innsbruck this summer a lot of
my students had this problem on Windows, often to the extent that they had to
frequently reboot their laptops because they would be rendered unusable. I
don't remember whether it was Isabelle 2024 or 2025 that caused that issue
though.
Yes, that was due to E Prover, mostly in Isabelle2024. For Isabelle2025 we've
had this NEWS item:
- Update of bundled provers:
. E 3.1 -- with patch on Windows/Cygwin for proper interrupts
It was due to bad project management on the side of Stephan Schulz: He had
accepted patches without looking closely enough.
Makarius
Email Gateway (Nov 06 2025 at 23:02):From: Peter Lammich <lammich@in.tum.de>
I've, very rarely, some zombie atp processes keeping my CPU nice and warm, and
my battery draining (on Linux). I typically just kill them manually.
Peter
On 6 Nov 2025 20:18, Makarius <makarius@sketis.net> wrote:
On 06/11/2025 19:50, Manuel Eberl wrote:
When I taught the Concrete Semantics course in Innsbruck this summer a
lot of
my students had this problem on Windows, often to the extent that they
had to
frequently reboot their laptops because they would be rendered unusable.
I
don't remember whether it was Isabelle 2024 or 2025 that caused that
issue
though.Yes, that was due to E Prover, mostly in Isabelle2024. For Isabelle2025
we've
had this NEWS item:\- Update of bundled provers:
. E 3.1 -- with patch on Windows/Cygwin for proper interruptsIt was due to bad project management on the side of Stephan Schulz: He had
accepted patches without looking closely enough.Makarius
Email Gateway (Nov 07 2025 at 10:14):From: Makarius <makarius@sketis.net>
On 07/11/2025 00:02, Peter Lammich wrote:
I've, very rarely, some zombie atp processes keeping my CPU nice and warm, and
my battery draining (on Linux). I typically just kill them manually.
So which ATPs (or SMTs) are they?
Makarius
Email Gateway (Nov 07 2025 at 10:50):From: Peter Lammich <lammich@in.tum.de>
On 07/11/2025 11:13, Makarius wrote:
On 07/11/2025 00:02, Peter Lammich wrote:
I've, very rarely, some zombie atp processes keeping my CPU nice and
warm, and my battery draining (on Linux). I typically just kill them
manually.So which ATPs (or SMTs) are they?
I do not remember, but will log them the next time I encounter one ...
(happens very rarely, as I said)
Makarius
Email Gateway (Nov 17 2025 at 12:23):From: Makarius <makarius@sketis.net>
On 06/11/2025 19:24, Lawrence Paulson via isabelle-dev wrote:
While we are thinking about the next release, I thought I would bring up an intermittent issue. I use sledgehammer quite a lot, and sometimes things grind to a halt. Then I check the process monitor and find many copies of veriT seemingly looping. It's okay to just kill them. But I imagine this annoys a lot of people and I wonder if there is a way of preventing it. Does anybody else experience this?
This thread is still pending: I am presently busy elsewhere, but will revisit
it later.
Just a brief summary of the situation in current Isabelle/4053d744316f. We have:
- new arm64-darwin executable, and x86_64-darwin executable, both built
afresh on our current platform baseline (macOS 12)
- replacement of the x86_64-windows executable: instead of our self-built
one from Oct-2021 (269a39b6c5f8), it is the official veriT download for
Windows --- thus we might have another chance to see old problems on Windows
disappear
- arm64-linux and x86_64-linux as before, unchanged
Some user of macOS 26 has reported privately, that the new arm64-darwin
executable does not make a difference, the problem persists.
To sort this out in time for the Isabelle2025-1 release, we first need a few
reproducible examples.
Makarius
Email Gateway (Nov 19 2025 at 22:23):From: Makarius <makarius@sketis.net>
On 17/11/2025 13:22, Makarius wrote:
This thread is still pending: I am presently busy elsewhere, but will revisit
it later.
Some user of macOS 26 has reported privately, that the new arm64-darwin
executable does not make a difference, the problem persists.To sort this out in time for the Isabelle2025-1 release, we first need a few
reproducible examples.
Same situation: I will busy for the next 2 days, and hope for someone else
(Larry?) to come up with reproducible examples with too many veriT processes
on macOS 26.
Makarius
Email Gateway (Nov 20 2025 at 11:49):From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
I have to say that it is rare. I use sledgehammer frequently (never try) and the odd thing is that usually you don't get any, but occasionally they seem to accumulate, almost as if a certain sort of proof interfered with correct termination. It's hard to imagine how that would work.
Larry
On 19 Nov 2025, at 22:22, Makarius <makarius@sketis.net> wrote:
Same situation: I will busy for the next 2 days, and hope for someone else (Larry?) to come up with reproducible examples with too many veriT processes on macOS 26.
Email Gateway (Nov 27 2025 at 15:32):From: Makarius <makarius@sketis.net>
On 19 Nov 2025, at 22:22, Makarius <makarius@sketis.net> wrote:
Same situation: I will busy for the next 2 days, and hope for someone else (Larry?) to come up with reproducible examples with too many veriT processes on macOS 26.
On 20/11/2025 12:49, Lawrence Paulson wrote:
I have to say that it is rare. I use sledgehammer frequently (never try)
and the odd thing is that usually you don't get any, but occasionally they
seem to accumulate, almost as if a certain sort of proof interfered with
correct termination. It's hard to imagine how that would work.
It still sounds like a serious problem, and I am still busy elsewhere. We do
need proper empirical proof / reproducible examples to sort it out.
Makarius
Email Gateway (Nov 27 2025 at 15:32):From: Makarius <makarius@sketis.net>
On 19 Nov 2025, at 22:22, Makarius <makarius@sketis.net> wrote:
Same situation: I will busy for the next 2 days, and hope for someone else (Larry?) to come up with reproducible examples with too many veriT processes on macOS 26.
On 20/11/2025 12:49, Lawrence Paulson wrote:
I have to say that it is rare. I use sledgehammer frequently (never try)
and the odd thing is that usually you don't get any, but occasionally they
seem to accumulate, almost as if a certain sort of proof interfered with
correct termination. It's hard to imagine how that would work.
It still sounds like a serious problem, and I am still busy elsewhere. We do
need proper empirical proof / reproducible examples to sort it out.
Makarius
Email Gateway (Nov 27 2025 at 15:38):From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
Right now I am running sledgehammer almost continuously and they are not showing up. I'm afraid it's just weird.
Larry
On 27 Nov 2025, at 15:32, Makarius <makarius@sketis.net> wrote:
It still sounds like a serious problem, and I am still busy elsewhere. We do need proper empirical proof / reproducible examples to sort it out.
Email Gateway (Nov 27 2025 at 15:38):From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
Right now I am running sledgehammer almost continuously and they are not showing up. I'm afraid it's just weird.
Larry
On 27 Nov 2025, at 15:32, Makarius <makarius@sketis.net> wrote:
It still sounds like a serious problem, and I am still busy elsewhere. We do need proper empirical proof / reproducible examples to sort it out.
Email Gateway (Nov 28 2025 at 15:39):From: Makarius <makarius@sketis.net>
On 27 Nov 2025, at 15:32, Makarius <makarius@sketis.net> wrote:
It still sounds like a serious problem, and I am still busy elsewhere. We do need proper empirical proof / reproducible examples to sort it out.
On 27/11/2025 16:37, Lawrence Paulson wrote:
Right now I am running sledgehammer almost continuously and they are not
showing up. I'm afraid it's just weird.
Did any other user of macOS 26 see veriT processes hanging around recently?
This question is relevant for the Isabelle2025-1 release, because macOS 26
is officially supported by it.
Makarius
Email Gateway (Nov 28 2025 at 15:56):From: Peter Lammich <lammich@in.tum.de>
On 07/11/2025 11:50, Peter Lammich wrote:
On 07/11/2025 11:13, Makarius wrote:
On 07/11/2025 00:02, Peter Lammich wrote:
I've, very rarely, some zombie atp processes keeping my CPU nice and
warm, and my battery draining (on Linux). I typically just kill them
manually.So which ATPs (or SMTs) are they?
I do not remember, but will log them the next time I encounter one ...
(happens very rarely, as I said)Just happened (on Isabelle2025) ... veriT keeping one CPU busy, and
using tons of memory. Manually killing the process helps.
PID USER PR NI VIRT RES SHR S %CPU %MEM TIME+
COMMAND
28257 peter 20 0 36.2g 31.1g 3084 R 99.7 33.1 7:03.43
veriT
On
Processor: Intel® Core™ Ultra 7
155H × 22
Graphics: Intel® Arc™ Graphics
(MTL)
Disk Capacity: 2.0 TB
Makarius
Email Gateway (Nov 28 2025 at 16:17):From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
As it is intermittent, I was wondering whether certain characteristics of the goal might cause this.
Is your example reproducible?
Larry
On 28 Nov 2025, at 15:56, Peter Lammich <lammich@in.tum.de> wrote:
Just happened (on Isabelle2025) ... veriT keeping one CPU busy, and using tons of memory. Manually killing the process helps.
Email Gateway (Nov 28 2025 at 16:40):From: Peter Lammich <lammich@in.tum.de>
On 28/11/2025 17:16, Lawrence Paulson wrote:
As it is intermittent, I was wondering whether certain characteristics of the goal might cause this.
Is your example reproducible?
Unfortunately not. I only realized that this process was running 7
minutes after it was started ... no idea what I was sledgehammering at
this point :(
I typically realize that only when I keep hearing my CPU fan, and my CPU
temperature keeps being high, although no proof or sledgehammer is running.
--
Peter
Larry
On 28 Nov 2025, at 15:56, Peter Lammich <lammich@in.tum.de> wrote:
Just happened (on Isabelle2025) ... veriT keeping one CPU busy, and using tons of memory. Manually killing the process helps.
Email Gateway (Nov 28 2025 at 16:57):From: Makarius <makarius@sketis.net>
On 28/11/2025 17:40, Peter Lammich wrote:
On 28/11/2025 17:16, Lawrence Paulson wrote:
As it is intermittent, I was wondering whether certain characteristics of
the goal might cause this.Is your example reproducible?
Unfortunately not. I only realized that this process was running 7 minutes
after it was started ... no idea what I was sledgehammering at this point :(I typically realize that only when I keep hearing my CPU fan, and my CPU
temperature keeps being high, although no proof or sledgehammer is running.
Peter,
that is new information: the problem happens on Linux, and for Isabelle2025
already. So it is not specific to macOS 26, nor to any changes towards
Isabelle2025-1.
I am still interested to learn about the reasons, but it is now more likely to
get ticked-off as "non-regression" towards Isabelle2025.
Makarius
Email Gateway (Nov 28 2025 at 19:57):From: Peter Lammich <lammich@in.tum.de>
Another one. veriT. Somewhere in my proof exploration of the below.
I'll try to re-sledgehammer all goals in there, maybe it provokes a
rogue veriT again...
--
Peter
imports Complex_Main
begin
lemma upt_fuse: "⟦l≤m; m<h ⟧ ⟹ [l..<m] @ [m..<h] = [l..<h]"
by (metis less_imp_add_positive upt_add_eq_append)
corollary harmonic_series_unbounded_aux: "n ≤ (∑i←[1..<2^(2*n)+1]. 1/i)"
proof -
have A: "(real n+1)/2 ≤ (∑i←[1..<2^n+1]. 1/i)" for n
proof (induction n)
case 0
then show ?case by simp
next
case (Suc n)
(* It feels like we're working against the simplifier for [_ ..<
Suc _], so we disable that rule *)
find_theorems "[_..<Suc _]"
note [simp del] = upt_Suc
have SPLIT: "[1..< 2^Suc n + 1] = [1..< 2^n + 1]@[2^n + 1 ..< 2^Suc
n + 1]" (is "_ = ?l1@?l2")
by (simp add: upt_fuse)
from Suc.IH have "(real n+1)/2 ≤ (∑i←?l1. 1/i)" .
moreover have "1/2 ≤ (∑i←?l2. 1/i)" proof -
have 1: "(1/2 :: real) ≤ (∑i←?l2. 1/2^Suc n)" by (simp add:
sum_list_triv)
have 2: "(∑i←?l2. 1/2^Suc n) ≤ (∑i←?l2. 1/i)"
apply (rule sum_list_mono)
apply (clarsimp simp: less_Suc_eq_le)
apply (drule of_nat_mono[where j="2*2^_"])
by (auto simp: field_simps)
from order_trans[OF 1 2] show ?thesis .
qed
ultimately show ?case
apply (subst SPLIT)
by simp
qed
show ?thesis
apply (rule order_trans[OF _ A])
by auto
qed
lemma harmonic_series_unbounded: "∃n. c ≤ (∑i←[1..<n]. 1/i)"
proof -
have "c ≤ (nat ¦⌈c⌉¦)" by linarith
also note harmonic_series_unbounded_aux
finally show ?thesis by blast
qed
On 28/11/2025 17:56, Makarius wrote:
On 28/11/2025 17:40, Peter Lammich wrote:
On 28/11/2025 17:16, Lawrence Paulson wrote:
As it is intermittent, I was wondering whether certain
characteristics of the goal might cause this.Is your example reproducible?
Unfortunately not. I only realized that this process was running 7
minutes after it was started ... no idea what I was sledgehammering
at this point :(I typically realize that only when I keep hearing my CPU fan, and my
CPU temperature keeps being high, although no proof or sledgehammer
is running.Peter,
that is new information: the problem happens on Linux, and for
Isabelle2025 already. So it is not specific to macOS 26, nor to any
changes towards Isabelle2025-1.I am still interested to learn about the reasons, but it is now more
likely to get ticked-off as "non-regression" towards Isabelle2025.Makarius
Email Gateway (Nov 28 2025 at 20:38):From: Manuel Eberl <manuel@pruvisto.org>
Just FYI, we have a lot of material on the harmonic numbers in the
distribution already. Including of course the fact that they're
unbounded. E.g. in HOL-Analysis.Summation_Tests:
lemma not_summable_harmonic: "¬summable (λn. inverse (of_nat n) :: 'a
:: real_normed_field)"
Or, expressed in a different way:
definition✐‹tag important› harm :: "nat ⇒ 'a :: real_normed_field" where
"harm n = (∑k=1..n. inverse (of_nat k))"
theorem not_convergent_harm: "¬convergent (harm :: nat ⇒ 'a ::
real_normed_field)"
Or a more precise lower bound:
lemma harm_ge_ln: "harm n ≥ ln (real n + 1)"
And a lot more.
Cheers,
Manuel
On 11/28/25 20:57, Peter Lammich wrote:
Another one. veriT. Somewhere in my proof exploration of the below.
I'll try to re-sledgehammer all goals in there, maybe it provokes a
rogue veriT again...--
Peter
imports Complex_Main
beginlemma upt_fuse: "⟦l≤m; m<h ⟧ ⟹ [l..<m] @ [m..<h] = [l..<h]"
by (metis less_imp_add_positive upt_add_eq_append)corollary harmonic_series_unbounded_aux: "n ≤ (∑i←[1..<2^(2*n)+1]. 1/i)"
proof -have A: "(real n+1)/2 ≤ (∑i←[1..<2^n+1]. 1/i)" for n
proof (induction n)
case 0
then show ?case by simp
next
case (Suc n)(* It feels like we're working against the simplifier for [_ ..<
Suc _], so we disable that rule *)
find_theorems "[_..<Suc _]"
note [simp del] = upt_Suchave SPLIT: "[1..< 2^Suc n + 1] = [1..< 2^n + 1]@[2^n + 1 ..<
2^Suc n + 1]" (is "_ = ?l1@?l2")
by (simp add: upt_fuse)from Suc.IH have "(real n+1)/2 ≤ (∑i←?l1. 1/i)" .
moreover have "1/2 ≤ (∑i←?l2. 1/i)" proof -
have 1: "(1/2 :: real) ≤ (∑i←?l2. 1/2^Suc n)" by (simp add:
sum_list_triv)
have 2: "(∑i←?l2. 1/2^Suc n) ≤ (∑i←?l2. 1/i)"
apply (rule sum_list_mono)
apply (clarsimp simp: less_Suc_eq_le)
apply (drule of_nat_mono[where j="2*2^_"])
by (auto simp: field_simps)
from order_trans[OF 1 2] show ?thesis .
qed
ultimately show ?case
apply (subst SPLIT)
by simp
qedshow ?thesis
apply (rule order_trans[OF _ A])
by auto
qedlemma harmonic_series_unbounded: "∃n. c ≤ (∑i←[1..<n]. 1/i)"
proof -
have "c ≤ (nat ¦⌈c⌉¦)" by linarith
also note harmonic_series_unbounded_aux
finally show ?thesis by blast
qedOn 28/11/2025 17:56, Makarius wrote:
On 28/11/2025 17:40, Peter Lammich wrote:
On 28/11/2025 17:16, Lawrence Paulson wrote:
As it is intermittent, I was wondering whether certain
characteristics of the goal might cause this.Is your example reproducible?
Unfortunately not. I only realized that this process was running 7
minutes after it was started ... no idea what I was sledgehammering
at this point :(I typically realize that only when I keep hearing my CPU fan, and my
CPU temperature keeps being high, although no proof or sledgehammer
is running.Peter,
that is new information: the problem happens on Linux, and for
Isabelle2025 already. So it is not specific to macOS 26, nor to any
changes towards Isabelle2025-1.I am still interested to learn about the reasons, but it is now more
likely to get ticked-off as "non-regression" towards Isabelle2025.Makarius
Last updated: Dec 10 2025 at 12:50 UTC