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

[Makarius]

On 21/10/2022 20:02, Makarius wrote:
> 
> Here is an example in Isabelle/ML

Here the same example for Isabelle/Scala, e.g. the Console/Scala plugin in 
Isabelle/jEdit:

val b1 = 
Bytes.read(Path.explode("~~/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy"))
val b2 = Timing.timeit() { b1.compress(Compress.Options_Zstd()) }
val b3 = Timing.timeit() { b2.uncompress() }

val b1 = 
Bytes.read(Path.explode("~~/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy"))
val b2 = Timing.timeit() { b1.compress(Compress.Options_XZ()) }
val b3 = Timing.timeit() { b2.uncompress() }


It shows how Isabelle/ML (world of mathematics) and Isabelle/Scala (world of 
physics) nicely work together. The ML functions from before actually invoke 
these Scala operations via the PIDE protocol channel, using a custom-made 
Bytes type on both sides (for better scalability).


	Makarius