zombie proof processes

Makarius makarius at sketis.net
Fri Nov 28 17:56:23 CET 2025


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



More information about the isabelle-dev mailing list