compress reports;
authorFabian Huch <huch@in.tum.de>
Thu, 04 Jul 2024 09:57:40 +0200
changeset 80498 748f9bee8278
parent 80497 bd00bdf39c86
child 80499 433475f17d73
compress reports;
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)
     }