--- 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)
}