Yosuke Ito (May 10 2026 at 08:23): Yosuke Ito (May 10 2026 at 08:23):I think the the zombie veriT process problem still remains in Isabelle2025-2. I changed the setting of SLEDGEHAMMER_PROVERS to exclude veriT. The command
isabelle getenv SLEDGEHAMMER_PROVERS
produces
SLEDGEHAMMER_PROVERS=cvc5 z3 e spass vampire zipperposition
as desired. However, when I invoke sledgehammer, veriT pops up again, and goes into an infinite loop in the background. How can I disable veriT altogether?
Mathias Fleury (May 12 2026 at 20:13):https://isabelle.in.tum.de/dist/Isabelle2025-2/doc/sledgehammer.pdf, so sledgehammer_params[prover=...]
Mathias Fleury (May 12 2026 at 20:14):that being said, sledgehammer will try to reconstruct goals with the smt tactic and that is not option controlled. You could use no_smt_proofs, but that also deactivates z3.
Mathias Fleury (May 12 2026 at 20:15):Alternatively, you could add the option --max-time=30 to veriT
Mathias Fleury (May 12 2026 at 20:16):declare [[verit_options = "--proof-with-sharing --max-time=30"]]
That way, you keep everything working, but veriT should kill itself after 30s if isabelle killing fails
Mathias Fleury (May 12 2026 at 20:16):I really would like to know why killing processes is not working
Lukas Stevens (May 12 2026 at 20:36):This is probably because veriT lets subprocesses escape its PID group.
Mathias Fleury (May 13 2026 at 04:48):veriT does not use subprocesses
Yosuke Ito (May 13 2026 at 09:52):@Mathias Fleury
Thank you very much for your help. I'll try this one.
declare [[verit_options = "--proof-with-sharing --max-time=30"]]
I was wondering if Isabelle hol has ever been utilized to verify and validated video game source code in C??? this might be a ridiculous question.
Last updated: May 17 2026 at 06:46 UTC