NEWS: uniform support for Message_Digest / SHA1 / SHA256 in Isabelle/ML/Scala

[Makarius]

*** ML ***

* Both SHA1 and SHA256 are supported via Isabelle/Scala, with minor
changes of the supported operations: Minor INCOMPATIBILITY. SHA1.fake
has been replaced by SHA1.parse (including proper checks). Structure
Message_Digest provides general operations. The native SHA1
implementation in ML has been discontinued, which may impact
performance.


*** System ***

* Both SHA1 and SHA256 are supported in Isabelle/Scala. SHA1 is still
used routinely, but will be eventually phased out. Result is of type
Message_Digest.T, with slightly different toString method. Subtle
INCOMPATIBILITY: use "rep" instead (as in Isabelle/ML).

This refers to Isabelle/50d7fead3758.


After dismantling parts of the old "use_thy" loader state, the ML operation 
SHA1.digest turned out to be unused (in Pure), so that was a good opportunity 
to dismantle our native SHA1 C-module for Poly/ML, and thus simplify the poly 
build process and make it more robust.

SHA1 remains relevant to some other Isabelle/ML tools (e.g. Sledgehammer, 
caches), but it now goes through the explicit ML-Scala-function protocol.


Adding SHA256 was an easy exercise in re-use of high-quality cryptographic 
algorithms on the JVM: We may use SHA256 routinely at a later stage, when SHA1 
has been generally discredited. There is no immediate need for action, though.

My motivation to provide SHA256 right now was a talk at FOSDEM 2026 about the 
next decade of git. The really interesting talks at that conference were 
non-git / post-git ones, see also https://fosdem.org/2026/schedule/track/main 
--- I did not attend this event in person, but a small open source event in 
Augsburg, where one post-git guy mentioned the very talk that I had watched 
myself some weeks before.


	Makarius