--- 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
--- 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
--- 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 \
--- /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)
+ })
+}
--- 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)
--- 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
--- /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")
+ }
+}
--- 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,