478 val groups = SQL.Column.string("groups") |
478 val groups = SQL.Column.string("groups") |
479 val threads = SQL.Column.int("threads") |
479 val threads = SQL.Column.int("threads") |
480 val timing_elapsed = SQL.Column.long("timing_elapsed") |
480 val timing_elapsed = SQL.Column.long("timing_elapsed") |
481 val timing_cpu = SQL.Column.long("timing_cpu") |
481 val timing_cpu = SQL.Column.long("timing_cpu") |
482 val timing_gc = SQL.Column.long("timing_gc") |
482 val timing_gc = SQL.Column.long("timing_gc") |
|
483 val timing_factor = SQL.Column.double("timing_factor") |
483 val ml_timing_elapsed = SQL.Column.long("ml_timing_elapsed") |
484 val ml_timing_elapsed = SQL.Column.long("ml_timing_elapsed") |
484 val ml_timing_cpu = SQL.Column.long("ml_timing_cpu") |
485 val ml_timing_cpu = SQL.Column.long("ml_timing_cpu") |
485 val ml_timing_gc = SQL.Column.long("ml_timing_gc") |
486 val ml_timing_gc = SQL.Column.long("ml_timing_gc") |
|
487 val ml_timing_factor = SQL.Column.double("ml_timing_factor") |
486 val heap_size = SQL.Column.long("heap_size") |
488 val heap_size = SQL.Column.long("heap_size") |
487 val status = SQL.Column.string("status") |
489 val status = SQL.Column.string("status") |
488 val ml_statistics = SQL.Column.bytes("ml_statistics") |
490 val ml_statistics = SQL.Column.bytes("ml_statistics") |
489 |
491 |
490 val sessions_table = |
492 val sessions_table = |
491 SQL.Table("isabelle_build_log_sessions", |
493 SQL.Table("isabelle_build_log_sessions", |
492 List(Meta_Info.log_name, session_name, chapter, groups, threads, timing_elapsed, timing_cpu, |
494 List(Meta_Info.log_name, session_name, chapter, groups, threads, timing_elapsed, timing_cpu, |
493 timing_gc, ml_timing_elapsed, ml_timing_cpu, ml_timing_gc, heap_size, status)) |
495 timing_gc, timing_factor, ml_timing_elapsed, ml_timing_cpu, ml_timing_gc, ml_timing_factor, |
|
496 heap_size, status)) |
494 val ml_statistics_table = |
497 val ml_statistics_table = |
495 SQL.Table("isabelle_build_log_ml_statistics", |
498 SQL.Table("isabelle_build_log_ml_statistics", |
496 List(Meta_Info.log_name, session_name, ml_statistics)) |
499 List(Meta_Info.log_name, session_name, ml_statistics)) |
497 } |
500 } |
498 |
501 |
718 db.set_string(stmt, 4, session.proper_groups) |
721 db.set_string(stmt, 4, session.proper_groups) |
719 db.set_int(stmt, 5, session.threads) |
722 db.set_int(stmt, 5, session.threads) |
720 db.set_long(stmt, 6, session.timing.elapsed.proper_ms) |
723 db.set_long(stmt, 6, session.timing.elapsed.proper_ms) |
721 db.set_long(stmt, 7, session.timing.cpu.proper_ms) |
724 db.set_long(stmt, 7, session.timing.cpu.proper_ms) |
722 db.set_long(stmt, 8, session.timing.gc.proper_ms) |
725 db.set_long(stmt, 8, session.timing.gc.proper_ms) |
723 db.set_long(stmt, 9, session.ml_timing.elapsed.proper_ms) |
726 db.set_double(stmt, 9, session.timing.factor) |
724 db.set_long(stmt, 10, session.ml_timing.cpu.proper_ms) |
727 db.set_long(stmt, 10, session.ml_timing.elapsed.proper_ms) |
725 db.set_long(stmt, 11, session.ml_timing.gc.proper_ms) |
728 db.set_long(stmt, 11, session.ml_timing.cpu.proper_ms) |
726 db.set_long(stmt, 12, session.heap_size) |
729 db.set_long(stmt, 12, session.ml_timing.gc.proper_ms) |
727 db.set_string(stmt, 13, session.status.map(_.toString)) |
730 db.set_double(stmt, 13, session.ml_timing.factor) |
|
731 db.set_long(stmt, 14, session.heap_size) |
|
732 db.set_string(stmt, 15, session.status.map(_.toString)) |
728 stmt.execute() |
733 stmt.execute() |
729 } |
734 } |
730 }) |
735 }) |
731 } |
736 } |
732 } |
737 } |