# HG changeset patch # User wenzelm # Date 1493742471 -7200 # Node ID 4a762cad298fe246be80e3abbee0a2dc3cb25639 # Parent eba08da54c6b59e995c16609b1fccd0e10f4b846# Parent 47bbf7150aae2d7a58b41200e6619007900a0db6 merged diff -r eba08da54c6b -r 4a762cad298f src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Tue May 02 14:34:17 2017 +0100 +++ b/src/Pure/Admin/build_log.scala Tue May 02 18:27:51 2017 +0200 @@ -230,9 +230,13 @@ def find_line(marker: String): Option[String] = find(Library.try_unprefix(marker, _)) - def find_match(regex: Regex): Option[String] = - lines.iterator.map(regex.unapplySeq(_)).find(res => res.isDefined && res.get.length == 1). - map(res => res.get.head) + def find_match(regexes: List[Regex]): Option[String] = + regexes match { + case Nil => None + case regex :: rest => + lines.iterator.map(regex.unapplySeq(_)).find(res => res.isDefined && res.get.length == 1). + map(res => res.get.head) orElse find_match(rest) + } /* settings */ @@ -324,8 +328,8 @@ val Start = new Regex("""^isabelle_identify: (.+)$""") val No_End = new Regex("""$.""") - val Isabelle_Version = new Regex("""^Isabelle version: (\S+)$""") - val AFP_Version = new Regex("""^AFP version: (\S+)$""") + val Isabelle_Version = List(new Regex("""^Isabelle version: (\S+)$""")) + val AFP_Version = List(new Regex("""^AFP version: (\S+)$""")) } object Isatest @@ -334,8 +338,7 @@ val engine = "isatest" val Start = new Regex("""^------------------- starting test --- (.+) --- (.+)$""") val End = new Regex("""^------------------- test (?:successful|FAILED) --- (.+) --- .*$""") - val Isabelle_Version = new Regex("""^Isabelle version: (\S+)$""") - val No_AFP_Version = new Regex("""$.""") + val Isabelle_Version = List(new Regex("""^Isabelle version: (\S+)$""")) } object AFP_Test @@ -345,8 +348,8 @@ val Start = new Regex("""^Start test(?: for .+)? at ([^,]+), (.*)$""") val Start_Old = new Regex("""^Start test(?: for .+)? at ([^,]+)$""") val End = new Regex("""^End test on (.+), .+, elapsed time:.*$""") - val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\S+)$""") - val AFP_Version = new Regex("""^AFP version: .* -- hg id (\S+)$""") + val Isabelle_Version = List(new Regex("""^Isabelle version: .* -- hg id (\S+)$""")) + val AFP_Version = List(new Regex("""^AFP version: .* -- hg id (\S+)$""")) val Bad_Init = new Regex("""^cp:.*: Disc quota exceeded$""") } @@ -359,9 +362,12 @@ val Start_Date = new Regex("""^Build started at (.+)$""") val No_End = new Regex("""$.""") val Isabelle_Version = - new Regex("""^(?:Build for Isabelle id |Isabelle id |ISABELLE_CI_REPO_ID=")(\w+).*$""") + List(new Regex("""^(?:Build for Isabelle id|Isabelle id) (\w+).*$"""), + new Regex("""^ISABELLE_CI_REPO_ID="(\w+)".*$"""), + new Regex("""^(\w{12}) tip.*$""")) val AFP_Version = - new Regex("""^(?:Build for AFP id |AFP id |ISABELLE_CI_AFP_ID=")(\w+).*$""") + List(new Regex("""^(?:Build for AFP id|AFP id) (\w+).*$"""), + new Regex("""^ISABELLE_CI_AFP_ID="(\w+)".*$""")) val CONFIGURATION = "=== CONFIGURATION ===" val BUILD = "=== BUILD ===" } @@ -369,7 +375,7 @@ private def parse_meta_info(log_file: Log_File): Meta_Info = { def parse(engine: String, host: String, start: Date, - End: Regex, Isabelle_Version: Regex, AFP_Version: Regex): Meta_Info = + End: Regex, Isabelle_Version: List[Regex], AFP_Version: List[Regex]): Meta_Info = { val build_id = { @@ -408,7 +414,7 @@ case Isatest.Start(log_file.Strict_Date(start), host) :: _ => parse(Isatest.engine, host, start, Isatest.End, - Isatest.Isabelle_Version, Isatest.No_AFP_Version) + Isatest.Isabelle_Version, Nil) case AFP_Test.Start(log_file.Strict_Date(start), host) :: _ => parse(AFP_Test.engine, host, start, AFP_Test.End, @@ -480,9 +486,11 @@ val timing_elapsed = SQL.Column.long("timing_elapsed") val timing_cpu = SQL.Column.long("timing_cpu") val timing_gc = SQL.Column.long("timing_gc") + val timing_factor = SQL.Column.double("timing_factor") val ml_timing_elapsed = SQL.Column.long("ml_timing_elapsed") val ml_timing_cpu = SQL.Column.long("ml_timing_cpu") val ml_timing_gc = SQL.Column.long("ml_timing_gc") + val ml_timing_factor = SQL.Column.double("ml_timing_factor") val heap_size = SQL.Column.long("heap_size") val status = SQL.Column.string("status") val ml_statistics = SQL.Column.bytes("ml_statistics") @@ -490,7 +498,8 @@ val sessions_table = SQL.Table("isabelle_build_log_sessions", List(Meta_Info.log_name, session_name, chapter, groups, threads, timing_elapsed, timing_cpu, - timing_gc, ml_timing_elapsed, ml_timing_cpu, ml_timing_gc, heap_size, status)) + timing_gc, timing_factor, ml_timing_elapsed, ml_timing_cpu, ml_timing_gc, ml_timing_factor, + heap_size, status)) val ml_statistics_table = SQL.Table("isabelle_build_log_ml_statistics", List(Meta_Info.log_name, session_name, ml_statistics)) @@ -720,11 +729,13 @@ db.set_long(stmt, 6, session.timing.elapsed.proper_ms) db.set_long(stmt, 7, session.timing.cpu.proper_ms) db.set_long(stmt, 8, session.timing.gc.proper_ms) - db.set_long(stmt, 9, session.ml_timing.elapsed.proper_ms) - db.set_long(stmt, 10, session.ml_timing.cpu.proper_ms) - db.set_long(stmt, 11, session.ml_timing.gc.proper_ms) - db.set_long(stmt, 12, session.heap_size) - db.set_string(stmt, 13, session.status.map(_.toString)) + db.set_double(stmt, 9, session.timing.factor) + db.set_long(stmt, 10, session.ml_timing.elapsed.proper_ms) + db.set_long(stmt, 11, session.ml_timing.cpu.proper_ms) + db.set_long(stmt, 12, session.ml_timing.gc.proper_ms) + db.set_double(stmt, 13, session.ml_timing.factor) + db.set_long(stmt, 14, session.heap_size) + db.set_string(stmt, 15, session.status.map(_.toString)) stmt.execute() } }) @@ -899,4 +910,15 @@ Meta_Info.log_name(table1).sql + " = " + Meta_Info.log_name(table2).sql)) } } + + + /* main operations */ + + def database_update(store: Store, db: SQL.Database, dirs: List[Path], + ml_statistics: Boolean = false, full_view: Boolean = false) + { + val files = Log_File.find_files(dirs) + store.write_info(db, files, ml_statistics = ml_statistics) + if (full_view) Build_Log.create_full_view(db) + } } diff -r eba08da54c6b -r 4a762cad298f src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Tue May 02 14:34:17 2017 +0100 +++ b/src/Pure/Admin/isabelle_cronjob.scala Tue May 02 18:27:51 2017 +0200 @@ -148,14 +148,8 @@ def database_update(options: Options) { val store = Build_Log.store(options) - val files = Build_Log.Log_File.find_files(database_dirs) - - // PostgreSQL server using(store.open_database())(db => - { - store.write_info(db, files, ml_statistics = true) - Build_Log.create_full_view(db) - }) + Build_Log.database_update(store, db, database_dirs, ml_statistics = true, full_view = true)) }