[isabelle-dev] NEWS: Zstd compression for Isabelle/Scala and Isabelle/ML

[Makarius]

*** ML ***

* Operations for Zstd compression (via Isabelle/Scala):

   Zstd.compress: Bytes.T -> Bytes.T
   Zstd.uncompress: Bytes.T -> Bytes.T


*** System ***

* Isabelle/Scala provides generic support for XZ and Zstd compression,
via Compress.Options and Compress.Cache. Bytes.uncompress automatically
detects the compression scheme.


This refers to Isabelle/f2b98eb6a7a9. See also 
https://github.com/luben/zstd-jni and https://github.com/facebook/zstd


Here is an example in Isabelle/ML (proper timing requires to re-check that 1-3 
times):


theory Scratch
   imports Pure
begin

ML ‹
   val b1 = Bytes.read @{file 
‹~~/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy›};
   val b2 = timeap Zstd.compress b1;
   val b3 = timeap Zstd.uncompress b2;
   @{assert} (Bytes.eq (b1, b3));
›

ML ‹
   val b1 = Bytes.read @{file 
‹~~/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy›};
   val b2 = timeap XZ.compress b1;
   val b3 = timeap XZ.uncompress b2;
   @{assert} (Bytes.eq (b1, b3));
›

end


This shows that Zstd (JNI library) is much faster than XZ (pure Java), while 
the compression ratio is only slightly lower.

It remains to be seen how we can use this super-fast compression, e.g. for 
blobs within build databases (presently XZ), or even for heaps of Poly/ML --- 
for the latter it might be better to see if this could be included in Poly/ML.


	Makarius