# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1720079860 -7200
# Node ID 748f9bee82788aef0d9d21d95b8ab8560cd6b127
# Parent  bd00bdf39c86f1e92714b6827cb5b65871b2d18b
compress reports;

diff -r bd00bdf39c86 -r 748f9bee8278 src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Wed Jul 03 21:11:24 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Thu Jul 04 09:57:40 2024 +0200
@@ -601,14 +601,19 @@
     private val log_name = "build-manager"
 
     private def log_file = dir + Path.basic(log_name).log
+    private def log_file_gz = dir + Path.basic(log_name).log.gz
 
     def init(): Unit = Isabelle_System.make_directory(dir)
 
-    def ok: Boolean = log_file.is_file
+    def ok: Boolean = log_file.is_file != log_file_gz.is_file
 
     def progress: Progress = new File_Progress(log_file)
 
-    def read: Report.Data = Report.Data(if_proper(ok, File.read(log_file)))
+    def read: Report.Data = {
+      val log =
+        if_proper(ok, if (log_file.is_file) File.read(log_file) else File.read_gzip(log_file_gz))
+      Report.Data(log)
+    }
 
     def result(uuid: Option[UUID.T]): Result = {
       val End = """^Job ended at [^,]+, with status (\w+)$""".r
@@ -627,6 +632,11 @@
       val isabelle_version = meta_info.get(Build_Log.Prop.isabelle_version)
       val afp_version = meta_info.get(Build_Log.Prop.afp_version)
 
+      if (log_file.is_file) {
+        File.write_gzip(log_file_gz, build_log_file.text)
+        Isabelle_System.rm_tree(log_file)
+      }
+
       Result(kind, id, status, uuid, build_host, start_date, end_date, isabelle_version,
         afp_version)
     }