# HG changeset patch # User Fabian Huch # 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) }