zombie proof processes

[Makarius]

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