zombie proof processes

Makarius makarius at sketis.net
Thu Nov 27 16:32:01 CET 2025


>> On 19 Nov 2025, at 22:22, Makarius <makarius at 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



More information about the isabelle-dev mailing list