Stream: Mirror: Isabelle Development Mailing List

Topic: NEWS: uniform support for Message_Digest / SHA1 / SHA256 ...

Email Gateway (May 04 2026 at 19:42):

From: Makarius <makarius@sketis.net>

* 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

Last updated: May 15 2026 at 10:26 UTC