--- a/src/HOL/Import/patches/patch2 Sat Jan 18 22:41:33 2025 +0100
+++ b/src/HOL/Import/patches/patch2 Sat Jan 18 23:19:23 2025 +0100
@@ -5,7 +5,7 @@
needs "lib.ml";;
+#load "unix.cma";;
-+let poutc = Unix.open_process_out "buffer | gzip -c > proofs.gz";;
++let poutc = open_out "proofs";;
+let foutc = open_out "facts.lst";;
+let stop_recording () = close_out poutc; close_out foutc;;
+
--- a/src/Pure/Admin/component_hol_light.scala Sat Jan 18 22:41:33 2025 +0100
+++ b/src/Pure/Admin/component_hol_light.scala Sat Jan 18 23:19:23 2025 +0100
@@ -27,8 +27,8 @@
if (!only_offline) {
Linux.check_system()
- Isabelle_System.require_command("buffer", test = "-i /dev/null")
Isabelle_System.require_command("patch")
+ Isabelle_System.require_command("zstd")
}
@@ -76,7 +76,6 @@
export MAXTMS=10000
./ocaml-hol -I +compiler-libs stage2.ml
- gzip -d proofs.gz
> maps.lst
"$HOL_LIGHT_IMPORT/x86_64-linux/offline"
@@ -157,12 +156,12 @@
"export MAXTMS=10000",
"./ocaml-hol -I +compiler-libs stage2.ml")
run(3,
- "gzip -d proofs.gz",
"> maps.lst",
- File.bash_path(platform_dir + offline_exe) + " proofs")
+ File.bash_path(platform_dir + offline_exe) + " proofs",
+ "zstd -8 proofs")
val bundle_dir = Isabelle_System.make_directory(component_dir.path + Path.explode("bundle"))
- Isabelle_System.copy_file(hol_light_dir + Path.explode("proofs"), bundle_dir)
+ Isabelle_System.copy_file(hol_light_dir + Path.explode("proofs.zst"), bundle_dir)
}
}
}