src/Pure/Admin/build_log.scala

 import scala.collection.immutable.SortedMap
 import scala.collection.mutable
 import scala.util.matching.Regex
 
 
-object Build_Log
-{
+object Build_Log {
   /** content **/
 
   /* properties */
 
-  object Prop
-  {
+  object Prop {
     val build_tags = SQL.Column.string("build_tags")  // lines
     val build_args = SQL.Column.string("build_args")  // lines
     val build_group_id = SQL.Column.string("build_group_id")
     val build_id = SQL.Column.string("build_id")
     val build_engine = SQL.Column.string("build_engine")

   }
 
 
   /* settings */
 
-  object Settings
-  {
+  object Settings {
     val ISABELLE_BUILD_OPTIONS = SQL.Column.string("ISABELLE_BUILD_OPTIONS")
     val ML_PLATFORM = SQL.Column.string("ML_PLATFORM")
     val ML_HOME = SQL.Column.string("ML_HOME")
     val ML_SYSTEM = SQL.Column.string("ML_SYSTEM")
     val ML_OPTIONS = SQL.Column.string("ML_OPTIONS")

     val all_settings = ISABELLE_BUILD_OPTIONS :: ml_settings
 
     type Entry = (String, String)
     type T = List[Entry]
 
-    object Entry
-    {
+    object Entry {
       def unapply(s: String): Option[Entry] =
         for { (a, b) <- Properties.Eq.unapply(s) }
         yield (a, Library.perhaps_unquote(b))
       def getenv(a: String): String =
         Properties.Eq(a, quote(Isabelle_System.getenv(a)))

 
   /** log file **/
 
   def print_date(date: Date): String = Log_File.Date_Format(date)
 
-  object Log_File
-  {
+  object Log_File {
     /* log file */
 
-    def plain_name(name: String): String =
-    {
+    def plain_name(name: String): String = {
       List(".log", ".log.gz", ".log.xz", ".gz", ".xz").find(name.endsWith) match {
         case Some(s) => Library.try_unsuffix(s, name).get
         case None => name
       }
     }

       new Log_File(plain_name(name), lines.map(Library.trim_line))
 
     def apply(name: String, text: String): Log_File =
       new Log_File(plain_name(name), Library.trim_split_lines(text))
 
-    def apply(file: JFile): Log_File =
-    {
+    def apply(file: JFile): Log_File = {
       val name = file.getName
       val text =
         if (name.endsWith(".gz")) File.read_gzip(file)
         else if (name.endsWith(".xz")) File.read_xz(file)
         else File.read(file)

 
     def is_log(file: JFile,
       prefixes: List[String] =
         List(Build_History.log_prefix, Identify.log_prefix, Identify.log_prefix2,
           Isatest.log_prefix, AFP_Test.log_prefix, Jenkins.log_prefix),
-      suffixes: List[String] = List(".log", ".log.gz", ".log.xz")): Boolean =
-    {
+      suffixes: List[String] = List(".log", ".log.gz", ".log.xz")
+    ): Boolean = {
       val name = file.getName
 
       prefixes.exists(name.startsWith) &&
       suffixes.exists(name.endsWith) &&
       name != "isatest.log" &&

     }
 
 
     /* date format */
 
-    val Date_Format =
-    {
+    val Date_Format = {
       val fmts =
         Date.Formatter.variants(
           List("EEE MMM d HH:mm:ss O yyyy", "EEE MMM d HH:mm:ss VV yyyy"),
           List(Locale.ENGLISH, Locale.GERMAN)) :::
         List(

 
       Date.Format.make(fmts, tune)
     }
   }
 
-  class Log_File private(val name: String, val lines: List[String])
-  {
+  class Log_File private(val name: String, val lines: List[String]) {
     log_file =>
 
     override def toString: String = name
 
     def text: String = cat_lines(lines)

       error("Error in log file " + quote(name) + ": " + msg)
 
 
     /* date format */
 
-    object Strict_Date
-    {
+    object Strict_Date {
       def unapply(s: String): Some[Date] =
         try { Some(Log_File.Date_Format.parse(s)) }
         catch { case exn: DateTimeParseException => log_file.err(exn.getMessage) }
     }
 

 
 
 
   /** digested meta info: produced by Admin/build_history in log.xz file **/
 
-  object Meta_Info
-  {
+  object Meta_Info {
     val empty: Meta_Info = Meta_Info(Nil, Nil)
   }
 
-  sealed case class Meta_Info(props: Properties.T, settings: Settings.T)
-  {
+  sealed case class Meta_Info(props: Properties.T, settings: Settings.T) {
     def is_empty: Boolean = props.isEmpty && settings.isEmpty
 
     def get(c: SQL.Column): Option[String] =
       Properties.get(props, c.name) orElse
       Properties.get(settings, c.name)
 
     def get_date(c: SQL.Column): Option[Date] =
       get(c).map(Log_File.Date_Format.parse)
   }
 
-  object Identify
-  {
+  object Identify {
     val log_prefix = "isabelle_identify_"
     val log_prefix2 = "plain_identify_"
 
     def engine(log_file: Log_File): String =
       if (log_file.name.startsWith(Jenkins.log_prefix)) "jenkins_identify"

     val No_End = new Regex("""$.""")
     val Isabelle_Version = List(new Regex("""^Isabelle version: (\S+)$"""))
     val AFP_Version = List(new Regex("""^AFP version: (\S+)$"""))
   }
 
-  object Isatest
-  {
+  object Isatest {
     val log_prefix = "isatest-makeall-"
     val engine = "isatest"
     val Start = new Regex("""^------------------- starting test --- (.+) --- (.+)$""")
     val End = new Regex("""^------------------- test (?:successful|FAILED) --- (.+) --- .*$""")
     val Isabelle_Version = List(new Regex("""^Isabelle version: (\S+)$"""))
   }
 
-  object AFP_Test
-  {
+  object AFP_Test {
     val log_prefix = "afp-test-devel-"
     val engine = "afp-test"
     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 = 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$""")
   }
 
-  object Jenkins
-  {
+  object Jenkins {
     val log_prefix = "jenkins_"
     val engine = "jenkins"
     val Host = new Regex("""^Building remotely on (\S+) \((\S+)\).*$""")
     val Start = new Regex("""^(?:Started by an SCM change|Started from command line by admin|).*$""")
     val Start_Date = new Regex("""^Build started at (.+)$""")

         new Regex("""^ISABELLE_CI_AFP_ID="(\w+)".*$"""))
     val CONFIGURATION = "=== CONFIGURATION ==="
     val BUILD = "=== BUILD ==="
   }
 
-  private def parse_meta_info(log_file: Log_File): Meta_Info =
-  {
+  private def parse_meta_info(log_file: Log_File): Meta_Info = {
     def parse(engine: String, host: String, start: Date,
-      End: Regex, Isabelle_Version: List[Regex], AFP_Version: List[Regex]): Meta_Info =
-    {
-      val build_id =
-      {
+      End: Regex, Isabelle_Version: List[Regex], AFP_Version: List[Regex]
+    ): Meta_Info = {
+      val build_id = {
         val prefix = proper_string(host) orElse proper_string(engine) getOrElse "build"
         prefix + ":" + start.time.ms
       }
       val build_engine = if (engine == "") Nil else List(Prop.build_engine.name -> engine)
       val build_host = if (host == "") Nil else List(Prop.build_host.name -> host)

 
   /** build info: toplevel output of isabelle build or Admin/build_history **/
 
   val SESSION_NAME = "session_name"
 
-  object Session_Status extends Enumeration
-  {
+  object Session_Status extends Enumeration {
     val existing, finished, failed, cancelled = Value
   }
 
   sealed case class Session_Entry(
     chapter: String = "",

     sources: Option[String] = None,
     heap_size: Option[Long] = None,
     status: Option[Session_Status.Value] = None,
     errors: List[String] = Nil,
     theory_timings: Map[String, Timing] = Map.empty,
-    ml_statistics: List[Properties.T] = Nil)
-  {
+    ml_statistics: List[Properties.T] = Nil
+  ) {
     def proper_groups: Option[String] = if (groups.isEmpty) None else Some(cat_lines(groups))
     def finished: Boolean = status == Some(Session_Status.finished)
     def failed: Boolean = status == Some(Session_Status.failed)
   }
 
-  object Build_Info
-  {
+  object Build_Info {
     val sessions_dummy: Map[String, Session_Entry] =
       Map("" -> Session_Entry(theory_timings = Map("" -> Timing.zero)))
   }
 
-  sealed case class Build_Info(sessions: Map[String, Session_Entry])
-  {
+  sealed case class Build_Info(sessions: Map[String, Session_Entry]) {
     def finished_sessions: List[String] = for ((a, b) <- sessions.toList if b.finished) yield a
     def failed_sessions: List[String] = for ((a, b) <- sessions.toList if b.failed) yield a
   }
 
-  private def parse_build_info(log_file: Log_File, parse_ml_statistics: Boolean): Build_Info =
-  {
-    object Chapter_Name
-    {
+  private def parse_build_info(log_file: Log_File, parse_ml_statistics: Boolean): Build_Info = {
+    object Chapter_Name {
       def unapply(s: String): Some[(String, String)] =
         space_explode('/', s) match {
           case List(chapter, name) => Some((chapter, name))
           case _ => Some(("", s))
         }

       new Regex("""^Timing (\S+) \((\d+) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
     val Session_Started = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""")
     val Sources = new Regex("""^Sources (\S+) (\S{""" + SHA1.digest_length + """})$""")
     val Heap = new Regex("""^Heap (\S+) \((\d+) bytes\)$""")
 
-    object Theory_Timing
-    {
+    object Theory_Timing {
       def unapply(line: String): Option[(String, (String, Timing))] =
         Protocol.Theory_Timing_Marker.unapply(line.replace('~', '-')).map(log_file.parse_props)
         match {
           case Some((SESSION_NAME, session) :: props) =>
             for (theory <- Markup.Name.unapply(props))

     session_timing: Properties.T,
     command_timings: List[Properties.T],
     theory_timings: List[Properties.T],
     ml_statistics: List[Properties.T],
     task_statistics: List[Properties.T],
-    errors: List[String])
-  {
+    errors: List[String]
+  ) {
     def error(s: String): Session_Info =
       copy(errors = errors ::: List(s))
   }
 
   private def parse_session_info(
     log_file: Log_File,
     command_timings: Boolean,
     theory_timings: Boolean,
     ml_statistics: Boolean,
-    task_statistics: Boolean): Session_Info =
-  {
+    task_statistics: Boolean
+  ): Session_Info = {
     Session_Info(
       session_timing = log_file.find_props(Protocol.Session_Timing_Marker) getOrElse Nil,
       command_timings =
         if (command_timings) log_file.filter_props(Protocol.Command_Timing_Marker) else Nil,
       theory_timings =

 
   /** persistent store **/
 
   /* SQL data model */
 
-  object Data
-  {
+  object Data {
     def build_log_table(name: String, columns: List[SQL.Column], body: String = ""): SQL.Table =
       SQL.Table("isabelle_build_log_" + name, columns, body)
 
 
     /* main content */

       build_log_table("ml_statistics", List(log_name, session_name, ml_statistics))
 
 
     /* AFP versions */
 
-    val isabelle_afp_versions_table: SQL.Table =
-    {
+    val isabelle_afp_versions_table: SQL.Table = {
       val version1 = Prop.isabelle_version
       val version2 = Prop.afp_version
       build_log_table("isabelle_afp_versions", List(version1.make_primary_key, version2),
         SQL.select(List(version1, version2), distinct = true) + meta_info_table +
         " WHERE " + version1.defined + " AND " + version2.defined)

 
     def pull_date(afp: Boolean = false): SQL.Column =
       if (afp) SQL.Column.date("afp_pull_date")
       else SQL.Column.date("pull_date")
 
-    def pull_date_table(afp: Boolean = false): SQL.Table =
-    {
+    def pull_date_table(afp: Boolean = false): SQL.Table = {
       val (name, versions) =
         if (afp) ("afp_pull_date", List(Prop.isabelle_version, Prop.afp_version))
         else ("pull_date", List(Prop.isabelle_version))
 
       build_log_table(name, versions.map(_.make_primary_key) ::: List(pull_date(afp)),

 
     def recent_time(days: Int): SQL.Source =
       "now() - INTERVAL '" + days.max(0) + " days'"
 
     def recent_pull_date_table(
-      days: Int, rev: String = "", afp_rev: Option[String] = None): SQL.Table =
-    {
+      days: Int,
+      rev: String = "",
+      afp_rev: Option[String] = None
+    ): SQL.Table = {
       val afp = afp_rev.isDefined
       val rev2 = afp_rev.getOrElse("")
       val table = pull_date_table(afp)
 
       val version1 = Prop.isabelle_version

            else if (rev == "" && rev2 != "") " OR " + eq2
            else if (rev != "" && rev2 != "") " OR (" + eq1 + " AND " + eq2 + ")"
            else "")))
     }
 
-    def select_recent_log_names(days: Int): SQL.Source =
-    {
+    def select_recent_log_names(days: Int): SQL.Source = {
       val table1 = meta_info_table
       val table2 = recent_pull_date_table(days)
       table1.select(List(log_name), distinct = true) + SQL.join_inner + table2.query_named +
         " ON " + Prop.isabelle_version(table1) + " = " + Prop.isabelle_version(table2)
     }
 
-    def select_recent_versions(days: Int,
-      rev: String = "", afp_rev: Option[String] = None, sql: SQL.Source = ""): SQL.Source =
-    {
+    def select_recent_versions(
+      days: Int,
+      rev: String = "",
+      afp_rev: Option[String] = None,
+      sql: SQL.Source = ""
+    ): SQL.Source = {
       val afp = afp_rev.isDefined
       val version = Prop.isabelle_version
       val table1 = recent_pull_date_table(days, rev = rev, afp_rev = afp_rev)
       val table2 = meta_info_table
       val aux_table = SQL.Table("aux", table2.columns, table2.select(sql = sql))

     }
 
 
     /* universal view on main data */
 
-    val universal_table: SQL.Table =
-    {
+    val universal_table: SQL.Table = {
       val afp_pull_date = pull_date(afp = true)
       val version1 = Prop.isabelle_version
       val version2 = Prop.afp_version
       val table1 = meta_info_table
       val table2 = pull_date_table(afp = true)

   /* database access */
 
   def store(options: Options, cache: XML.Cache = XML.Cache.make()): Store =
     new Store(options, cache)
 
-  class Store private[Build_Log](options: Options, val cache: XML.Cache)
-  {
+  class Store private[Build_Log](options: Options, val cache: XML.Cache) {
     def open_database(
       user: String = options.string("build_log_database_user"),
       password: String = options.string("build_log_database_password"),
       database: String = options.string("build_log_database_name"),
       host: String = options.string("build_log_database_host"),
       port: Int = options.int("build_log_database_port"),
       ssh_host: String = options.string("build_log_ssh_host"),
       ssh_user: String = options.string("build_log_ssh_user"),
-      ssh_port: Int = options.int("build_log_ssh_port")): PostgreSQL.Database =
-    {
+      ssh_port: Int = options.int("build_log_ssh_port")
+    ): PostgreSQL.Database = {
       PostgreSQL.open_database(
         user = user, password = password, database = database, host = host, port = port,
         ssh =
           if (ssh_host == "") None
           else Some(SSH.open_session(options, host = ssh_host, user = ssh_user, port = ssh_port)),
         ssh_close = true)
     }
 
     def update_database(
-      db: PostgreSQL.Database, dirs: List[Path], ml_statistics: Boolean = false): Unit =
-    {
+      db: PostgreSQL.Database, dirs: List[Path], ml_statistics: Boolean = false): Unit = {
       val log_files =
         dirs.flatMap(dir =>
           File.find_files(dir.file, pred = Log_File.is_log(_), follow_links = true))
       write_info(db, log_files, ml_statistics = ml_statistics)
 
       db.create_view(Data.pull_date_table())
       db.create_view(Data.pull_date_table(afp = true))
       db.create_view(Data.universal_table)
     }
 
-    def snapshot_database(db: PostgreSQL.Database, sqlite_database: Path,
-      days: Int = 100, ml_statistics: Boolean = false): Unit =
-    {
+    def snapshot_database(
+      db: PostgreSQL.Database,
+      sqlite_database: Path,
+      days: Int = 100,
+      ml_statistics: Boolean = false
+    ): Unit = {
       Isabelle_System.make_directory(sqlite_database.dir)
       sqlite_database.file.delete
 
-      using(SQLite.open_database(sqlite_database))(db2 =>
-      {
+      using(SQLite.open_database(sqlite_database))(db2 => {
         db.transaction {
           db2.transaction {
             // main content
             db2.create_table(Data.meta_info_table)
             db2.create_table(Data.sessions_table)

                   read_build_info(db, log_name, ml_statistics = true))
               }
             }
 
             // pull_date
-            for (afp <- List(false, true))
-            {
+            for (afp <- List(false, true)) {
               val afp_rev = if (afp) Some("") else None
               val table = Data.pull_date_table(afp)
               db2.create_table(table)
-              db2.using_statement(table.insert())(stmt2 =>
-              {
+              db2.using_statement(table.insert())(stmt2 => {
                 db.using_statement(
-                  Data.recent_pull_date_table(days, afp_rev = afp_rev).query)(stmt =>
-                {
+                  Data.recent_pull_date_table(days, afp_rev = afp_rev).query)(stmt => {
                   val res = stmt.execute_query()
                   while (res.next()) {
                     for ((c, i) <- table.columns.zipWithIndex) {
                       stmt2.string(i + 1) = res.get_string(c)
                     }

 
     def domain(db: SQL.Database, table: SQL.Table, column: SQL.Column): Set[String] =
       db.using_statement(table.select(List(column), distinct = true))(stmt =>
         stmt.execute_query().iterator(_.string(column)).toSet)
 
-    def update_meta_info(db: SQL.Database, log_name: String, meta_info: Meta_Info): Unit =
-    {
+    def update_meta_info(db: SQL.Database, log_name: String, meta_info: Meta_Info): Unit = {
       val table = Data.meta_info_table
-      db.using_statement(db.insert_permissive(table))(stmt =>
-      {
+      db.using_statement(db.insert_permissive(table))(stmt => {
         stmt.string(1) = log_name
         for ((c, i) <- table.columns.tail.zipWithIndex) {
           if (c.T == SQL.Type.Date)
             stmt.date(i + 2) = meta_info.get_date(c)
           else

         }
         stmt.execute()
       })
     }
 
-    def update_sessions(db: SQL.Database, log_name: String, build_info: Build_Info): Unit =
-    {
+    def update_sessions(db: SQL.Database, log_name: String, build_info: Build_Info): Unit = {
       val table = Data.sessions_table
-      db.using_statement(db.insert_permissive(table))(stmt =>
-      {
+      db.using_statement(db.insert_permissive(table))(stmt => {
         val sessions =
           if (build_info.sessions.isEmpty) Build_Info.sessions_dummy
           else build_info.sessions
         for ((session_name, session) <- sessions) {
           stmt.string(1) = log_name

           stmt.execute()
         }
       })
     }
 
-    def update_theories(db: SQL.Database, log_name: String, build_info: Build_Info): Unit =
-    {
+    def update_theories(db: SQL.Database, log_name: String, build_info: Build_Info): Unit = {
       val table = Data.theories_table
-      db.using_statement(db.insert_permissive(table))(stmt =>
-      {
+      db.using_statement(db.insert_permissive(table))(stmt => {
         val sessions =
           if (build_info.sessions.forall({ case (_, session) => session.theory_timings.isEmpty }))
             Build_Info.sessions_dummy
           else build_info.sessions
         for {

           stmt.execute()
         }
       })
     }
 
-    def update_ml_statistics(db: SQL.Database, log_name: String, build_info: Build_Info): Unit =
-    {
+    def update_ml_statistics(db: SQL.Database, log_name: String, build_info: Build_Info): Unit = {
       val table = Data.ml_statistics_table
-      db.using_statement(db.insert_permissive(table))(stmt =>
-      {
+      db.using_statement(db.insert_permissive(table))(stmt => {
         val ml_stats: List[(String, Option[Bytes])] =
           Par_List.map[(String, Session_Entry), (String, Option[Bytes])](
             { case (a, b) => (a, Properties.compress(b.ml_statistics, cache = cache.xz).proper) },
             build_info.sessions.iterator.filter(p => p._2.ml_statistics.nonEmpty).toList)
         val entries = if (ml_stats.nonEmpty) ml_stats else List("" -> None)

           stmt.execute()
         }
       })
     }
 
-    def write_info(db: SQL.Database, files: List[JFile], ml_statistics: Boolean = false): Unit =
-    {
-      abstract class Table_Status(table: SQL.Table)
-      {
+    def write_info(db: SQL.Database, files: List[JFile], ml_statistics: Boolean = false): Unit = {
+      abstract class Table_Status(table: SQL.Table) {
         db.create_table(table)
         private var known: Set[String] = domain(db, table, Data.log_name)
 
         def required(file: JFile): Boolean = !known(Log_File.plain_name(file.getName))
 
         def update_db(db: SQL.Database, log_file: Log_File): Unit
-        def update(log_file: Log_File): Unit =
-        {
+        def update(log_file: Log_File): Unit = {
           if (!known(log_file.name)) {
             update_db(db, log_file)
             known += log_file.name
           }
         }

             }
           })
 
       for (file_group <-
             files.filter(file => status.exists(_.required(file))).
-              grouped(options.int("build_log_transaction_size") max 1))
-      {
+              grouped(options.int("build_log_transaction_size") max 1)) {
         val log_files = Par_List.map[JFile, Log_File](Log_File.apply, file_group)
         db.transaction { log_files.foreach(log_file => status.foreach(_.update(log_file))) }
       }
     }
 
-    def read_meta_info(db: SQL.Database, log_name: String): Option[Meta_Info] =
-    {
+    def read_meta_info(db: SQL.Database, log_name: String): Option[Meta_Info] = {
       val table = Data.meta_info_table
       val columns = table.columns.tail
-      db.using_statement(table.select(columns, Data.log_name.where_equal(log_name)))(stmt =>
-      {
+      db.using_statement(table.select(columns, Data.log_name.where_equal(log_name)))(stmt => {
         val res = stmt.execute_query()
         if (!res.next()) None
         else {
           val results =
             columns.map(c => c.name ->

 
     def read_build_info(
       db: SQL.Database,
       log_name: String,
       session_names: List[String] = Nil,
-      ml_statistics: Boolean = false): Build_Info =
-    {
+      ml_statistics: Boolean = false): Build_Info = {
       val table1 = Data.sessions_table
       val table2 = Data.ml_statistics_table
 
       val where_log_name =
         Data.log_name(table1).where_equal(log_name) + " AND " +

           (columns, SQL.enclose(join))
         }
         else (columns1, table1.ident)
 
       val sessions =
-        db.using_statement(SQL.select(columns) + from + " " + where)(stmt =>
-        {
-          stmt.execute_query().iterator(res =>
-          {
+        db.using_statement(SQL.select(columns) + from + " " + where)(stmt => {
+          stmt.execute_query().iterator(res => {
             val session_name = res.string(Data.session_name)
             val session_entry =
               Session_Entry(
                 chapter = res.string(Data.chapter),
                 groups = split_lines(res.string(Data.groups)),