20 |
20 |
21 |
21 |
22 /* data profiles */ |
22 /* data profiles */ |
23 |
23 |
24 sealed case class Profile( |
24 sealed case class Profile( |
25 description: String, history: Int = 0, afp: Boolean = false, sql: String) |
25 description: String, history: Int = 0, afp: Boolean = false, slow: Boolean = false, sql: String) |
26 { |
26 { |
27 def days(options: Options): Int = options.int("build_log_history") max history |
27 def days(options: Options): Int = options.int("build_log_history") max history |
28 |
28 |
29 def stretch(options: Options): Double = |
29 def stretch(options: Options): Double = |
30 (days(options) max default_history min (default_history * 5)).toDouble / default_history |
30 (days(options) max default_history min (default_history * 5)).toDouble / default_history |
166 Build_Log.Prop.afp_version, |
166 Build_Log.Prop.afp_version, |
167 Build_Log.Settings.ISABELLE_BUILD_OPTIONS, |
167 Build_Log.Settings.ISABELLE_BUILD_OPTIONS, |
168 Build_Log.Settings.ML_PLATFORM, |
168 Build_Log.Settings.ML_PLATFORM, |
169 Build_Log.Data.session_name, |
169 Build_Log.Data.session_name, |
170 Build_Log.Data.chapter, |
170 Build_Log.Data.chapter, |
|
171 Build_Log.Data.groups, |
171 Build_Log.Data.threads, |
172 Build_Log.Data.threads, |
172 Build_Log.Data.timing_elapsed, |
173 Build_Log.Data.timing_elapsed, |
173 Build_Log.Data.timing_cpu, |
174 Build_Log.Data.timing_cpu, |
174 Build_Log.Data.timing_gc, |
175 Build_Log.Data.timing_gc, |
175 Build_Log.Data.ml_timing_elapsed, |
176 Build_Log.Data.ml_timing_elapsed, |
189 { |
190 { |
190 val res = stmt.execute_query() |
191 val res = stmt.execute_query() |
191 while (res.next()) { |
192 while (res.next()) { |
192 val session_name = res.string(Build_Log.Data.session_name) |
193 val session_name = res.string(Build_Log.Data.session_name) |
193 val chapter = res.string(Build_Log.Data.chapter) |
194 val chapter = res.string(Build_Log.Data.chapter) |
|
195 val groups = split_lines(res.string(Build_Log.Data.groups)) |
194 val threads = |
196 val threads = |
195 { |
197 { |
196 val threads1 = |
198 val threads1 = |
197 res.string(Build_Log.Settings.ISABELLE_BUILD_OPTIONS) match { |
199 res.string(Build_Log.Settings.ISABELLE_BUILD_OPTIONS) match { |
198 case Threads_Option(Value.Int(i)) => i |
200 case Threads_Option(Value.Int(i)) => i |
246 |
248 |
247 val sessions = data_entries.getOrElse(data_name, Map.empty) |
249 val sessions = data_entries.getOrElse(data_name, Map.empty) |
248 val entries = sessions.get(session_name).map(_.entries) getOrElse Nil |
250 val entries = sessions.get(session_name).map(_.entries) getOrElse Nil |
249 val session = Session(session_name, threads, entry :: entries, ml_stats) |
251 val session = Session(session_name, threads, entry :: entries, ml_stats) |
250 |
252 |
251 if (!afp || chapter == "AFP") { |
253 if ((!afp || chapter == "AFP") && (!profile.slow || groups.contains("slow"))) { |
252 data_entries += (data_name -> (sessions + (session_name -> session))) |
254 data_entries += (data_name -> (sessions + (session_name -> session))) |
253 } |
255 } |
254 } |
256 } |
255 }) |
257 }) |
256 } |
258 } |