# HG changeset patch
# User wenzelm
# Date 1666343281 -7200
# Node ID a15f16e8ad18c8a2271099a0b97cb22e119cbb78
# Parent  fa30620e31bfbe016f9ce9e3d5d688b213cac821
support for Zstd data compression;

diff -r fa30620e31bf -r a15f16e8ad18 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Thu Oct 20 23:46:49 2022 +0200
+++ b/Admin/components/components.sha1	Fri Oct 21 11:08:01 2022 +0200
@@ -516,3 +516,4 @@
 b884c60653002a7811e3b652ae0515e825d98667 zipperposition-2.0.tar.gz
 b129ec4f8a4474953ec107536298ee08a01fbebc zipperposition-2.1-1.tar.gz
 5f53a77efb5cbe9d0c95d74a1588cc923bd711a7 zipperposition-2.1.tar.gz
+c101182780aeafbc2e0ea7e8b10b91c6f7483af2 zstd-jni-1.5.2-5.tar.gz
diff -r fa30620e31bf -r a15f16e8ad18 Admin/components/main
--- a/Admin/components/main	Thu Oct 20 23:46:49 2022 +0200
+++ b/Admin/components/main	Fri Oct 21 11:08:01 2022 +0200
@@ -34,3 +34,4 @@
 xz-java-1.9
 z3-4.4.0_4.4.1
 zipperposition-2.1-1
+zstd-jni-1.5.2-5
diff -r fa30620e31bf -r a15f16e8ad18 etc/build.props
--- a/etc/build.props	Thu Oct 20 23:46:49 2022 +0200
+++ b/etc/build.props	Fri Oct 21 11:08:01 2022 +0200
@@ -34,6 +34,7 @@
   src/Pure/Admin/build_vampire.scala \
   src/Pure/Admin/build_verit.scala \
   src/Pure/Admin/build_zipperposition.scala \
+  src/Pure/Admin/build_zstd.scala \
   src/Pure/Admin/check_sources.scala \
   src/Pure/Admin/ci_build.scala \
   src/Pure/Admin/isabelle_cronjob.scala \
@@ -100,6 +101,7 @@
   src/Pure/General/value.scala \
   src/Pure/General/word.scala \
   src/Pure/General/xz.scala \
+  src/Pure/General/zstd.scala \
   src/Pure/Isar/document_structure.scala \
   src/Pure/Isar/keyword.scala \
   src/Pure/Isar/line_structure.scala \
diff -r fa30620e31bf -r a15f16e8ad18 src/Pure/Admin/build_zstd.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/build_zstd.scala	Fri Oct 21 11:08:01 2022 +0200
@@ -0,0 +1,119 @@
+/*  Title:      Pure/Admin/build_zstd.scala
+    Author:     Makarius
+
+Build Isabelle zstd-jni component from official download.
+*/
+
+package isabelle
+
+
+object Build_Zstd {
+  /* platforms */
+
+  sealed case class Platform(name: String, template: String, exe: Boolean = false) {
+    def install(jar_dir: Path, component_dir: Path, version: String): Unit = {
+      val source = jar_dir + Path.explode(template.replace("{V}", version))
+      val target = Isabelle_System.make_directory(component_dir + Path.basic(name))
+      Isabelle_System.copy_file(source, target)
+      if (exe) File.set_executable(target + source.base, true)
+    }
+  }
+
+  private val platforms =
+    List(
+      Platform("arm64-darwin", "darwin/aarch64/libzstd-jni-{V}.dylib"),
+      Platform("x86_64-darwin", "darwin/x86_64/libzstd-jni-{V}.dylib"),
+      Platform("arm64-linux", "linux/aarch64/libzstd-jni-{V}.so"),
+      Platform("x86_64-linux", "linux/amd64/libzstd-jni-{V}.so"),
+      Platform("x86_64-windows", "win/amd64/libzstd-jni-{V}.dll", exe = true))
+
+
+  /* build zstd */
+
+  val license_url = "https://raw.githubusercontent.com/luben/zstd-jni/master/LICENSE"
+  val default_download_url = "https://repo1.maven.org/maven2/com/github/luben/zstd-jni"
+  val default_version = "1.5.2-5"
+
+  def build_zstd(
+    target_dir: Path = Path.current,
+    download_url: String = default_download_url,
+    version: String = default_version,
+    progress: Progress = new Progress,
+  ): Unit = {
+    /* component */
+
+    val component_name = "zstd-jni-" + version
+    val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component_name))
+    progress.echo("Component " + component_dir)
+
+    File.write(component_dir + Path.basic("README"),
+      "This is " + component_name + " from\n" + download_url +
+        "\n\n        Makarius\n        " + Date.Format.date(Date.now()) + "\n")
+
+    Isabelle_System.download_file(
+      license_url, component_dir + Path.basic("LICENSE"), progress = progress)
+
+
+    /* jar */
+
+    val jar_name = component_name + ".jar"
+    val jar = component_dir + Path.basic(jar_name)
+    Isabelle_System.download_file(
+      download_url + "/" + version + "/" + jar_name, jar, progress = progress)
+
+    Isabelle_System.with_tmp_dir("build") { jar_dir =>
+      progress.echo("Unpacking " + jar)
+      Isabelle_System.bash("isabelle_jdk jar xf " + File.bash_path(jar.absolute),
+        cwd = jar_dir.file).check
+      for (platform <- platforms) platform.install(jar_dir, component_dir, version)
+    }
+
+
+    /* settings */
+
+    val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
+
+    File.write(etc_dir + Path.basic("settings"),
+"""# -*- shell-script -*- :mode=shellscript:
+
+ISABELLE_ZSTD_HOME="$COMPONENT"
+
+classpath "$ISABELLE_ZSTD_HOME/""" + jar_name + """"
+""")
+  }
+
+
+  /* Isabelle tool wrapper */
+
+  val isabelle_tool =
+    Isabelle_Tool("build_zstd", "build Isabelle zstd-jni component from official download",
+      Scala_Project.here,
+      { args =>
+        var target_dir = Path.current
+        var download_url = default_download_url
+        var version = default_version
+
+        val getopts = Getopts("""
+Usage: isabelle build_zstd [OPTIONS]
+
+  Options are:
+    -D DIR       target directory (default ".")
+    -U URL       download URL (default: """ + quote(default_download_url) + """)
+    -V VERSION   version (default: """ + quote(default_version) + """)
+
+  Build zstd-jni component from the specified download base URL and VERSION,
+  see also https://github.com/luben/zstd-jni
+""",
+          "D:" -> (arg => target_dir = Path.explode(arg)),
+          "U:" -> (arg => download_url = arg),
+          "V:" -> (arg => version = arg))
+
+        val more_args = getopts(args)
+        if (more_args.nonEmpty) getopts.usage()
+
+        val progress = new Console_Progress()
+
+        build_zstd(target_dir = target_dir, download_url = download_url,
+          version = version, progress = progress)
+      })
+}
diff -r fa30620e31bf -r a15f16e8ad18 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Thu Oct 20 23:46:49 2022 +0200
+++ b/src/Pure/General/file.scala	Fri Oct 21 11:08:01 2022 +0200
@@ -19,6 +19,8 @@
 
 import org.tukaani.xz.{XZInputStream, XZOutputStream}
 
