44 val build_start = SQL.Column.date("build_start") |
44 val build_start = SQL.Column.date("build_start") |
45 val build_end = SQL.Column.date("build_end") |
45 val build_end = SQL.Column.date("build_end") |
46 val isabelle_version = SQL.Column.string("isabelle_version") |
46 val isabelle_version = SQL.Column.string("isabelle_version") |
47 val afp_version = SQL.Column.string("afp_version") |
47 val afp_version = SQL.Column.string("afp_version") |
48 |
48 |
49 val columns: List[SQL.Column] = |
49 val all_props: List[SQL.Column] = |
50 List(build_tags, build_args, build_group_id, build_id, build_engine, |
50 List(build_tags, build_args, build_group_id, build_id, build_engine, |
51 build_host, build_start, build_end, isabelle_version, afp_version) |
51 build_host, build_start, build_end, isabelle_version, afp_version) |
52 } |
52 } |
53 |
53 |
54 |
54 |
55 /* settings */ |
55 /* settings */ |
56 |
56 |
57 object Settings |
57 object Settings |
58 { |
58 { |
59 val build_settings = List("ISABELLE_BUILD_OPTIONS") |
59 val ISABELLE_BUILD_OPTIONS = SQL.Column.string("ISABELLE_BUILD_OPTIONS") |
60 val ml_settings = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS") |
60 val ML_PLATFORM = SQL.Column.string("ML_PLATFORM") |
61 val all_settings = build_settings ::: ml_settings |
61 val ML_HOME = SQL.Column.string("ML_HOME") |
|
62 val ML_SYSTEM = SQL.Column.string("ML_SYSTEM") |
|
63 val ML_OPTIONS = SQL.Column.string("ML_OPTIONS") |
|
64 |
|
65 val ml_settings = List(ML_PLATFORM, ML_HOME, ML_SYSTEM, ML_OPTIONS) |
|
66 val all_settings = ISABELLE_BUILD_OPTIONS :: ml_settings |
62 |
67 |
63 type Entry = (String, String) |
68 type Entry = (String, String) |
64 type T = List[Entry] |
69 type T = List[Entry] |
65 |
70 |
66 object Entry |
71 object Entry |
239 lines.find(_.startsWith(a + "=")) match { |
245 lines.find(_.startsWith(a + "=")) match { |
240 case Some(line) => Settings.Entry.unapply(line) |
246 case Some(line) => Settings.Entry.unapply(line) |
241 case None => None |
247 case None => None |
242 } |
248 } |
243 |
249 |
244 def get_settings(as: List[String]): Settings.T = |
250 def get_all_settings: Settings.T = |
245 for { a <- as; entry <- get_setting(a) } yield entry |
251 for { c <- Settings.all_settings; entry <- get_setting(c.name) } |
|
252 yield entry |
246 |
253 |
247 |
254 |
248 /* properties (YXML) */ |
255 /* properties (YXML) */ |
249 |
256 |
250 val xml_cache = new XML.Cache() |
257 val xml_cache = new XML.Cache() |
286 object Meta_Info |
293 object Meta_Info |
287 { |
294 { |
288 val empty: Meta_Info = Meta_Info(Nil, Nil) |
295 val empty: Meta_Info = Meta_Info(Nil, Nil) |
289 |
296 |
290 val log_name = SQL.Column.string("log_name", primary_key = true) |
297 val log_name = SQL.Column.string("log_name", primary_key = true) |
291 val settings = SQL.Column.bytes("settings") |
|
292 |
|
293 val table = |
298 val table = |
294 SQL.Table("isabelle_build_log_meta_info", log_name :: Prop.columns ::: List(settings)) |
299 SQL.Table("isabelle_build_log_meta_info", log_name :: Prop.all_props ::: Settings.all_settings) |
295 } |
300 } |
296 |
301 |
297 sealed case class Meta_Info(props: Properties.T, settings: List[(String, String)]) |
302 sealed case class Meta_Info(props: Properties.T, settings: Settings.T) |
298 { |
303 { |
299 def is_empty: Boolean = props.isEmpty && settings.isEmpty |
304 def is_empty: Boolean = props.isEmpty && settings.isEmpty |
300 |
305 |
301 def get(c: SQL.Column): Option[String] = Properties.get(props, c.name) |
306 def get(c: SQL.Column): Option[String] = |
302 def get_date(c: SQL.Column): Option[Date] = get(c).map(Log_File.Date_Format.parse(_)) |
307 Properties.get(props, c.name) orElse |
|
308 Properties.get(settings, c.name) |
|
309 |
|
310 def get_date(c: SQL.Column): Option[Date] = |
|
311 get(c).map(Log_File.Date_Format.parse(_)) |
303 } |
312 } |
304 |
313 |
305 object Isatest |
314 object Isatest |
306 { |
315 { |
307 val log_prefix = "isatest-makeall-" |
316 val log_prefix = "isatest-makeall-" |
363 val afp_version = |
372 val afp_version = |
364 log_file.find_match(AFP_Version).map(Prop.afp_version.name -> _) |
373 log_file.find_match(AFP_Version).map(Prop.afp_version.name -> _) |
365 |
374 |
366 Meta_Info((Prop.build_id.name -> build_id) :: build_engine ::: build_host ::: |
375 Meta_Info((Prop.build_id.name -> build_id) :: build_engine ::: build_host ::: |
367 start_date ::: end_date ::: isabelle_version.toList ::: afp_version.toList, |
376 start_date ::: end_date ::: isabelle_version.toList ::: afp_version.toList, |
368 log_file.get_settings(Settings.all_settings)) |
377 log_file.get_all_settings) |
369 } |
378 } |
370 |
379 |
371 log_file.lines match { |
380 log_file.lines match { |
372 case line :: _ if line.startsWith(Build_History.META_INFO_MARKER) => |
381 case line :: _ if line.startsWith(Build_History.META_INFO_MARKER) => |
373 Meta_Info(log_file.find_props(Build_History.META_INFO_MARKER).get, |
382 Meta_Info(log_file.find_props(Build_History.META_INFO_MARKER).get, |
374 log_file.get_settings(Settings.all_settings)) |
383 log_file.get_all_settings) |
375 |
384 |
376 case Isatest.Start(log_file.Strict_Date(start), host) :: _ => |
385 case Isatest.Start(log_file.Strict_Date(start), host) :: _ => |
377 parse(Isatest.engine, host, start, Isatest.End, |
386 parse(Isatest.engine, host, start, Isatest.End, |
378 Isatest.Isabelle_Version, Isatest.No_AFP_Version) |
387 Isatest.Isabelle_Version, Isatest.No_AFP_Version) |
379 |
388 |
682 for (file <- filter_files(db, Meta_Info.table, files)) { |
691 for (file <- filter_files(db, Meta_Info.table, files)) { |
683 val log_file = Log_File(file) |
692 val log_file = Log_File(file) |
684 val meta_info = log_file.parse_meta_info() |
693 val meta_info = log_file.parse_meta_info() |
685 |
694 |
686 db.set_string(stmt, 1, log_file.name) |
695 db.set_string(stmt, 1, log_file.name) |
687 for ((c, i) <- Prop.columns.zipWithIndex) { |
696 for ((c, i) <- Meta_Info.table.columns.tail.zipWithIndex) { |
688 if (c.T == SQL.Type.Date) |
697 if (c.T == SQL.Type.Date) |
689 db.set_date(stmt, i + 2, meta_info.get_date(c).orNull) |
698 db.set_date(stmt, i + 2, meta_info.get_date(c).orNull) |
690 else |
699 else |
691 db.set_string(stmt, i + 2, meta_info.get(c).map(Prop.multiple_lines(_)).orNull) |
700 db.set_string(stmt, i + 2, meta_info.get(c).map(Prop.multiple_lines(_)).orNull) |
692 } |
701 } |
693 db.set_bytes(stmt, Meta_Info.table.columns.length, encode_properties(meta_info.settings)) |
|
694 |
702 |
695 stmt.execute() |
703 stmt.execute() |
696 } |
704 } |
697 }) |
705 }) |
698 } |
706 } |