zombie proof processes: veriT

[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?

I have made a pro-forma update of the verit component for macOS:

changeset:   83544:d1a66e53c15c
tag:         tip
user:        wenzelm
date:        Mon Nov 10 22:28:18 2025 +0100
summary:     rebuild "verit" for arm64-darwin (new) and x86_64-darwin, using 
current platform baseline (macOS 12);


I had done that before for Linux:

changeset:   79563:76ad72736e9e
user:        wenzelm
date:        Wed Jan 31 22:36:12 2024 +0100
files:       Admin/components/PLATFORMS Admin/components/components.sha1 
Admin/components/main
description:
rebuild "verit" for arm64-linux for more robustness, e.g. relevant for theory 
"HOL-ex.BigO";
uniform baseline for "linux" and "linux_arm";


That was always the same veriT version from 4 years ago:

changeset:   74812:ed3adabf0dbe
user:        wenzelm
date:        Fri Nov 19 20:35:35 2021 +0100
files:       Admin/components/components.sha1 Admin/components/main 
src/Pure/Admin/build_verit.scala
description:
updated to verit-2021.06.2-rmx;


... actually from 5 years ago, see https://verit.loria.fr/download

Under the heading "UNSTABLE" I see this notable Changelog entry:

- veriT now always returns with an error code 14 in case of a timeout and
   24 in case of a CPU timeout (when available).  This is independent of
   the operating system.

Maybe that helps. So it might be a good time to prompt the veriT guys to make 
a new stable release eventually. (The sledgehammer and/or SMT guys need to do 
this.)


	Makarius