257 val sql = |
257 val sql = |
258 profile.select(options, ml_statistics = ml_statistics, only_sessions = only_sessions) |
258 profile.select(options, ml_statistics = ml_statistics, only_sessions = only_sessions) |
259 progress.echo(sql, verbose = true) |
259 progress.echo(sql, verbose = true) |
260 |
260 |
261 db.using_statement(sql) { stmt => |
261 db.using_statement(sql) { stmt => |
262 val res = stmt.execute_query() |
262 using(stmt.execute_query()) { res => |
263 while (res.next()) { |
263 while (res.next()) { |
264 val session_name = res.string(Build_Log.Data.session_name) |
264 val session_name = res.string(Build_Log.Data.session_name) |
265 val chapter = res.string(Build_Log.Data.chapter) |
265 val chapter = res.string(Build_Log.Data.chapter) |
266 val groups = split_lines(res.string(Build_Log.Data.groups)) |
266 val groups = split_lines(res.string(Build_Log.Data.groups)) |
267 val threads = { |
267 val threads = { |
268 val threads1 = |
268 val threads1 = |
269 res.string(Build_Log.Settings.ISABELLE_BUILD_OPTIONS) match { |
269 res.string(Build_Log.Settings.ISABELLE_BUILD_OPTIONS) match { |
270 case Threads_Option(Value.Int(i)) => i |
270 case Threads_Option(Value.Int(i)) => i |
271 case _ => 1 |
271 case _ => 1 |
|
272 } |
|
273 val threads2 = res.get_int(Build_Log.Data.threads).getOrElse(1) |
|
274 threads1 max threads2 |
|
275 } |
|
276 val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM) |
|
277 val ml_platform_64 = |
|
278 ml_platform.startsWith("x86_64-") || ml_platform.startsWith("arm64-") |
|
279 val data_name = |
|
280 profile.description + |
|
281 (if (ml_platform_64) ", 64bit" else "") + |
|
282 (if (threads == 1) "" else ", " + threads + " threads") |
|
283 |
|
284 res.get_string(Build_Log.Prop.build_host).foreach(host => |
|
285 data_hosts += (data_name -> (get_hosts(data_name) + host))) |
|
286 |
|
287 data_stretch += (data_name -> profile.stretch(options)) |
|
288 |
|
289 val isabelle_version = res.string(Build_Log.Prop.isabelle_version) |
|
290 val afp_version = res.string(Build_Log.Prop.afp_version) |
|
291 |
|
292 val ml_stats = |
|
293 ML_Statistics( |
|
294 if (ml_statistics) { |
|
295 Properties.uncompress(res.bytes(Build_Log.Data.ml_statistics), cache = store.cache) |
|
296 } |
|
297 else Nil, |
|
298 domain = ml_statistics_domain, |
|
299 heading = session_name + print_version(isabelle_version, afp_version, chapter)) |
|
300 |
|
301 val entry = |
|
302 Entry( |
|
303 chapter = chapter, |
|
304 pull_date = res.date(Build_Log.Data.pull_date(afp = false)), |
|
305 afp_pull_date = |
|
306 if (afp) res.get_date(Build_Log.Data.pull_date(afp = true)) else None, |
|
307 isabelle_version = isabelle_version, |
|
308 afp_version = afp_version, |
|
309 timing = |
|
310 res.timing( |
|
311 Build_Log.Data.timing_elapsed, |
|
312 Build_Log.Data.timing_cpu, |
|
313 Build_Log.Data.timing_gc), |
|
314 ml_timing = |
|
315 res.timing( |
|
316 Build_Log.Data.ml_timing_elapsed, |
|
317 Build_Log.Data.ml_timing_cpu, |
|
318 Build_Log.Data.ml_timing_gc), |
|
319 maximum_code = Space.B(ml_stats.maximum(ML_Statistics.CODE_SIZE)), |
|
320 average_code = Space.B(ml_stats.average(ML_Statistics.CODE_SIZE)), |
|
321 maximum_stack = Space.B(ml_stats.maximum(ML_Statistics.STACK_SIZE)), |
|
322 average_stack = Space.B(ml_stats.average(ML_Statistics.STACK_SIZE)), |
|
323 maximum_heap = Space.B(ml_stats.maximum(ML_Statistics.HEAP_SIZE)), |
|
324 average_heap = Space.B(ml_stats.average(ML_Statistics.HEAP_SIZE)), |
|
325 stored_heap = Space.bytes(res.long(Build_Log.Data.heap_size)), |
|
326 status = Build_Log.Session_Status.withName(res.string(Build_Log.Data.status)), |
|
327 errors = |
|
328 Build_Log.uncompress_errors( |
|
329 res.bytes(Build_Log.Data.errors), cache = store.cache)) |
|
330 |
|
331 val sessions = data_entries.getOrElse(data_name, Map.empty) |
|
332 val session = |
|
333 sessions.get(session_name) match { |
|
334 case None => |
|
335 Session(session_name, threads, List(entry), ml_stats, entry.date) |
|
336 case Some(old) => |
|
337 val (ml_stats1, ml_stats1_date) = |
|
338 if (entry.date > old.ml_statistics_date) (ml_stats, entry.date) |
|
339 else (old.ml_statistics, old.ml_statistics_date) |
|
340 Session(session_name, threads, entry :: old.entries, ml_stats1, ml_stats1_date) |
272 } |
341 } |
273 val threads2 = res.get_int(Build_Log.Data.threads).getOrElse(1) |
342 |
274 threads1 max threads2 |
343 if ((!afp || chapter == AFP.chapter) && |
275 } |
344 (!profile.bulky || groups.exists(AFP.groups_bulky.toSet))) { |
276 val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM) |
345 data_entries += (data_name -> (sessions + (session_name -> session))) |
277 val ml_platform_64 = |
|
278 ml_platform.startsWith("x86_64-") || ml_platform.startsWith("arm64-") |
|
279 val data_name = |
|
280 profile.description + |
|
281 (if (ml_platform_64) ", 64bit" else "") + |
|
282 (if (threads == 1) "" else ", " + threads + " threads") |
|
283 |
|
284 res.get_string(Build_Log.Prop.build_host).foreach(host => |
|
285 data_hosts += (data_name -> (get_hosts(data_name) + host))) |
|
286 |
|
287 data_stretch += (data_name -> profile.stretch(options)) |
|
288 |
|
289 val isabelle_version = res.string(Build_Log.Prop.isabelle_version) |
|
290 val afp_version = res.string(Build_Log.Prop.afp_version) |
|
291 |
|
292 val ml_stats = |
|
293 ML_Statistics( |
|
294 if (ml_statistics) { |
|
295 Properties.uncompress(res.bytes(Build_Log.Data.ml_statistics), cache = store.cache) |
|
296 } |
|
297 else Nil, |
|
298 domain = ml_statistics_domain, |
|
299 heading = session_name + print_version(isabelle_version, afp_version, chapter)) |
|
300 |
|
301 val entry = |
|
302 Entry( |
|
303 chapter = chapter, |
|
304 pull_date = res.date(Build_Log.Data.pull_date(afp = false)), |
|
305 afp_pull_date = |
|
306 if (afp) res.get_date(Build_Log.Data.pull_date(afp = true)) else None, |
|
307 isabelle_version = isabelle_version, |
|
308 afp_version = afp_version, |
|
309 timing = |
|
310 res.timing( |
|
311 Build_Log.Data.timing_elapsed, |
|
312 Build_Log.Data.timing_cpu, |
|
313 Build_Log.Data.timing_gc), |
|
314 ml_timing = |
|
315 res.timing( |
|
316 Build_Log.Data.ml_timing_elapsed, |
|
317 Build_Log.Data.ml_timing_cpu, |
|
318 Build_Log.Data.ml_timing_gc), |
|
319 maximum_code = Space.B(ml_stats.maximum(ML_Statistics.CODE_SIZE)), |
|
320 average_code = Space.B(ml_stats.average(ML_Statistics.CODE_SIZE)), |
|
321 maximum_stack = Space.B(ml_stats.maximum(ML_Statistics.STACK_SIZE)), |
|
322 average_stack = Space.B(ml_stats.average(ML_Statistics.STACK_SIZE)), |
|
323 maximum_heap = Space.B(ml_stats.maximum(ML_Statistics.HEAP_SIZE)), |
|
324 average_heap = Space.B(ml_stats.average(ML_Statistics.HEAP_SIZE)), |
|
325 stored_heap = Space.bytes(res.long(Build_Log.Data.heap_size)), |
|
326 status = Build_Log.Session_Status.withName(res.string(Build_Log.Data.status)), |
|
327 errors = |
|
328 Build_Log.uncompress_errors( |
|
329 res.bytes(Build_Log.Data.errors), cache = store.cache)) |
|
330 |
|
331 val sessions = data_entries.getOrElse(data_name, Map.empty) |
|
332 val session = |
|
333 sessions.get(session_name) match { |
|
334 case None => |
|
335 Session(session_name, threads, List(entry), ml_stats, entry.date) |
|
336 case Some(old) => |
|
337 val (ml_stats1, ml_stats1_date) = |
|
338 if (entry.date > old.ml_statistics_date) (ml_stats, entry.date) |
|
339 else (old.ml_statistics, old.ml_statistics_date) |
|
340 Session(session_name, threads, entry :: old.entries, ml_stats1, ml_stats1_date) |
|
341 } |
346 } |
342 |
|
343 if ((!afp || chapter == AFP.chapter) && |
|
344 (!profile.bulky || groups.exists(AFP.groups_bulky.toSet))) { |
|
345 data_entries += (data_name -> (sessions + (session_name -> session))) |
|
346 } |
347 } |
347 } |
348 } |
348 } |
349 } |
349 } |
350 } |
350 } |
351 } |