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
Last updated: Nov 16 2025 at 12:39 UTC