65 for (profile <- profiles.sortBy(_.name)) { |
65 for (profile <- profiles.sortBy(_.name)) { |
66 progress.echo("input " + quote(profile.name)) |
66 progress.echo("input " + quote(profile.name)) |
67 val columns = |
67 val columns = |
68 List( |
68 List( |
69 Build_Log.Data.pull_date, |
69 Build_Log.Data.pull_date, |
|
70 Build_Log.Settings.ISABELLE_BUILD_OPTIONS, |
70 Build_Log.Settings.ML_PLATFORM, |
71 Build_Log.Settings.ML_PLATFORM, |
71 Build_Log.Data.session_name, |
72 Build_Log.Data.session_name, |
72 Build_Log.Data.threads, |
73 Build_Log.Data.threads, |
73 Build_Log.Data.timing_elapsed, |
74 Build_Log.Data.timing_elapsed, |
74 Build_Log.Data.timing_cpu, |
75 Build_Log.Data.timing_cpu, |
75 Build_Log.Data.timing_gc, |
76 Build_Log.Data.timing_gc, |
76 Build_Log.Data.ml_timing_elapsed, |
77 Build_Log.Data.ml_timing_elapsed, |
77 Build_Log.Data.ml_timing_cpu, |
78 Build_Log.Data.ml_timing_cpu, |
78 Build_Log.Data.ml_timing_gc) |
79 Build_Log.Data.ml_timing_gc) |
79 |
80 |
|
81 val Threads_Option = """threads\s*=\s*(\d+)""".r |
|
82 |
80 val sql = profile.select(columns, history_length, only_sessions) |
83 val sql = profile.select(columns, history_length, only_sessions) |
81 if (verbose) progress.echo(sql) |
84 if (verbose) progress.echo(sql) |
82 |
85 |
83 db.using_statement(sql)(stmt => |
86 db.using_statement(sql)(stmt => |
84 { |
87 { |
85 val res = stmt.execute_query() |
88 val res = stmt.execute_query() |
86 while (res.next()) { |
89 while (res.next()) { |
87 val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM) |
90 val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM) |
88 val threads = res.get_int(Build_Log.Data.threads) |
91 |
|
92 val threads_option = |
|
93 res.string(Build_Log.Settings.ISABELLE_BUILD_OPTIONS) match { |
|
94 case Threads_Option(Value.Int(i)) => i |
|
95 case _ => 1 |
|
96 } |
|
97 val threads = res.get_int(Build_Log.Data.threads).getOrElse(1) |
|
98 |
89 val name = |
99 val name = |
90 profile.name + |
100 profile.name + |
91 "_m" + (if (ml_platform.startsWith("x86_64")) "64" else "32") + |
101 "_m" + (if (ml_platform.startsWith("x86_64")) "64" else "32") + |
92 "_M" + threads.getOrElse(1) |
102 "_M" + (threads_option max threads) |
93 |
103 |
94 val session = res.string(Build_Log.Data.session_name) |
104 val session = res.string(Build_Log.Data.session_name) |
95 val entry = |
105 val entry = |
96 Entry(res.date(Build_Log.Data.pull_date), |
106 Entry(res.date(Build_Log.Data.pull_date), |
97 res.timing( |
107 res.timing( |