SQL database operations for combined session info;
authorwenzelm
Thu Mar 16 23:33:39 2017 +0100 (2017-03-16)
changeset 65281c70e7d24a16d
parent 65280 ef37f5236794
child 65282 f4c5f10829a0
SQL database operations for combined session info;
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Thu Mar 16 23:27:29 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Thu Mar 16 23:33:39 2017 +0100
     1.3 @@ -521,6 +521,7 @@
     1.4    {
     1.5      /* file names */
     1.6  
     1.7 +    def database(name: String): Path = Path.basic("log") + Path.basic(name).ext("db")
     1.8      def log(name: String): Path = Path.basic("log") + Path.basic(name)
     1.9      def log_gz(name: String): Path = log(name).ext("gz")
    1.10  
    1.11 @@ -551,6 +552,9 @@
    1.12        input_dirs.find(dir => (dir + log_gz(name)).is_file).map(dir =>
    1.13          (dir + log_gz(name), read_heap_digest(dir + Path.basic(name))))
    1.14  
    1.15 +    def find_database(name: String): Option[Path] =
    1.16 +      input_dirs.map(_ + database(name)).find(_.is_file)
    1.17 +
    1.18      def find_log(name: String): Option[Path] =
    1.19        input_dirs.map(_ + log(name)).find(_.is_file)
    1.20  
    1.21 @@ -565,4 +569,91 @@
    1.22          error("Unknown logic " + quote(name) + " -- no heap file found in:\n" +
    1.23            cat_lines(input_dirs.map(dir => "  " + dir.expand.implode)))
    1.24    }
    1.25 +
    1.26 +
    1.27 +  /* SQL database operations */
    1.28 +
    1.29 +  def encode_properties(ps: Properties.T): Bytes =
    1.30 +    Bytes(YXML.string_of_body(XML.Encode.properties(ps)))
    1.31 +
    1.32 +  def decode_properties(bs: Bytes): Properties.T =
    1.33 +    XML.Decode.properties(YXML.parse_body(bs.text))
    1.34 +
    1.35 +  def compress_properties(ps: List[Properties.T], options: XZ.Options = XZ.options()): Bytes =
    1.36 +  {
    1.37 +    if (ps.isEmpty) Bytes.empty
    1.38 +    else Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.properties)(ps))).compress(options)
    1.39 +  }
    1.40 +
    1.41 +  def uncompress_properties(bs: Bytes): List[Properties.T] =
    1.42 +  {
    1.43 +    if (bs.isEmpty) Nil
    1.44 +    else XML.Decode.list(XML.Decode.properties)(YXML.parse_body(bs.uncompress().text))
    1.45 +  }
    1.46 +
    1.47 +  object Session_Info
    1.48 +  {
    1.49 +    // Build_Log.Session_Info
    1.50 +    val session_name = SQL.Column.string("session_name")
    1.51 +    val session_timing = SQL.Column.bytes("session_timing")
    1.52 +    val command_timings = SQL.Column.bytes("command_timings")
    1.53 +    val ml_statistics = SQL.Column.bytes("ml_statistics")
    1.54 +    val task_statistics = SQL.Column.bytes("task_statistics")
    1.55 +
    1.56 +    // Build.Session_Info
    1.57 +    val sources = SQL.Column.string("sources")
    1.58 +    val input_heap = SQL.Column.string("input_heap")
    1.59 +    val output_heap = SQL.Column.string("output_heap")
    1.60 +    val return_code = SQL.Column.int("return_code")
    1.61 +
    1.62 +    val table = SQL.Table("isabelle_session_info",
    1.63 +      List(session_name, session_timing, command_timings, ml_statistics, task_statistics,
    1.64 +        sources, input_heap, output_heap, return_code))
    1.65 +
    1.66 +    def write_data(db: SQLite.Database, info1: Build_Log.Session_Info, info2: Build.Session_Info)
    1.67 +    {
    1.68 +      db.transaction {
    1.69 +        db.drop_table(table)
    1.70 +        db.create_table(table)
    1.71 +        using(db.insert_statement(table))(stmt =>
    1.72 +        {
    1.73 +          db.set_string(stmt, 1, info1.session_name)
    1.74 +          db.set_bytes(stmt, 2, encode_properties(info1.session_timing))
    1.75 +          db.set_bytes(stmt, 3, compress_properties(info1.command_timings))
    1.76 +          db.set_bytes(stmt, 4, compress_properties(info1.ml_statistics))
    1.77 +          db.set_bytes(stmt, 5, compress_properties(info1.task_statistics))
    1.78 +          db.set_string(stmt, 6, info2.sources)
    1.79 +          db.set_string(stmt, 7, info2.input_heap)
    1.80 +          db.set_string(stmt, 8, info2.output_heap)
    1.81 +          db.set_int(stmt, 9, info2.return_code)
    1.82 +          stmt.execute()
    1.83 +        })
    1.84 +      }
    1.85 +    }
    1.86 +
    1.87 +    def read_data(db: SQLite.Database): Option[(Build_Log.Session_Info, Build.Session_Info)] =
    1.88 +    {
    1.89 +      using(db.select_statement(table, table.columns))(stmt =>
    1.90 +      {
    1.91 +        val rs = stmt.executeQuery
    1.92 +        if (!rs.next) None
    1.93 +        else {
    1.94 +          val info1 =
    1.95 +            Build_Log.Session_Info(
    1.96 +              db.string(rs, session_name.name),
    1.97 +              decode_properties(db.bytes(rs, session_timing.name)),
    1.98 +              uncompress_properties(db.bytes(rs, command_timings.name)),
    1.99 +              uncompress_properties(db.bytes(rs, ml_statistics.name)),
   1.100 +              uncompress_properties(db.bytes(rs, task_statistics.name)))
   1.101 +          val info2 =
   1.102 +            Build.Session_Info(
   1.103 +              db.string(rs, sources.name),
   1.104 +              db.string(rs, input_heap.name),
   1.105 +              db.string(rs, output_heap.name),
   1.106 +              db.int(rs, return_code.name))
   1.107 +          Some((info1, info2))
   1.108 +        }
   1.109 +      })
   1.110 +    }
   1.111 +  }
   1.112  }
     2.1 --- a/src/Pure/Tools/build.scala	Thu Mar 16 23:27:29 2017 +0100
     2.2 +++ b/src/Pure/Tools/build.scala	Thu Mar 16 23:33:39 2017 +0100
     2.3 @@ -203,6 +203,9 @@
     2.4  
     2.5    /* sources and heaps */
     2.6  
     2.7 +  sealed case class Session_Info(
     2.8 +    sources: String, input_heap: String, output_heap: String, return_code: Int)
     2.9 +
    2.10    private val SOURCES = "sources: "
    2.11    private val INPUT_HEAP = "input_heap: "
    2.12    private val OUTPUT_HEAP = "output_heap: "