--- a/src/Pure/Admin/build_history.scala Tue Oct 18 10:11:22 2016 +0200
+++ b/src/Pure/Admin/build_history.scala Tue Oct 18 11:24:14 2016 +0200
@@ -146,8 +146,9 @@
/* main */
+ val build_host = Isabelle_System.hostname()
val build_history_date = Date.now()
- val build_host = Isabelle_System.hostname()
+ val build_group_id = build_host + ":" + build_history_date.time.ms
var first_build = true
for (threads <- threads_list) yield
@@ -183,23 +184,27 @@
Isabelle_System.copy_dir(isabelle_base_log, isabelle_output_log)
val build_start = Date.now()
- val res =
+ val build_result =
other_isabelle("build -v " + File.bash_args(build_args), redirect = true, echo = verbose)
val build_end = Date.now()
-
- /* output log */
-
val log_path =
other_isabelle.isabelle_home_user +
Build_Log.log_subdir(build_history_date) +
Build_Log.log_filename(
BUILD_HISTORY, build_history_date, build_host, ml_platform, "M" + threads)
- val build_info = Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info()
+ val build_info =
+ Build_Log.Log_File(log_path.base.implode, build_result.out_lines).parse_build_info()
+
+
+ /* output log */
val meta_info =
- List(Build_Log.Field.build_engine -> BUILD_HISTORY,
+ List(
+ Build_Log.Field.build_group_id -> build_group_id,
+ Build_Log.Field.build_id -> (build_host + ":" + build_start.time.ms),
+ Build_Log.Field.build_engine -> BUILD_HISTORY,
Build_Log.Field.build_host -> build_host,
Build_Log.Field.build_start -> Build_Log.print_date(build_start),
Build_Log.Field.build_end -> Build_Log.print_date(build_end),
@@ -228,7 +233,7 @@
Isabelle_System.mkdirs(log_path.dir)
File.write_xz(log_path.ext("xz"),
terminate_lines(
- Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: res.out_lines :::
+ Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: build_result.out_lines :::
ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _)) :::
heap_sizes), XZ.options(6))
@@ -242,7 +247,7 @@
first_build = false
- (res, log_path.ext("xz"))
+ (build_result, log_path.ext("xz"))
}
}
--- a/src/Pure/Admin/build_log.scala Tue Oct 18 10:11:22 2016 +0200
+++ b/src/Pure/Admin/build_log.scala Tue Oct 18 11:24:14 2016 +0200
@@ -247,6 +247,8 @@
object Field
{
+ val build_group_id = "build_group_id"
+ val build_id = "build_id"
val build_engine = "build_engine"
val build_host = "build_host"
val build_start = "build_start"
@@ -303,6 +305,11 @@
def parse(engine: String, host: String, start: Date,
End: Regex, Isabelle_Version: Regex, AFP_Version: Regex): Meta_Info =
{
+ val build_id =
+ {
+ val prefix = if (host != "") host else if (engine != "") engine else ""
+ (if (prefix == "") "build" else prefix) + ":" + start.time.ms
+ }
val build_engine = if (engine == "") Nil else List(Field.build_engine -> engine)
val build_host = if (host == "") Nil else List(Field.build_host -> host)
@@ -319,7 +326,7 @@
val afp_version =
log_file.find_match(AFP_Version).map(Field.afp_version -> _)
- Meta_Info(build_engine ::: build_host :::
+ Meta_Info((Field.build_id -> build_id) :: build_engine ::: build_host :::
start_date ::: end_date ::: isabelle_version.toList ::: afp_version.toList,
log_file.get_settings(Settings.all_settings))
}