store exports in session database, with asynchronous / parallel compression;
authorwenzelm
Sun May 06 23:03:08 2018 +0200 (12 months ago)
changeset 68092888d35a19866
parent 68091 0c7820590236
child 68093 b98c5877b0f3
store exports in session database, with asynchronous / parallel compression;
src/Pure/Thy/export.scala
src/Pure/Tools/build.scala
src/Pure/build-jars
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Thy/export.scala	Sun May 06 23:03:08 2018 +0200
     1.3 @@ -0,0 +1,119 @@
     1.4 +/*  Title:      Pure/Thy/export.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Manage theory exports.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +object Export
    1.13 +{
    1.14 +  /* SQL data model */
    1.15 +
    1.16 +  object Data
    1.17 +  {
    1.18 +    val session_name = SQL.Column.string("session_name").make_primary_key
    1.19 +    val theory_name = SQL.Column.string("theory_name").make_primary_key
    1.20 +    val name = SQL.Column.string("name").make_primary_key
    1.21 +    val compressed = SQL.Column.bool("compressed")
    1.22 +    val body = SQL.Column.bytes("body")
    1.23 +
    1.24 +    val table =
    1.25 +      SQL.Table("isabelle_exports", List(session_name, theory_name, name, compressed, body))
    1.26 +
    1.27 +    def where_equal(session_name: String, theory_name: String): SQL.Source =
    1.28 +      "WHERE " + Data.session_name.equal(session_name) +
    1.29 +      " AND " + Data.theory_name.equal(theory_name)
    1.30 +  }
    1.31 +
    1.32 +  def read_names(db: SQL.Database, session_name: String, theory_name: String): List[String] =
    1.33 +  {
    1.34 +    val select = Data.table.select(List(Data.name), Data.where_equal(session_name, theory_name))
    1.35 +    db.using_statement(select)(stmt =>
    1.36 +      stmt.execute_query().iterator(res => res.string(Data.name)).toList)
    1.37 +  }
    1.38 +
    1.39 +  sealed case class Entry(
    1.40 +    session_name: String, theory_name: String, name: String, compressed: Boolean, body: Bytes)
    1.41 +  {
    1.42 +    override def toString: String = theory_name + ":" + name
    1.43 +
    1.44 +    def message(msg: String): String =
    1.45 +      msg + " " + quote(name) + " for theory " + quote(theory_name)
    1.46 +
    1.47 +    lazy val compressed_body: Bytes = if (compressed) body else body.compress()
    1.48 +    lazy val uncompressed_body: Bytes = if (compressed) body.uncompress() else body
    1.49 +
    1.50 +    def write(db: SQL.Database)
    1.51 +    {
    1.52 +      db.using_statement(Data.table.insert())(stmt =>
    1.53 +      {
    1.54 +        stmt.string(1) = session_name
    1.55 +        stmt.string(2) = theory_name
    1.56 +        stmt.string(3) = name
    1.57 +        stmt.bool(4) = compressed
    1.58 +        stmt.bytes(5) = body
    1.59 +        stmt.execute()
    1.60 +      })
    1.61 +    }
    1.62 +  }
    1.63 +
    1.64 +  def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String): Entry =
    1.65 +  {
    1.66 +    val select =
    1.67 +      Data.table.select(List(Data.compressed, Data.body),
    1.68 +        Data.where_equal(session_name, theory_name) + " AND " + Data.name.equal(name))
    1.69 +    db.using_statement(select)(stmt =>
    1.70 +    {
    1.71 +      val res = stmt.execute_query()
    1.72 +      if (res.next()) {
    1.73 +        val compressed = res.bool(Data.compressed)
    1.74 +        val body = res.bytes(Data.body)
    1.75 +        Entry(session_name, theory_name, name, compressed, body)
    1.76 +      }
    1.77 +      else error(Entry(session_name, theory_name, name, false, Bytes.empty).message("Bad export"))
    1.78 +    })
    1.79 +  }
    1.80 +
    1.81 +
    1.82 +  /* database consumer thread */
    1.83 +
    1.84 +  def consumer(db: SQL.Database): Consumer = new Consumer(db)
    1.85 +
    1.86 +  class Consumer private[Export](db: SQL.Database)
    1.87 +  {
    1.88 +    db.create_table(Data.table)
    1.89 +
    1.90 +    private val export_errors = Synchronized[List[String]](Nil)
    1.91 +
    1.92 +    private val consumer =
    1.93 +      Consumer_Thread.fork(name = "export")(consume = (future: Future[Entry]) =>
    1.94 +        {
    1.95 +          val entry = future.join
    1.96 +
    1.97 +          db.transaction {
    1.98 +            if (read_names(db, entry.session_name, entry.theory_name).contains(entry.name)) {
    1.99 +              export_errors.change(errs => entry.message("Duplicate export") :: errs)
   1.100 +            }
   1.101 +            else entry.write(db)
   1.102 +          }
   1.103 +          true
   1.104 +        })
   1.105 +
   1.106 +    def apply(session_name: String, args: Markup.Export.Args, body: Bytes)
   1.107 +    {
   1.108 +      consumer.send(
   1.109 +        if (args.compress)
   1.110 +          Future.fork(Entry(session_name, args.theory_name, args.name, true, body.compress()))
   1.111 +        else
   1.112 +          Future.value(Entry(session_name, args.theory_name, args.name, false, body)))
   1.113 +    }
   1.114 +
   1.115 +    def shutdown(close: Boolean = false): List[String] =
   1.116 +    {
   1.117 +      consumer.shutdown()
   1.118 +      if (close) db.close()
   1.119 +      export_errors.value.reverse
   1.120 +    }
   1.121 +  }
   1.122 +}
     2.1 --- a/src/Pure/Tools/build.scala	Sun May 06 23:01:45 2018 +0200
     2.2 +++ b/src/Pure/Tools/build.scala	Sun May 06 23:03:08 2018 +0200
     2.3 @@ -195,6 +195,8 @@
     2.4      private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf")
     2.5      isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph_display)
     2.6  
     2.7 +    private val export_consumer = Export.consumer(SQLite.open_database(store.output_database(name)))
     2.8 +
     2.9      private val future_result: Future[Process_Result] =
    2.10        Future.thread("build") {
    2.11          val parent = info.parent.getOrElse("")
    2.12 @@ -286,7 +288,7 @@
    2.13                      text <- Library.try_unprefix("\fexport = ", line)
    2.14                      (args, body) <-
    2.15                        Markup.Export.dest_inline(XML.Decode.properties(YXML.parse_body(text)))
    2.16 -                  } { } // FIXME
    2.17 +                  } { export_consumer(name, args, body) }
    2.18                },
    2.19              progress_limit =
    2.20                options.int("process_output_limit") match {
    2.21 @@ -310,8 +312,14 @@
    2.22      def join: Process_Result =
    2.23      {
    2.24        val result = future_result.join
    2.25 +      val export_result =
    2.26 +        export_consumer.shutdown(close = true).map(Output.error_message_text(_)) match {
    2.27 +          case Nil => result
    2.28 +          case errs if result.ok => result.copy(rc = 1).errors(errs)
    2.29 +          case errs => result.errors(errs)
    2.30 +        }
    2.31  
    2.32 -      if (result.ok)
    2.33 +      if (export_result.ok)
    2.34          Present.finish(progress, store.browser_info, graph_file, info, name)
    2.35  
    2.36        graph_file.delete
    2.37 @@ -322,11 +330,11 @@
    2.38            case Some(request) => !request.cancel
    2.39          }
    2.40  
    2.41 -      if (result.interrupted) {
    2.42 -        if (was_timeout) result.error(Output.error_message_text("Timeout")).was_timeout
    2.43 -        else result.error(Output.error_message_text("Interrupt"))
    2.44 +      if (export_result.interrupted) {
    2.45 +        if (was_timeout) export_result.error(Output.error_message_text("Timeout")).was_timeout
    2.46 +        else export_result.error(Output.error_message_text("Interrupt"))
    2.47        }
    2.48 -      else result
    2.49 +      else export_result
    2.50      }
    2.51    }
    2.52  
     3.1 --- a/src/Pure/build-jars	Sun May 06 23:01:45 2018 +0200
     3.2 +++ b/src/Pure/build-jars	Sun May 06 23:03:08 2018 +0200
     3.3 @@ -129,6 +129,7 @@
     3.4    System/system_channel.scala
     3.5    System/tty_loop.scala
     3.6    Thy/bibtex.scala
     3.7 +  Thy/export.scala
     3.8    Thy/html.scala
     3.9    Thy/latex.scala
    3.10    Thy/present.scala