28 |
28 |
29 def multiple(name: String, args: List[String]): Properties.T = |
29 def multiple(name: String, args: List[String]): Properties.T = |
30 if (args.isEmpty) Nil |
30 if (args.isEmpty) Nil |
31 else List(name -> args.mkString(separator.toString)) |
31 else List(name -> args.mkString(separator.toString)) |
32 |
32 |
33 val build_tags = "build_tags" // multiple |
33 val build_tags = SQL.Column.string("build_tags") // multiple |
34 val build_args = "build_args" // multiple |
34 val build_args = SQL.Column.string("build_args") // multiple |
35 val build_group_id = "build_group_id" |
35 val build_group_id = SQL.Column.string("build_group_id") |
36 val build_id = "build_id" |
36 val build_id = SQL.Column.string("build_id") |
37 val build_engine = "build_engine" |
37 val build_engine = SQL.Column.string("build_engine") |
38 val build_host = "build_host" |
38 val build_host = SQL.Column.string("build_host") |
39 val build_start = "build_start" |
39 val build_start = SQL.Column.date("build_start") |
40 val build_end = "build_end" |
40 val build_end = SQL.Column.date("build_end") |
41 val isabelle_version = "isabelle_version" |
41 val isabelle_version = SQL.Column.string("isabelle_version") |
42 val afp_version = "afp_version" |
42 val afp_version = SQL.Column.string("afp_version") |
|
43 |
|
44 val columns: List[SQL.Column] = |
|
45 List(build_tags, build_args, build_group_id, build_id, build_engine, |
|
46 build_host, build_start, build_end, isabelle_version, afp_version) |
43 } |
47 } |
44 |
48 |
45 |
49 |
46 /* settings */ |
50 /* settings */ |
47 |
51 |
271 /** digested meta info: produced by Admin/build_history in log.xz file **/ |
275 /** digested meta info: produced by Admin/build_history in log.xz file **/ |
272 |
276 |
273 object Meta_Info |
277 object Meta_Info |
274 { |
278 { |
275 val empty: Meta_Info = Meta_Info(Nil, Nil) |
279 val empty: Meta_Info = Meta_Info(Nil, Nil) |
|
280 |
|
281 val log_filename = SQL.Column.string("log_filename", primary_key = true) |
|
282 |
|
283 val columns: List[SQL.Column] = |
|
284 log_filename :: Prop.columns ::: Settings.all_settings.map(SQL.Column.string(_)) |
276 } |
285 } |
277 |
286 |
278 sealed case class Meta_Info(props: Properties.T, settings: List[(String, String)]) |
287 sealed case class Meta_Info(props: Properties.T, settings: List[(String, String)]) |
279 { |
288 { |
280 def is_empty: Boolean = props.isEmpty && settings.isEmpty |
289 def is_empty: Boolean = props.isEmpty && settings.isEmpty |
323 val build_id = |
332 val build_id = |
324 { |
333 { |
325 val prefix = if (host != "") host else if (engine != "") engine else "" |
334 val prefix = if (host != "") host else if (engine != "") engine else "" |
326 (if (prefix == "") "build" else prefix) + ":" + start.time.ms |
335 (if (prefix == "") "build" else prefix) + ":" + start.time.ms |
327 } |
336 } |
328 val build_engine = if (engine == "") Nil else List(Prop.build_engine -> engine) |
337 val build_engine = if (engine == "") Nil else List(Prop.build_engine.name -> engine) |
329 val build_host = if (host == "") Nil else List(Prop.build_host -> host) |
338 val build_host = if (host == "") Nil else List(Prop.build_host.name -> host) |
330 |
339 |
331 val start_date = List(Prop.build_start -> start.toString) |
340 val start_date = List(Prop.build_start.name -> start.toString) |
332 val end_date = |
341 val end_date = |
333 log_file.lines.last match { |
342 log_file.lines.last match { |
334 case End(log_file.Strict_Date(end_date)) => |
343 case End(log_file.Strict_Date(end_date)) => |
335 List(Prop.build_end -> end_date.toString) |
344 List(Prop.build_end.name -> end_date.toString) |
336 case _ => Nil |
345 case _ => Nil |
337 } |
346 } |
338 |
347 |
339 val isabelle_version = |
348 val isabelle_version = |
340 log_file.find_match(Isabelle_Version).map(Prop.isabelle_version -> _) |
349 log_file.find_match(Isabelle_Version).map(Prop.isabelle_version.name -> _) |
341 val afp_version = |
350 val afp_version = |
342 log_file.find_match(AFP_Version).map(Prop.afp_version -> _) |
351 log_file.find_match(AFP_Version).map(Prop.afp_version.name -> _) |
343 |
352 |
344 Meta_Info((Prop.build_id -> build_id) :: build_engine ::: build_host ::: |
353 Meta_Info((Prop.build_id.name -> build_id) :: build_engine ::: build_host ::: |
345 start_date ::: end_date ::: isabelle_version.toList ::: afp_version.toList, |
354 start_date ::: end_date ::: isabelle_version.toList ::: afp_version.toList, |
346 log_file.get_settings(Settings.all_settings)) |
355 log_file.get_settings(Settings.all_settings)) |
347 } |
356 } |
348 |
357 |
349 log_file.lines match { |
358 log_file.lines match { |