261 |
261 |
262 val log_path = |
262 val log_path = |
263 other_isabelle.log_dir + Path.explode(build_history_date.rep.getYear.toString) + |
263 other_isabelle.log_dir + Path.explode(build_history_date.rep.getYear.toString) + |
264 Path.explode(log_name(build_history_date, ml_platform, "M" + threads)) |
264 Path.explode(log_name(build_history_date, ml_platform, "M" + threads)) |
265 |
265 |
|
266 val build_info = Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info() |
|
267 |
266 val meta_info = |
268 val meta_info = |
267 List(Build_Log.Field.build_engine -> BUILD_HISTORY, |
269 List(Build_Log.Field.build_engine -> BUILD_HISTORY, |
268 Build_Log.Field.build_host -> build_host, |
270 Build_Log.Field.build_host -> build_host, |
269 Build_Log.Field.build_start -> Build_Log.Log_File.Date_Format(build_start), |
271 Build_Log.Field.build_start -> Build_Log.Log_File.Date_Format(build_start), |
270 Build_Log.Field.build_end -> Build_Log.Log_File.Date_Format(build_end), |
272 Build_Log.Field.build_end -> Build_Log.Log_File.Date_Format(build_end), |
271 Build_Log.Field.isabelle_version -> isabelle_version) |
273 Build_Log.Field.isabelle_version -> isabelle_version) |
272 |
274 |
273 val ml_statistics = |
275 val ml_statistics = |
274 Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info(). |
276 build_info.finished_sessions.flatMap(session_name => |
275 finished_sessions.flatMap(session_name => |
277 { |
276 { |
278 val session_log = isabelle_output_log + Path.explode(session_name).ext("gz") |
277 val session_log = isabelle_output_log + Path.explode(session_name).ext("gz") |
279 if (session_log.is_file) { |
278 if (session_log.is_file) { |
280 Build_Log.Log_File(session_log).parse_session_info(ml_statistics = true). |
279 Build_Log.Log_File(session_log).parse_session_info(ml_statistics = true). |
281 ml_statistics.map(props => (Build_Log.SESSION_NAME -> session_name) :: props) |
280 ml_statistics.map(props => (Build_Log.SESSION_NAME -> session_name) :: props) |
282 } |
281 } |
283 else Nil |
282 else Nil |
284 }) |
283 }) |
285 |
|
286 val heap_sizes = |
|
287 build_info.finished_sessions.flatMap(session_name => |
|
288 { |
|
289 val heap = isabelle_output + Path.explode(session_name) |
|
290 if (heap.is_file) |
|
291 Some("Heap " + session_name + " (" + Value.Long(heap.file.length) + " bytes)") |
|
292 else None |
|
293 }) |
284 |
294 |
285 Isabelle_System.mkdirs(log_path.dir) |
295 Isabelle_System.mkdirs(log_path.dir) |
286 File.write_gzip(log_path, |
296 File.write_gzip(log_path, |
287 cat_lines( |
297 Library.terminate_lines( |
288 Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: res.out_lines ::: |
298 Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: res.out_lines ::: |
289 ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _)))) |
299 ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _)) ::: |
|
300 heap_sizes)) |
290 |
301 |
291 Output.writeln(log_path.implode, stdout = true) |
302 Output.writeln(log_path.implode, stdout = true) |
292 |
303 |
293 |
304 |
294 /* next build */ |
305 /* next build */ |