zombie proof processes

Manuel Eberl manuel at pruvisto.org
Thu Nov 6 19:50:08 CET 2025


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
>


More information about the isabelle-dev mailing list