NEWS: move from CVC4 to cvc5

[Makarius]

*** HOL ***

* Sledgehammer:
   - Update of bundled provers:
       . cvc5 1.2.0 -- with support for arm64-linux


This refers to Isabelle/bbda3b4f3c99.


That is not just an update from version 4 to 5, but the change of spelling the 
name indicates that it is a quite different system.

One guy at Lean Together 2025, when talking about Sledgehammer and 
Magnushammer even put an exclamation mark at "Use cvc5!" (see minute 4:25 of 
https://www.youtube.com/watch?v=T9fhMJmJRAw&list=PLlF-CfQhukNlzXdQvu1SVt9vcD4--fLlg&index=20).


The support for arm64-linux was not available before, which is extra 
motivation to move on now. Thus we are almost complete in supporting that 
platform.

Testing cvc5 beforehand, we did encounter a few oddities concerning signals 
already, but lets hope that this workaround is now sufficient:

changeset:   81746:377887fbc968
user:        wenzelm
date:        Wed Jan 08 14:30:17 2025 +0100
files:       Admin/components/components.sha1 src/Pure/Admin/component_cvc5.scala
description:
rebuild cvc5 component (still inactive);
more robust workaround on all platforms, avoid crash of "sledgehammer [cvc5]" 
seen on x86_64-linux after line 75 of 
"$AFP/thys/Boolos_Curious_Inference_Automated/Boolos_Curious_Inference_Automated.thy";


It wraps everything into an outermost bash process, and refrains from using 
"exec" to make a "POSIX tail call". Thus the resulting process hierarchy looks 
more like a regular Terminal / shell process. (There are many fine points on 
process hierarchies and signals that can be done wrong. While I don't 
understand everything myself, I've seen enough bad approaches to be avoided.)


	Makarius