--- a/Admin/components/components.sha1 Thu Oct 20 14:43:29 2022 +0200
+++ b/Admin/components/components.sha1 Sat Oct 22 18:47:48 2022 +0200
@@ -158,6 +158,7 @@
056979bd1c08eb9d0d12cc1118b4ff70bfe2d594 isabelle_setup-20220701.tar.gz
be91402b3e5ef5bc6d4802a45175ee238cd9653e isabelle_setup-20220808.tar.gz
171df3eb58bdac4cc495f773b797fa578f7d4be6 isabelle_setup-20220817.tar.gz
+7b1ce9bd85e33076fa7022eeb66ce15915d078d9 isabelle_setup-20221020.tar.gz
0b2206f914336dec4923dd0479d8cee4b904f544 jdk-11+28.tar.gz
e12574d838ed55ef2845acf1152329572ab0cc56 jdk-11.0.10+9.tar.gz
3e05213cad47dbef52804fe329395db9b4e57f39 jdk-11.0.2+9.tar.gz
@@ -515,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 14:43:29 2022 +0200
+++ b/Admin/components/main Sat Oct 22 18:47:48 2022 +0200
@@ -9,7 +9,7 @@
flatlaf-2.4
idea-icons-20210508
isabelle_fonts-20211004
-isabelle_setup-20220817
+isabelle_setup-20221020
jdk-17.0.4.1+1
jedit-20211103
jfreechart-1.5.3
@@ -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/NEWS Thu Oct 20 14:43:29 2022 +0200
+++ b/NEWS Sat Oct 22 18:47:48 2022 +0200
@@ -50,6 +50,22 @@
- Added lemma wfP_subset_mset[simp].
+*** 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.
+
+
+
New in Isabelle2022 (October 2022)
----------------------------------
--- a/bin/isabelle_java Thu Oct 20 14:43:29 2022 +0200
+++ b/bin/isabelle_java Sat Oct 22 18:47:48 2022 +0200
@@ -64,7 +64,7 @@
exit 127
else
unset ISABELLE_HOME
- unset CLASSPATH
+ export CLASSPATH=""
exec "$JAVA_HOME/bin/java" "${JAVA_ARGS[@]}" \
-classpath "$ISABELLE_CLASSPATH" "$@"
fi
--- a/etc/build.props Thu Oct 20 14:43:29 2022 +0200
+++ b/etc/build.props Sat Oct 22 18:47:48 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 \
@@ -62,6 +63,7 @@
src/Pure/General/codepoint.scala \
src/Pure/General/comment.scala \
src/Pure/General/completion.scala \
+ src/Pure/General/compress.scala \
src/Pure/General/csv.scala \
src/Pure/General/date.scala \
src/Pure/General/exn.scala \
@@ -99,7 +101,7 @@
src/Pure/General/uuid.scala \
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 \
--- a/lib/Tools/java Thu Oct 20 14:43:29 2022 +0200
+++ b/lib/Tools/java Sat Oct 22 18:47:48 2022 +0200
@@ -7,7 +7,7 @@
eval "declare -a JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS)"
classpath "$ISABELLE_SETUP_CLASSPATH"; unset ISABELLE_SETUP_CLASSPATH
-classpath "$CLASSPATH"; unset CLASSPATH
+classpath "$CLASSPATH"; export CLASSPATH=""
isabelle_java java "${JAVA_ARGS[@]}" \
-classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@"
--- a/lib/Tools/scala Thu Oct 20 14:43:29 2022 +0200
+++ b/lib/Tools/scala Sat Oct 22 18:47:48 2022 +0200
@@ -7,7 +7,7 @@
isabelle scala_build || exit $?
classpath "$ISABELLE_SETUP_CLASSPATH"; unset ISABELLE_SETUP_CLASSPATH
-classpath "$CLASSPATH"; unset CLASSPATH
+classpath "$CLASSPATH"; export CLASSPATH=""
export jvm_cp_args="$(platform_path "$ISABELLE_CLASSPATH")"
export JAVA_OPTS="$ISABELLE_JAVA_SYSTEM_OPTIONS -J-Dscala.usejavacp=true"
--- a/lib/Tools/scala_build Thu Oct 20 14:43:29 2022 +0200
+++ b/lib/Tools/scala_build Sat Oct 22 18:47:48 2022 +0200
@@ -57,7 +57,7 @@
"$ISABELLE_HOME/lib/classes/Pure.shasum" \
"$ISABELLE_HOME/src/Tools/jEdit/dist"
-classpath "$CLASSPATH"; unset CLASSPATH
+classpath "$CLASSPATH"; export CLASSPATH=""
eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS)"
--- a/lib/Tools/scalac Thu Oct 20 14:43:29 2022 +0200
+++ b/lib/Tools/scalac Sat Oct 22 18:47:48 2022 +0200
@@ -7,7 +7,7 @@
isabelle scala_build || exit $?
classpath "$ISABELLE_SETUP_CLASSPATH"; unset ISABELLE_SETUP_CLASSPATH
-classpath "$CLASSPATH"; unset CLASSPATH
+classpath "$CLASSPATH"; export CLASSPATH=""
isabelle_scala scalac -Dfile.encoding=UTF-8 \
-classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@"
--- a/lib/scripts/getsettings Thu Oct 20 14:43:29 2022 +0200
+++ b/lib/scripts/getsettings Sat Oct 22 18:47:48 2022 +0200
@@ -41,7 +41,7 @@
ISABELLE_ROOT="$(platform_path "$ISABELLE_HOME")"
ISABELLE_CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"
- unset CLASSPATH
+ export CLASSPATH=""
else
if [ -z "$USER_HOME" ]; then
USER_HOME="$HOME"
@@ -50,7 +50,7 @@
ISABELLE_ROOT="$ISABELLE_HOME"
ISABELLE_CLASSPATH="$CLASSPATH"
- unset CLASSPATH
+ export CLASSPATH=""
fi
#init cumulative settings
--- a/src/Pure/Admin/build_history.scala Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/Admin/build_history.scala Sat Oct 22 18:47:48 2022 +0200
@@ -359,7 +359,7 @@
session_build_info :::
ml_statistics.map(Protocol.ML_Statistics_Marker.apply) :::
session_errors.map(Protocol.Error_Message_Marker.apply) :::
- heap_sizes), XZ.options(6))
+ heap_sizes), Compress.Options_XZ(6))
/* next build */
--- a/src/Pure/Admin/build_log.scala Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/Admin/build_log.scala Sat Oct 22 18:47:48 2022 +0200
@@ -616,7 +616,10 @@
errors = log_file.filter(Protocol.Error_Message_Marker))
}
- def compress_errors(errors: List[String], cache: XZ.Cache = XZ.Cache()): Option[Bytes] =
+ def compress_errors(
+ errors: List[String],
+ cache: Compress.Cache = Compress.Cache.none
+ ): Option[Bytes] =
if (errors.isEmpty) None
else {
Some(Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.string)(errors))).
@@ -627,7 +630,7 @@
if (bytes.is_empty) Nil
else {
XML.Decode.list(YXML.string_of_body)(
- YXML.parse_body(bytes.uncompress(cache = cache.xz).text, cache = cache))
+ YXML.parse_body(bytes.uncompress(cache = cache.compress).text, cache = cache))
}
@@ -954,7 +957,7 @@
stmt.double(13) = session.ml_timing.factor
stmt.long(14) = session.heap_size
stmt.string(15) = session.status.map(_.toString)
- stmt.bytes(16) = compress_errors(session.errors, cache = cache.xz)
+ stmt.bytes(16) = compress_errors(session.errors, cache = cache.compress)
stmt.string(17) = session.sources
stmt.execute()
}
@@ -988,7 +991,7 @@
db.using_statement(db.insert_permissive(table)) { stmt =>
val ml_stats: List[(String, Option[Bytes])] =
Par_List.map[(String, Session_Entry), (String, Option[Bytes])](
- { case (a, b) => (a, Properties.compress(b.ml_statistics, cache = cache.xz).proper) },
+ { case (a, b) => (a, Properties.compress(b.ml_statistics, cache = cache.compress).proper) },
build_info.sessions.iterator.filter(p => p._2.ml_statistics.nonEmpty).toList)
val entries = if (ml_stats.nonEmpty) ml_stats else List("" -> None)
for ((session_name, ml_statistics) <- entries) {
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/build_zstd.scala Sat Oct 22 18:47:48 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/Admin/jenkins.scala Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/Admin/jenkins.scala Sat Oct 22 18:47:48 2022 +0200
@@ -112,7 +112,7 @@
File.write_xz(log_path,
terminate_lines(Url.read(main_log) ::
ml_statistics.map(Protocol.ML_Statistics_Marker.apply)),
- XZ.options(6))
+ Compress.Options_XZ(6))
}
}
}
--- a/src/Pure/General/bytes.scala Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/General/bytes.scala Sat Oct 22 18:47:48 2022 +0200
@@ -7,11 +7,10 @@
package isabelle
-import java.io.{File => JFile, ByteArrayOutputStream, ByteArrayInputStream,
- OutputStream, InputStream, FileInputStream, FileOutputStream}
+import java.io.{ByteArrayInputStream, ByteArrayOutputStream, FileInputStream, FileOutputStream, InputStream, OutputStream, File as JFile}
import java.net.URL
-
-import org.tukaani.xz.{XZInputStream, XZOutputStream}
+import org.tukaani.xz
+import com.github.luben.zstd
object Bytes {
@@ -191,20 +190,61 @@
def write_stream(stream: OutputStream): Unit = stream.write(bytes, offset, length)
- /* XZ data compression */
+ /* XZ / Zstd data compression */
- def uncompress(cache: XZ.Cache = XZ.Cache()): Bytes =
- using(new XZInputStream(stream(), cache))(Bytes.read_stream(_, hint = length))
+ def detect_xz: Boolean =
+ length >= 6 &&
+ bytes(offset) == 0xFD.toByte &&
+ bytes(offset + 1) == 0x37.toByte &&
+ bytes(offset + 2) == 0x7A.toByte &&
+ bytes(offset + 3) == 0x58.toByte &&
+ bytes(offset + 4) == 0x5A.toByte &&
+ bytes(offset + 5) == 0x00.toByte
+
+ def detect_zstd: Boolean =
+ length >= 4 &&
+ bytes(offset) == 0x28.toByte &&
+ bytes(offset + 1) == 0xB5.toByte &&
+ bytes(offset + 2) == 0x2F.toByte &&
+ bytes(offset + 3) == 0xFD.toByte
+
+ def uncompress_xz(cache: Compress.Cache = Compress.Cache.none): Bytes =
+ using(new xz.XZInputStream(stream(), cache.for_xz))(Bytes.read_stream(_, hint = length))
- def compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.Cache()): Bytes = {
- val result = new ByteArrayOutputStream(length)
- using(new XZOutputStream(result, options, cache))(write_stream(_))
- new Bytes(result.toByteArray, 0, result.size)
+ def uncompress_zstd(cache: Compress.Cache = Compress.Cache.none): Bytes = {
+ Zstd.init()
+ val n = zstd.Zstd.decompressedSize(bytes, offset, length)
+ if (n > 0 && n < Integer.MAX_VALUE) {
+ Bytes(zstd.Zstd.decompress(array, n.toInt))
+ }
+ else {
+ using(new zstd.ZstdInputStream(stream(), cache.for_zstd))(Bytes.read_stream(_, hint = length))
+ }
+ }
+
+ def uncompress(cache: Compress.Cache = Compress.Cache.none): Bytes =
+ if (detect_xz) uncompress_xz(cache = cache)
+ else if (detect_zstd) uncompress_zstd(cache = cache)
+ else error("Cannot detect compression scheme")
+
+ def compress(
+ options: Compress.Options = Compress.Options(),
+ cache: Compress.Cache = Compress.Cache.none
+ ): Bytes = {
+ options match {
+ case options_xz: Compress.Options_XZ =>
+ val result = new ByteArrayOutputStream(length)
+ using(new xz.XZOutputStream(result, options_xz.make, cache.for_xz))(write_stream)
+ new Bytes(result.toByteArray, 0, result.size)
+ case options_zstd: Compress.Options_Zstd =>
+ Zstd.init()
+ Bytes(zstd.Zstd.compress(array, options_zstd.level))
+ }
}
def maybe_compress(
- options: XZ.Options = XZ.options(),
- cache: XZ.Cache = XZ.Cache()
+ options: Compress.Options = Compress.Options(),
+ cache: Compress.Cache = Compress.Cache.none
) : (Boolean, Bytes) = {
val compressed = compress(options = options, cache = cache)
if (compressed.length < length) (true, compressed) else (false, this)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/compress.scala Sat Oct 22 18:47:48 2022 +0200
@@ -0,0 +1,69 @@
+/* Title: Pure/General/compress.scala
+ Author: Makarius
+
+Support for generic data compression.
+*/
+
+package isabelle
+
+
+import org.tukaani.xz
+import com.github.luben.zstd
+
+
+object Compress {
+ /* options */
+
+ object Options {
+ def apply(): Options = Options_XZ()
+ }
+ sealed abstract class Options
+ case class Options_XZ(level: Int = 3) extends Options {
+ def make: xz.LZMA2Options = {
+ val opts = new xz.LZMA2Options
+ opts.setPreset(level)
+ opts
+ }
+ }
+ case class Options_Zstd(level: Int = 3) extends Options
+
+
+ /* cache */
+
+ class Cache private(val for_xz: xz.ArrayCache, val for_zstd: zstd.BufferPool)
+
+ object Cache {
+ def none: Cache = {
+ Zstd.init()
+ new Cache(xz.ArrayCache.getDummyCache(), zstd.NoPool.INSTANCE)
+ }
+ def make(): Cache = {
+ Zstd.init()
+ val pool = Untyped.constructor(classOf[zstd.RecyclingBufferPool]).newInstance()
+ new Cache(new xz.BasicArrayCache, pool)
+ }
+ }
+
+
+ /* Scala functions in ML */
+
+ object XZ_Compress extends Scala.Fun_Bytes("XZ.compress") {
+ val here = Scala_Project.here
+ def apply(arg: Bytes): Bytes = arg.compress(Options_XZ())
+ }
+
+ object XZ_Uncompress extends Scala.Fun_Bytes("XZ.uncompress") {
+ val here = Scala_Project.here
+ def apply(arg: Bytes): Bytes = arg.uncompress_xz()
+ }
+
+ object Zstd_Compress extends Scala.Fun_Bytes("Zstd.compress") {
+ val here = Scala_Project.here
+ def apply(arg: Bytes): Bytes = arg.compress(Options_Zstd())
+ }
+
+ object Zstd_Uncompress extends Scala.Fun_Bytes("Zstd.uncompress") {
+ val here = Scala_Project.here
+ def apply(arg: Bytes): Bytes = arg.uncompress_zstd()
+ }
+}
--- a/src/Pure/General/file.scala Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/General/file.scala Sat Oct 22 18:47:48 2022 +0200
@@ -17,7 +17,8 @@
import java.util.zip.{GZIPInputStream, GZIPOutputStream}
import java.util.EnumSet
-import org.tukaani.xz.{XZInputStream, XZOutputStream}
+import org.tukaani.xz
+import com.github.luben.zstd
import scala.collection.mutable
@@ -85,6 +86,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")
@@ -194,9 +196,15 @@
def read_gzip(path: Path): String = read_gzip(path.file)
def read_xz(file: JFile): String =
- read_stream(new XZInputStream(new BufferedInputStream(new FileInputStream(file))))
+ read_stream(new xz.XZInputStream(new BufferedInputStream(new FileInputStream(file))))
def read_xz(path: Path): String = read_xz(path.file)
+ def read_zstd(file: JFile): String = {
+ Zstd.init()
+ read_stream(new zstd.ZstdInputStream(new BufferedInputStream(new FileInputStream(file))))
+ }
+ def read_zstd(path: Path): String = read_zstd(path.file)
+
/* read lines */
@@ -240,12 +248,25 @@
write_file(file, text, (s: OutputStream) => new GZIPOutputStream(new BufferedOutputStream(s)))
def write_gzip(path: Path, text: String): Unit = write_gzip(path.file, text)
- def write_xz(file: JFile, text: String, options: XZ.Options): Unit =
- File.write_file(file, text, s => new XZOutputStream(new BufferedOutputStream(s), options))
- def write_xz(file: JFile, text: String): Unit = write_xz(file, text, XZ.options())
- def write_xz(path: Path, text: String, options: XZ.Options): Unit =
+ def write_xz(file: JFile, text: String, options: Compress.Options_XZ): Unit =
+ File.write_file(file, text,
+ s => new xz.XZOutputStream(new BufferedOutputStream(s), options.make))
+ def write_xz(file: JFile, text: String): Unit = write_xz(file, text, Compress.Options_XZ())
+ def write_xz(path: Path, text: String, options: Compress.Options_XZ): Unit =
write_xz(path.file, text, options)
- def write_xz(path: Path, text: String): Unit = write_xz(path, text, XZ.options())
+ def write_xz(path: Path, text: String): Unit = write_xz(path, text, Compress.Options_XZ())
+
+ def write_zstd(file: JFile, text: String, options: Compress.Options_Zstd): Unit = {
+ Zstd.init()
+ File.write_file(file, text,
+ s => new zstd.ZstdOutputStream(new BufferedOutputStream(s), options.level))
+ }
+ def write_zstd(file: JFile, text: String): Unit =
+ write_zstd(file, text, Compress.Options_Zstd())
+ def write_zstd(path: Path, text: String, options: Compress.Options_Zstd): Unit =
+ write_zstd(path.file, text, options)
+ def write_zstd(path: Path, text: String): Unit =
+ write_zstd(path, text, Compress.Options_Zstd())
def write_backup(path: Path, text: String): Unit = {
if (path.is_file) Isabelle_System.move_file(path, path.backup)
--- a/src/Pure/General/http.scala Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/General/http.scala Sat Oct 22 18:47:48 2022 +0200
@@ -22,7 +22,7 @@
val mime_type_html: String = "text/html; charset=utf-8"
val default_mime_type: String = mime_type_bytes
- val default_encoding: String = UTF8.charset_name
+ val default_encoding: String = UTF8.charset.name
def apply(
bytes: Bytes,
--- a/src/Pure/General/path.scala Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/General/path.scala Sat Oct 22 18:47:48 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
--- a/src/Pure/General/properties.scala Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/General/properties.scala Sat Oct 22 18:47:48 2022 +0200
@@ -54,8 +54,8 @@
}
def compress(ps: List[T],
- options: XZ.Options = XZ.options(),
- cache: XZ.Cache = XZ.Cache()
+ options: Compress.Options = Compress.Options(),
+ cache: Compress.Cache = Compress.Cache.none
): Bytes = {
if (ps.isEmpty) Bytes.empty
else {
@@ -69,7 +69,7 @@
else {
val ps =
XML.Decode.list(XML.Decode.properties)(
- YXML.parse_body(bs.uncompress(cache = cache.xz).text))
+ YXML.parse_body(bs.uncompress(cache = cache.compress).text))
if (cache.no_cache) ps else ps.map(cache.props)
}
}
--- a/src/Pure/General/url.scala Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/General/url.scala Sat Oct 22 18:47:48 2022 +0200
@@ -64,8 +64,8 @@
/* strings */
- def decode(s: String): String = URLDecoder.decode(s, UTF8.charset_name)
- def encode(s: String): String = URLEncoder.encode(s, UTF8.charset_name)
+ def decode(s: String): String = URLDecoder.decode(s, UTF8.charset)
+ def encode(s: String): String = URLEncoder.encode(s, UTF8.charset)
/* read */
--- a/src/Pure/General/utf8.scala Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/General/utf8.scala Sat Oct 22 18:47:48 2022 +0200
@@ -7,16 +7,13 @@
package isabelle
-import java.nio.charset.Charset
-import scala.io.Codec
+import java.nio.charset.{Charset, StandardCharsets}
object UTF8 {
/* charset */
- val charset_name: String = "UTF-8"
- val charset: Charset = Charset.forName(charset_name)
- def codec(): Codec = Codec(charset)
+ val charset: Charset = StandardCharsets.UTF_8
def bytes(s: String): Array[Byte] = s.getBytes(charset)
--- a/src/Pure/General/xz.scala Thu Oct 20 14:43:29 2022 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-/* Title: Pure/General/xz.scala
- Author: Makarius
-
-Support for XZ data compression.
-*/
-
-package isabelle
-
-
-import org.tukaani.xz.{LZMA2Options, ArrayCache, BasicArrayCache}
-
-
-object XZ {
- /* options */
-
- type Options = LZMA2Options
-
- def options(preset: Int = 3): Options = {
- val opts = new LZMA2Options
- opts.setPreset(preset)
- opts
- }
-
-
- /* cache */
-
- type Cache = ArrayCache
-
- object Cache {
- def none: ArrayCache = ArrayCache.getDummyCache()
- def apply(): ArrayCache = ArrayCache.getDefaultCache()
- def make(): ArrayCache = new BasicArrayCache
- }
-
-
- /* Scala functions in ML */
-
- object Compress extends Scala.Fun_Bytes("XZ.compress") {
- val here = Scala_Project.here
- def apply(arg: Bytes): Bytes = arg.compress()
- }
-
- object Uncompress extends Scala.Fun_Bytes("XZ.uncompress") {
- val here = Scala_Project.here
- def apply(arg: Bytes): Bytes = arg.uncompress()
- }
-}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/zstd.ML Sat Oct 22 18:47:48 2022 +0200
@@ -0,0 +1,19 @@
+(* Title: Pure/General/zstd.ML
+ Author: Makarius
+
+Support for Zstd compression (via Isabelle/Scala).
+*)
+
+signature Zstd =
+sig
+ val compress: Bytes.T -> Bytes.T
+ val uncompress: Bytes.T -> Bytes.T
+end;
+
+structure Zstd: Zstd =
+struct
+
+val compress = \<^scala>\<open>Zstd.compress\<close>;
+val uncompress = \<^scala>\<open>Zstd.uncompress\<close>;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/zstd.scala Sat Oct 22 18:47:48 2022 +0200
@@ -0,0 +1,32 @@
+/* Title: Pure/General/xz.scala
+ Author: Makarius
+
+Support for Zstd data compression.
+*/
+
+package isabelle
+
+
+import com.github.luben.zstd
+
+
+object Zstd {
+ def init(): Unit = init_jni
+
+ private lazy val init_jni: Unit = {
+ require(!zstd.util.Native.isLoaded(),
+ "Zstd library already initialized by other means than isabelle.Zstd.init()")
+
+ 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))
+
+ zstd.util.Native.assumeLoaded()
+ assert(zstd.util.Native.isLoaded())
+ Class.forName("com.github.luben.zstd.Zstd")
+ }
+}
--- a/src/Pure/PIDE/xml.scala Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/PIDE/xml.scala Sat Oct 22 18:47:48 2022 +0200
@@ -189,15 +189,15 @@
object Cache {
def make(
- xz: XZ.Cache = XZ.Cache.make(),
+ compress: Compress.Cache = Compress.Cache.make(),
max_string: Int = isabelle.Cache.default_max_string,
initial_size: Int = isabelle.Cache.default_initial_size): Cache =
- new Cache(xz, max_string, initial_size)
+ new Cache(compress, max_string, initial_size)
- val none: Cache = make(XZ.Cache.none, max_string = 0)
+ val none: Cache = make(Compress.Cache.none, max_string = 0)
}
- class Cache(val xz: XZ.Cache, max_string: Int, initial_size: Int)
+ class Cache(val compress: Compress.Cache, max_string: Int, initial_size: Int)
extends isabelle.Cache(max_string, initial_size) {
protected def cache_props(x: Properties.T): Properties.T = {
if (x.isEmpty) x
--- a/src/Pure/ROOT.ML Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/ROOT.ML Sat Oct 22 18:47:48 2022 +0200
@@ -348,6 +348,7 @@
ML_file "General/base64.ML";
ML_file "General/xz.ML";
+ML_file "General/zstd.ML";
ML_file "Tools/build.ML";
ML_file "Tools/named_thms.ML";
ML_file "Tools/print_operation.ML";
@@ -364,4 +365,3 @@
ML_file "Tools/jedit.ML";
ML_file "Tools/ghc.ML";
ML_file "Tools/generated_files.ML";
-
--- a/src/Pure/System/isabelle_charset.scala Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/System/isabelle_charset.scala Sat Oct 22 18:47:48 2022 +0200
@@ -22,7 +22,7 @@
class Isabelle_Charset extends Charset(Isabelle_Charset.name, null) {
override def contains(cs: Charset): Boolean =
- cs.name.equalsIgnoreCase(UTF8.charset_name) || UTF8.charset.contains(cs)
+ cs.name.equalsIgnoreCase(UTF8.charset.name) || UTF8.charset.contains(cs)
override def newDecoder(): CharsetDecoder = UTF8.charset.newDecoder
--- a/src/Pure/System/isabelle_tool.scala Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/System/isabelle_tool.scala Sat Oct 22 18:47:48 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,
--- a/src/Pure/System/scala.scala Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/System/scala.scala Sat Oct 22 18:47:48 2022 +0200
@@ -368,8 +368,10 @@
Scala_Build.Scala_Fun,
Base64.Decode,
Base64.Encode,
- XZ.Compress,
- XZ.Uncompress,
+ Compress.XZ_Compress,
+ Compress.XZ_Uncompress,
+ Compress.Zstd_Compress,
+ Compress.Zstd_Uncompress,
Doc.Doc_Names,
Bibtex.Check_Database,
Isabelle_System.Make_Directory,
--- a/src/Pure/Thy/export.scala Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/Thy/export.scala Sat Oct 22 18:47:48 2022 +0200
@@ -134,7 +134,7 @@
def uncompressed: Bytes = {
val (compressed, bytes) = body.join
- if (compressed) bytes.uncompress(cache = cache.xz) else bytes
+ if (compressed) bytes.uncompress(cache = cache.compress) else bytes
}
def uncompressed_yxml: XML.Body =
@@ -183,7 +183,7 @@
cache: XML.Cache
): Entry = {
val body =
- if (args.compress) Future.fork(bytes.maybe_compress(cache = cache.xz))
+ if (args.compress) Future.fork(bytes.maybe_compress(cache = cache.compress))
else Future.value((false, bytes))
val entry_name = Entry_Name(session = session_name, theory = args.theory_name, name = args.name)
Entry(entry_name, args.executable, body, cache)
--- a/src/Pure/Thy/sessions.scala Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/Thy/sessions.scala Sat Oct 22 18:47:48 2022 +0200
@@ -1149,6 +1149,7 @@
info_roots += make_info(chapter_defs, options, select, dir, chapter, entry)
case _ =>
}
+ chapter = UNSORTED
}
info_roots.toList
}
@@ -1487,11 +1488,11 @@
db.using_statement(table.insert()) { stmt =>
stmt.string(1) = name
stmt.bytes(2) = Properties.encode(build_log.session_timing)
- stmt.bytes(3) = Properties.compress(build_log.command_timings, cache = cache.xz)
- stmt.bytes(4) = Properties.compress(build_log.theory_timings, cache = cache.xz)
- stmt.bytes(5) = Properties.compress(build_log.ml_statistics, cache = cache.xz)
- stmt.bytes(6) = Properties.compress(build_log.task_statistics, cache = cache.xz)
- stmt.bytes(7) = Build_Log.compress_errors(build_log.errors, cache = cache.xz)
+ stmt.bytes(3) = Properties.compress(build_log.command_timings, cache = cache.compress)
+ stmt.bytes(4) = Properties.compress(build_log.theory_timings, cache = cache.compress)
+ stmt.bytes(5) = Properties.compress(build_log.ml_statistics, cache = cache.compress)
+ stmt.bytes(6) = Properties.compress(build_log.task_statistics, cache = cache.compress)
+ stmt.bytes(7) = Build_Log.compress_errors(build_log.errors, cache = cache.compress)
stmt.string(8) = build.sources
stmt.string(9) = cat_lines(build.input_heaps)
stmt.string(10) = build.output_heap getOrElse ""
--- a/src/Pure/term.scala Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/term.scala Sat Oct 22 18:47:48 2022 +0200
@@ -177,16 +177,16 @@
object Cache {
def make(
- xz: XZ.Cache = XZ.Cache.make(),
+ compress: Compress.Cache = Compress.Cache.make(),
max_string: Int = isabelle.Cache.default_max_string,
initial_size: Int = isabelle.Cache.default_initial_size): Cache =
- new Cache(xz, initial_size, max_string)
+ new Cache(compress, initial_size, max_string)
val none: Cache = make(max_string = 0)
}
- class Cache(xz: XZ.Cache, max_string: Int, initial_size: Int)
- extends XML.Cache(xz, max_string, initial_size) {
+ class Cache(compress: Compress.Cache, max_string: Int, initial_size: Int)
+ extends XML.Cache(compress, max_string, initial_size) {
protected def cache_indexname(x: Indexname): Indexname =
lookup(x) getOrElse store(Indexname(cache_string(x.name), x.index))
--- a/src/Tools/Setup/src/Environment.java Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Tools/Setup/src/Environment.java Sat Oct 22 18:47:48 2022 +0200
@@ -9,6 +9,7 @@
import java.io.File;
import java.io.IOException;
+import java.nio.charset.StandardCharsets;
import java.nio.file.Files;
import java.nio.file.Path;
import java.util.HashMap;
@@ -179,6 +180,11 @@
/* raw process */
+ private static read_file(path: Path): String =
+ {
+ return new String(Files.readAllBytes(path), StandardCharsets.UTF_8);
+ }
+
public static ProcessBuilder process_builder(
List<String> cmd, File cwd, Map<String,String> env, boolean redirect)
{
@@ -242,8 +248,8 @@
}
int rc = proc.exitValue();
- String out = Files.readString(out_file);
- String err = Files.readString(err_file);
+ String out = read_file(out_file);
+ String err = read_file(err_file);
res = new Exec_Result(rc, out, err);
}
finally {
@@ -388,7 +394,7 @@
Exec_Result res = exec_process(cmd, null, env, true);
if (!res.ok()) throw new RuntimeException(res.out());
- for (String s : Files.readString(settings_file).split("\u0000", -1)) {
+ for (String s : read_file(settings_file).split("\u0000", -1)) {
int i = s.indexOf('=');
if (i > 0) { settings.put(s.substring(0, i), s.substring(i + 1)); }
else if (i < 0 && !s.isEmpty()) { settings.put(s, ""); }
--- a/src/Tools/jEdit/src/isabelle_encoding.scala Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Tools/jEdit/src/isabelle_encoding.scala Sat Oct 22 18:47:48 2022 +0200
@@ -40,10 +40,10 @@
}
override def getTextReader(in: InputStream): Reader =
- text_reader(in, UTF8.codec(), true)
+ text_reader(in, Codec(UTF8.charset), true)
override def getPermissiveTextReader(in: InputStream): Reader = {
- val codec = UTF8.codec()
+ val codec = Codec(UTF8.charset)
codec.onMalformedInput(CodingErrorAction.REPLACE)
codec.onUnmappableCharacter(CodingErrorAction.REPLACE)
text_reader(in, codec, false)
@@ -52,7 +52,7 @@
override def getTextWriter(out: OutputStream): Writer = {
val buffer = new ByteArrayOutputStream(BUFSIZE) {
override def flush(): Unit = {
- val text = Symbol.encode(toString(UTF8.charset_name))
+ val text = Symbol.encode(toString(UTF8.charset))
out.write(UTF8.bytes(text))
out.flush()
}
--- a/src/Tools/jEdit/src/jedit_main.scala Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_main.scala Sat Oct 22 18:47:48 2022 +0200
@@ -128,7 +128,7 @@
catch {
case exn: Throwable =>
GUI.init_laf()
- GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
+ GUI.dialog(null, "Isabelle main", GUI.scrollable_text(Exn.print(exn)))
sys.exit(Process_Result.RC.failure)
}
}
--- a/src/Tools/jEdit/src/session_build.scala Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Tools/jEdit/src/session_build.scala Sat Oct 22 18:47:48 2022 +0200
@@ -29,7 +29,7 @@
}
catch {
case exn: Throwable =>
- GUI.dialog(view, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
+ GUI.dialog(view, "Isabelle build", GUI.scrollable_text(Exn.print(exn)))
}
}
}