+import com.github.luben.zstd.{ZstdInputStream, ZstdOutputStream}
+
 import scala.collection.mutable
 
 
@@ -85,6 +87,7 @@
   def is_thy(s: String): Boolean = s.endsWith(".thy")
   def is_xz(s: String): Boolean = s.endsWith(".xz")
   def is_zip(s: String): Boolean = s.endsWith(".zip")
+  def is_zst(s: String): Boolean = s.endsWith(".zst")
 
   def is_backup(s: String): Boolean = s.endsWith("~") || s.endsWith(".orig")
 
@@ -197,6 +200,12 @@
     read_stream(new XZInputStream(new BufferedInputStream(new FileInputStream(file))))
   def read_xz(path: Path): String = read_xz(path.file)
 
+  def read_zstd(file: JFile): String = {
+    Zstd.init_jni
+    read_stream(new ZstdInputStream(new BufferedInputStream(new FileInputStream(file))))
+  }
+  def read_zstd(path: Path): String = read_zstd(path.file)
+
 
   /* read lines */
 
@@ -247,6 +256,12 @@
     write_xz(path.file, text, options)
   def write_xz(path: Path, text: String): Unit = write_xz(path, text, XZ.options())
 
+  def write_zstd(file: JFile, text: String): Unit = {
+    Zstd.init_jni
+    write_file(file, text, (s: OutputStream) => new ZstdOutputStream(new BufferedOutputStream(s)))
+  }
+  def write_zstd(path: Path, text: String): Unit = write_zstd(path.file, text)
+
   def write_backup(path: Path, text: String): Unit = {
     if (path.is_file) Isabelle_System.move_file(path, path.backup)
     write(path, text)
diff -r fa30620e31bf -r a15f16e8ad18 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Thu Oct 20 23:46:49 2022 +0200
+++ b/src/Pure/General/path.scala	Fri Oct 21 11:08:01 2022 +0200
@@ -240,6 +240,7 @@
   def orig: Path = ext("orig")
   def patch: Path = ext("patch")
   def shasum: Path = ext("shasum")
+  def zst: Path = ext("zst")
 
   def backup: Path = {
     val (prfx, s) = split_path
diff -r fa30620e31bf -r a15f16e8ad18 src/Pure/General/zstd.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/zstd.scala	Fri Oct 21 11:08:01 2022 +0200
@@ -0,0 +1,23 @@
+/*  Title:      Pure/General/xz.scala
+    Author:     Makarius
+
+Support for Zstd data compression.
+*/
+
+package isabelle
+
+
+object Zstd {
+  lazy val init_jni: Unit = {
+    val lib_dir = Path.explode("$ISABELLE_ZSTD_HOME/" + Platform.jvm_platform)
+    val lib_file =
+      File.find_files(lib_dir.file) match {
+        case List(file) => file
+        case _ => error("Exactly one file expected in directory " + lib_dir.expand)
+      }
+    System.load(File.platform_path(lib_file.getAbsolutePath))
+    com.github.luben.zstd.util.Native.assumeLoaded()
+    assert(com.github.luben.zstd.util.Native.isLoaded())
+    Class.forName("com.github.luben.zstd.Zstd")
+  }
+}
diff -r fa30620e31bf -r a15f16e8ad18 src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Thu Oct 20 23:46:49 2022 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Fri Oct 21 11:08:01 2022 +0200
@@ -175,6 +175,7 @@
   Build_Vampire.isabelle_tool,
   Build_VeriT.isabelle_tool,
   Build_Zipperposition.isabelle_tool,
+  Build_Zstd.isabelle_tool,
   Check_Sources.isabelle_tool,
   Components.isabelle_tool,
   isabelle.vscode.Build_VSCode.isabelle_tool,