# HG changeset patch # User wenzelm # Date 1476791094 -7200 # Node ID 0f000101652a98f39c02b1bbc2da700a5b8d71e6 # Parent 12a47f263122ea8d8a0f4a73342a35facb7f0c5d tuned; diff -r 12a47f263122 -r 0f000101652a src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala Tue Oct 18 11:50:38 2016 +0200 +++ b/src/Pure/Admin/build_history.scala Tue Oct 18 13:44:54 2016 +0200 @@ -203,15 +203,15 @@ val meta_info = (if (build_tags.isEmpty) Nil - else List(Build_Log.Field.build_tags -> Word.implode(build_tags))) ::: + else List(Build_Log.Prop.build_tags -> Word.implode(build_tags))) ::: List( - Build_Log.Field.build_group_id -> build_group_id, - Build_Log.Field.build_id -> (build_host + ":" + build_start.time.ms), - Build_Log.Field.build_engine -> BUILD_HISTORY, - Build_Log.Field.build_host -> build_host, - Build_Log.Field.build_start -> Build_Log.print_date(build_start), - Build_Log.Field.build_end -> Build_Log.print_date(build_end), - Build_Log.Field.isabelle_version -> isabelle_version) + Build_Log.Prop.build_group_id -> build_group_id, + Build_Log.Prop.build_id -> (build_host + ":" + build_start.time.ms), + Build_Log.Prop.build_engine -> BUILD_HISTORY, + Build_Log.Prop.build_host -> build_host, + Build_Log.Prop.build_start -> Build_Log.print_date(build_start), + Build_Log.Prop.build_end -> Build_Log.print_date(build_end), + Build_Log.Prop.isabelle_version -> isabelle_version) val ml_statistics = build_info.finished_sessions.flatMap(session_name => diff -r 12a47f263122 -r 0f000101652a src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Tue Oct 18 11:50:38 2016 +0200 +++ b/src/Pure/Admin/build_log.scala Tue Oct 18 13:44:54 2016 +0200 @@ -18,36 +18,25 @@ object Build_Log { - /** directory content **/ + /** content **/ - /* file names */ + /* properties */ - def log_date(date: Date): String = - String.format(Locale.ROOT, "%s.%05d", - DateTimeFormatter.ofPattern("yyyy-MM-dd").format(date.rep), - new java.lang.Long((date.time - date.midnight.time).ms / 1000)) - - def log_subdir(date: Date): Path = - Path.explode("log") + Path.explode(date.rep.getYear.toString) - - def log_filename(engine: String, date: Date, more: List[String] = Nil): Path = - Path.explode((engine :: log_date(date) :: more).mkString("", "_", ".log")) + object Prop + { + val build_tags = "build_tags" + val build_group_id = "build_group_id" + val build_id = "build_id" + val build_engine = "build_engine" + val build_host = "build_host" + val build_start = "build_start" + val build_end = "build_end" + val isabelle_version = "isabelle_version" + val afp_version = "afp_version" + } - /* log file collections */ - - def is_log(file: JFile): Boolean = - List(".log", ".log.gz", ".log.xz").exists(ext => file.getName.endsWith(ext)) - - def isatest_files(dir: Path): List[JFile] = - File.find_files(dir.file, file => is_log(file) && file.getName.startsWith("isatest-makeall-")) - - def afp_test_files(dir: Path): List[JFile] = - File.find_files(dir.file, file => is_log(file) && file.getName.startsWith("afp-test-devel-")) - - - - /** settings **/ + /* settings */ object Settings { @@ -78,6 +67,32 @@ } + /* file names */ + + def log_date(date: Date): String = + String.format(Locale.ROOT, "%s.%05d", + DateTimeFormatter.ofPattern("yyyy-MM-dd").format(date.rep), + new java.lang.Long((date.time - date.midnight.time).ms / 1000)) + + def log_subdir(date: Date): Path = + Path.explode("log") + Path.explode(date.rep.getYear.toString) + + def log_filename(engine: String, date: Date, more: List[String] = Nil): Path = + Path.explode((engine :: log_date(date) :: more).mkString("", "_", ".log")) + + + /* log file collections */ + + def is_log(file: JFile): Boolean = + List(".log", ".log.gz", ".log.xz").exists(ext => file.getName.endsWith(ext)) + + def isatest_files(dir: Path): List[JFile] = + File.find_files(dir.file, file => is_log(file) && file.getName.startsWith("isatest-makeall-")) + + def afp_test_files(dir: Path): List[JFile] = + File.find_files(dir.file, file => is_log(file) && file.getName.startsWith("afp-test-devel-")) + + /** log file **/ @@ -245,19 +260,6 @@ /** meta info **/ - object Field - { - val build_tags = "build_tags" - val build_group_id = "build_group_id" - val build_id = "build_id" - val build_engine = "build_engine" - val build_host = "build_host" - val build_start = "build_start" - val build_end = "build_end" - val isabelle_version = "isabelle_version" - val afp_version = "afp_version" - } - object Meta_Info { val empty: Meta_Info = Meta_Info(Nil, Nil) @@ -311,23 +313,23 @@ val prefix = if (host != "") host else if (engine != "") engine else "" (if (prefix == "") "build" else prefix) + ":" + start.time.ms } - val build_engine = if (engine == "") Nil else List(Field.build_engine -> engine) - val build_host = if (host == "") Nil else List(Field.build_host -> host) + val build_engine = if (engine == "") Nil else List(Prop.build_engine -> engine) + val build_host = if (host == "") Nil else List(Prop.build_host -> host) - val start_date = List(Field.build_start -> start.toString) + val start_date = List(Prop.build_start -> start.toString) val end_date = log_file.lines.last match { case End(log_file.Strict_Date(end_date)) => - List(Field.build_end -> end_date.toString) + List(Prop.build_end -> end_date.toString) case _ => Nil } val isabelle_version = - log_file.find_match(Isabelle_Version).map(Field.isabelle_version -> _) + log_file.find_match(Isabelle_Version).map(Prop.isabelle_version -> _) val afp_version = - log_file.find_match(AFP_Version).map(Field.afp_version -> _) + log_file.find_match(AFP_Version).map(Prop.afp_version -> _) - Meta_Info((Field.build_id -> build_id) :: build_engine ::: build_host ::: + Meta_Info((Prop.build_id -> build_id) :: build_engine ::: build_host ::: start_date ::: end_date ::: isabelle_version.toList ::: afp_version.toList, log_file.get_settings(Settings.all_settings)) }