# HG changeset patch
# User wenzelm
# Date 1737238763 -3600
# Node ID 8d5989ab1e422bcd11f05a2eb0e7e0ae3028ea19
# Parent  f4cd3e67909655bbde28d6b19807d7d656ae75e8
clarified compression;

diff -r f4cd3e679096 -r 8d5989ab1e42 src/HOL/Import/patches/patch2
--- 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;;
 +
diff -r f4cd3e679096 -r 8d5989ab1e42 src/Pure/Admin/component_hol_light.scala
--- 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)
       }
     }
   }