--- 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)
+ }
}