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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
