store theory timings in session in build_log database;
authorwenzelm
Mon Oct 16 19:59:18 2017 +0200 (20 months ago)
changeset 668740b8da0fc9563
parent 66873 9953ae603a23
child 66875 f60d3e6d5975
store theory timings in session in build_log database;
tuned;
src/Pure/Admin/build_history.scala
src/Pure/Admin/build_log.scala
     1.1 --- a/src/Pure/Admin/build_history.scala	Mon Oct 16 14:32:09 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_history.scala	Mon Oct 16 19:59:18 2017 +0200
     1.3 @@ -253,6 +253,19 @@
     1.4            Build_Log.Prop.isabelle_version.name -> isabelle_version) :::
     1.5          afp_version.map(Build_Log.Prop.afp_version.name -> _).toList
     1.6  
     1.7 +      build_out_progress.echo("Reading theory timings ...")
     1.8 +      val theory_timings =
     1.9 +        build_info.finished_sessions.flatMap(session_name =>
    1.10 +          {
    1.11 +            val database = isabelle_output + store.database(session_name)
    1.12 +
    1.13 +            val properties =
    1.14 +              using(SQLite.open_database(database))(db =>
    1.15 +                store.read_theory_timings(db, session_name))
    1.16 +
    1.17 +            properties.map(ps => (Build_Log.SESSION_NAME -> session_name) :: ps)
    1.18 +          })
    1.19 +
    1.20        build_out_progress.echo("Reading ML statistics ...")
    1.21        val ml_statistics =
    1.22          build_info.finished_sessions.flatMap(session_name =>
    1.23 @@ -311,6 +324,7 @@
    1.24        File.write_xz(log_path.ext("xz"),
    1.25          terminate_lines(
    1.26            Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: build_result.out_lines :::
    1.27 +          theory_timings.map(Build_Log.Log_File.print_props(Build_Log.THEORY_TIMING_MARKER, _)) :::
    1.28            ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _)) :::
    1.29            session_errors.map(Build_Log.Log_File.print_props(Build_Log.ERROR_MESSAGE_MARKER, _)) :::
    1.30            heap_sizes), XZ.options(6))
     2.1 --- a/src/Pure/Admin/build_log.scala	Mon Oct 16 14:32:09 2017 +0200
     2.2 +++ b/src/Pure/Admin/build_log.scala	Mon Oct 16 19:59:18 2017 +0200
     2.3 @@ -458,11 +458,6 @@
     2.4      val existing, finished, failed, cancelled = Value
     2.5    }
     2.6  
     2.7 -  object Session_Entry
     2.8 -  {
     2.9 -    val empty: Session_Entry = Session_Entry()
    2.10 -  }
    2.11 -
    2.12    sealed case class Session_Entry(
    2.13      chapter: String = "",
    2.14      groups: List[String] = Nil,
    2.15 @@ -472,6 +467,7 @@
    2.16      heap_size: Option[Long] = None,
    2.17      status: Option[Session_Status.Value] = None,
    2.18      errors: List[String] = Nil,
    2.19 +    theory_timings: Map[String, Timing] = Map.empty,
    2.20      ml_statistics: List[Properties.T] = Nil)
    2.21    {
    2.22      def proper_groups: Option[String] = if (groups.isEmpty) None else Some(cat_lines(groups))
    2.23 @@ -479,6 +475,12 @@
    2.24      def failed: Boolean = status == Some(Session_Status.failed)
    2.25    }
    2.26  
    2.27 +  object Build_Info
    2.28 +  {
    2.29 +    val sessions_dummy: Map[String, Session_Entry] =
    2.30 +      Map("" -> Session_Entry(theory_timings = Map("" -> Timing.zero)))
    2.31 +  }
    2.32 +
    2.33    sealed case class Build_Info(sessions: Map[String, Session_Entry])
    2.34    {
    2.35      def finished_sessions: List[String] = for ((a, b) <- sessions.toList if b.finished) yield a
    2.36 @@ -509,6 +511,19 @@
    2.37      val Session_Cancelled = new Regex("""^(\S+) CANCELLED""")
    2.38      val Heap = new Regex("""^Heap (\S+) \((\d+) bytes\)$""")
    2.39  
    2.40 +    object Theory_Timing
    2.41 +    {
    2.42 +      def unapply(line: String): Option[(String, (String, Timing))] =
    2.43 +        Library.try_unprefix(THEORY_TIMING_MARKER, line).map(log_file.parse_props(_)) match {
    2.44 +          case Some((SESSION_NAME, name) :: props) =>
    2.45 +            (props, props) match {
    2.46 +              case (Markup.Name(thy), Markup.Timing_Properties(t)) => Some((name, thy -> t))
    2.47 +              case _ => None
    2.48 +            }
    2.49 +          case _ => None
    2.50 +        }
    2.51 +    }
    2.52 +
    2.53      var chapter = Map.empty[String, String]
    2.54      var groups = Map.empty[String, List[String]]
    2.55      var threads = Map.empty[String, Int]
    2.56 @@ -518,12 +533,14 @@
    2.57      var failed = Set.empty[String]
    2.58      var cancelled = Set.empty[String]
    2.59      var heap_sizes = Map.empty[String, Long]
    2.60 +    var theory_timings = Map.empty[String, Map[String, Timing]]
    2.61      var ml_statistics = Map.empty[String, List[Properties.T]]
    2.62      var errors = Map.empty[String, List[String]]
    2.63  
    2.64      def all_sessions: Set[String] =
    2.65        chapter.keySet ++ groups.keySet ++ threads.keySet ++ timing.keySet ++ ml_timing.keySet ++
    2.66 -      failed ++ cancelled ++ started ++ heap_sizes.keySet ++ ml_statistics.keySet
    2.67 +      failed ++ cancelled ++ started ++ heap_sizes.keySet ++ theory_timings.keySet ++
    2.68 +      ml_statistics.keySet
    2.69  
    2.70  
    2.71      for (line <- log_file.lines) {
    2.72 @@ -562,21 +579,26 @@
    2.73          case Heap(name, Value.Long(size)) =>
    2.74            heap_sizes += (name -> size)
    2.75  
    2.76 +        case _ if line.startsWith(THEORY_TIMING_MARKER) && YXML.detect(line) =>
    2.77 +          line match {
    2.78 +            case Theory_Timing(name, theory_timing) =>
    2.79 +              theory_timings += (name -> (theory_timings.getOrElse(name, Map.empty) + theory_timing))
    2.80 +            case _ => log_file.err("malformed theory_timing " + quote(line))
    2.81 +          }
    2.82 +
    2.83          case _ if parse_ml_statistics && line.startsWith(ML_STATISTICS_MARKER) && YXML.detect(line) =>
    2.84 -          val (name, props) =
    2.85 -            Library.try_unprefix(ML_STATISTICS_MARKER, line).map(log_file.parse_props(_)) match {
    2.86 -              case Some((SESSION_NAME, name) :: props) => (name, props)
    2.87 -              case _ => log_file.err("malformed ML_statistics " + quote(line))
    2.88 -            }
    2.89 -          ml_statistics += (name -> (props :: ml_statistics.getOrElse(name, Nil)))
    2.90 +          Library.try_unprefix(ML_STATISTICS_MARKER, line).map(log_file.parse_props(_)) match {
    2.91 +            case Some((SESSION_NAME, name) :: props) =>
    2.92 +              ml_statistics += (name -> (props :: ml_statistics.getOrElse(name, Nil)))
    2.93 +            case _ => log_file.err("malformed ML_statistics " + quote(line))
    2.94 +          }
    2.95  
    2.96          case _ if line.startsWith(ERROR_MESSAGE_MARKER) && YXML.detect(line) =>
    2.97 -          val (name, msg) =
    2.98 -            Library.try_unprefix(ERROR_MESSAGE_MARKER, line).map(log_file.parse_props(_)) match {
    2.99 -              case Some(List((SESSION_NAME, name), (Markup.CONTENT, msg))) => (name, msg)
   2.100 -              case _ => log_file.err("malformed error message " + quote(line))
   2.101 -            }
   2.102 -          errors += (name -> (Library.decode_lines(msg) :: errors.getOrElse(name, Nil)))
   2.103 +          Library.try_unprefix(ERROR_MESSAGE_MARKER, line).map(log_file.parse_props(_)) match {
   2.104 +            case Some(List((SESSION_NAME, name), (Markup.CONTENT, msg))) =>
   2.105 +              errors += (name -> (Library.decode_lines(msg) :: errors.getOrElse(name, Nil)))
   2.106 +            case _ => log_file.err("malformed error message " + quote(line))
   2.107 +          }
   2.108  
   2.109          case _ =>
   2.110        }
   2.111 @@ -602,6 +624,7 @@
   2.112                heap_size = heap_sizes.get(name),
   2.113                status = Some(status),
   2.114                errors = errors.getOrElse(name, Nil).reverse,
   2.115 +              theory_timings = theory_timings.getOrElse(name, Map.empty),
   2.116                ml_statistics = ml_statistics.getOrElse(name, Nil).reverse)
   2.117            (name -> entry)
   2.118          }):_*)
   2.119 @@ -660,6 +683,7 @@
   2.120  
   2.121      val log_name = SQL.Column.string("log_name").make_primary_key
   2.122      val session_name = SQL.Column.string("session_name").make_primary_key
   2.123 +    val theory_name = SQL.Column.string("theory_name").make_primary_key
   2.124      val chapter = SQL.Column.string("chapter")
   2.125      val groups = SQL.Column.string("groups")
   2.126      val threads = SQL.Column.int("threads")
   2.127 @@ -671,6 +695,9 @@
   2.128      val ml_timing_cpu = SQL.Column.long("ml_timing_cpu")
   2.129      val ml_timing_gc = SQL.Column.long("ml_timing_gc")
   2.130      val ml_timing_factor = SQL.Column.double("ml_timing_factor")
   2.131 +    val theory_timing_elapsed = SQL.Column.long("theory_timing_elapsed")
   2.132 +    val theory_timing_cpu = SQL.Column.long("theory_timing_cpu")
   2.133 +    val theory_timing_gc = SQL.Column.long("theory_timing_gc")
   2.134      val heap_size = SQL.Column.long("heap_size")
   2.135      val status = SQL.Column.string("status")
   2.136      val errors = SQL.Column.bytes("errors")
   2.137 @@ -686,6 +713,11 @@
   2.138            timing_gc, timing_factor, ml_timing_elapsed, ml_timing_cpu, ml_timing_gc, ml_timing_factor,
   2.139            heap_size, status, errors))
   2.140  
   2.141 +    val theories_table =
   2.142 +      build_log_table("theories",
   2.143 +        List(log_name, session_name, theory_name, theory_timing_elapsed, theory_timing_cpu,
   2.144 +          theory_timing_gc))
   2.145 +
   2.146      val ml_statistics_table =
   2.147        build_log_table("ml_statistics", List(log_name, session_name, ml_statistics))
   2.148  
   2.149 @@ -853,6 +885,7 @@
   2.150              // main content
   2.151              db2.create_table(Data.meta_info_table)
   2.152              db2.create_table(Data.sessions_table)
   2.153 +            db2.create_table(Data.theories_table)
   2.154              db2.create_table(Data.ml_statistics_table)
   2.155  
   2.156              val recent_log_names =
   2.157 @@ -923,10 +956,10 @@
   2.158        val table = Data.sessions_table
   2.159        db.using_statement(db.insert_permissive(table))(stmt =>
   2.160        {
   2.161 -        val entries_iterator =
   2.162 -          if (build_info.sessions.isEmpty) Iterator("" -> Session_Entry.empty)
   2.163 -          else build_info.sessions.iterator
   2.164 -        for ((session_name, session) <- entries_iterator) {
   2.165 +        val sessions =
   2.166 +          if (build_info.sessions.isEmpty) Build_Info.sessions_dummy
   2.167 +          else build_info.sessions
   2.168 +        for ((session_name, session) <- sessions) {
   2.169            stmt.string(1) = log_name
   2.170            stmt.string(2) = session_name
   2.171            stmt.string(3) = proper_string(session.chapter)
   2.172 @@ -948,6 +981,30 @@
   2.173        })
   2.174      }
   2.175  
   2.176 +    def update_theories(db: SQL.Database, log_name: String, build_info: Build_Info)
   2.177 +    {
   2.178 +      val table = Data.theories_table
   2.179 +      db.using_statement(db.insert_permissive(table))(stmt =>
   2.180 +      {
   2.181 +        val sessions =
   2.182 +          if (build_info.sessions.forall({ case (_, session) => session.theory_timings.isEmpty }))
   2.183 +            Build_Info.sessions_dummy
   2.184 +          else build_info.sessions
   2.185 +        for {
   2.186 +          (session_name, session) <- sessions
   2.187 +          (theory_name, timing) <- session.theory_timings
   2.188 +        } {
   2.189 +          stmt.string(1) = log_name
   2.190 +          stmt.string(2) = session_name
   2.191 +          stmt.string(3) = theory_name
   2.192 +          stmt.long(4) = timing.elapsed.ms
   2.193 +          stmt.long(5) = timing.cpu.ms
   2.194 +          stmt.long(6) = timing.gc.ms
   2.195 +          stmt.execute()
   2.196 +        }
   2.197 +      })
   2.198 +    }
   2.199 +
   2.200      def update_ml_statistics(db: SQL.Database, log_name: String, build_info: Build_Info)
   2.201      {
   2.202        val table = Data.ml_statistics_table
   2.203 @@ -995,6 +1052,10 @@
   2.204              override def update_db(db: SQL.Database, log_file: Log_File): Unit =
   2.205                update_sessions(db, log_file.name, log_file.parse_build_info())
   2.206            },
   2.207 +          new Table_Status(Data.theories_table) {
   2.208 +            override def update_db(db: SQL.Database, log_file: Log_File): Unit =
   2.209 +              update_theories(db, log_file.name, log_file.parse_build_info())
   2.210 +          },
   2.211            new Table_Status(Data.ml_statistics_table) {
   2.212              override def update_db(db: SQL.Database, log_file: Log_File): Unit =
   2.213              if (ml_statistics) {