# HG changeset patch # User wenzelm # Date 1495390345 -7200 # Node ID 29c9e3742069f4cdd96b3b43d15bf916ca03c390 # Parent 29a31cf0b4bc0cd91a8bbda8eac0e9e0358fa466 incremental build progress, to see state after unexpected failure (see also b3d6fb291f58); diff -r 29a31cf0b4bc -r 29c9e3742069 src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala Sun May 21 20:11:12 2017 +0200 +++ b/src/Pure/Admin/build_history.scala Sun May 21 20:12:25 2017 +0200 @@ -169,6 +169,7 @@ val isabelle_output = Path.explode(other_isabelle("getenv -b ISABELLE_OUTPUT").check.out) val isabelle_output_log = isabelle_output + Path.explode("log") val isabelle_base_log = isabelle_output + Path.explode("../base_log") + val build_out = isabelle_output_log + Path.explode("build.out") if (first_build) { other_isabelle.resolve_components(verbose) @@ -194,7 +195,11 @@ val build_start = Date.now() val build_args1 = List("-v", "-j" + processes) ::: build_args val build_result = - other_isabelle("build " + Bash.strings(build_args1), redirect = true, echo = verbose) + { + val progress1 = new Seq_Progress(progress, new File_Progress(build_out)) + val other_isabelle1 = new Other_Isabelle(progress1, hg.root, isabelle_identifier) + other_isabelle1("build " + Bash.strings(build_args1), redirect = true, echo = verbose) + } val build_end = Date.now() val log_path = @@ -203,9 +208,6 @@ Build_Log.log_filename(Build_History.engine, build_history_date, List(build_host, ml_platform, "M" + threads) ::: build_tags) - Isabelle_System.mkdirs(isabelle_output_log) - File.write(isabelle_output_log + Path.explode("build.log"), build_result.out) - val build_info: Build_Log.Build_Info = Build_Log.Log_File(log_path.base.implode, build_result.out_lines). parse_build_info(ml_statistics = true) @@ -264,6 +266,8 @@ /* next build */ + build_out.file.delete + if (multicore_base && first_build && isabelle_output_log.is_dir) Isabelle_System.copy_dir(isabelle_output_log, isabelle_base_log)