src/Pure/Thy/export.scala
author wenzelm
Thu May 17 14:40:58 2018 +0200 (6 months ago)
changeset 68202 a99180ad3441
parent 68171 13162bb3a677
child 68205 9a8949f71fd4
permissions -rw-r--r--
clarified signature;
wenzelm@68092
     1
/*  Title:      Pure/Thy/export.scala
wenzelm@68092
     2
    Author:     Makarius
wenzelm@68092
     3
wenzelm@68102
     4
Manage theory exports: compressed blobs.
wenzelm@68092
     5
*/
wenzelm@68092
     6
wenzelm@68092
     7
package isabelle
wenzelm@68092
     8
wenzelm@68116
     9
wenzelm@68116
    10
import scala.annotation.tailrec
wenzelm@68116
    11
import scala.util.matching.Regex
wenzelm@68116
    12
wenzelm@68116
    13
wenzelm@68092
    14
object Export
wenzelm@68092
    15
{
wenzelm@68092
    16
  /* SQL data model */
wenzelm@68092
    17
wenzelm@68092
    18
  object Data
wenzelm@68092
    19
  {
wenzelm@68092
    20
    val session_name = SQL.Column.string("session_name").make_primary_key
wenzelm@68092
    21
    val theory_name = SQL.Column.string("theory_name").make_primary_key
wenzelm@68092
    22
    val name = SQL.Column.string("name").make_primary_key
wenzelm@68092
    23
    val compressed = SQL.Column.bool("compressed")
wenzelm@68092
    24
    val body = SQL.Column.bytes("body")
wenzelm@68092
    25
wenzelm@68092
    26
    val table =
wenzelm@68092
    27
      SQL.Table("isabelle_exports", List(session_name, theory_name, name, compressed, body))
wenzelm@68092
    28
wenzelm@68116
    29
    def where_equal(session_name: String, theory_name: String = "", name: String = ""): SQL.Source =
wenzelm@68092
    30
      "WHERE " + Data.session_name.equal(session_name) +
wenzelm@68116
    31
        (if (theory_name == "") "" else " AND " + Data.theory_name.equal(theory_name)) +
wenzelm@68116
    32
        (if (name == "") "" else " AND " + Data.name.equal(name))
wenzelm@68116
    33
  }
wenzelm@68116
    34
wenzelm@68116
    35
  def read_name(db: SQL.Database, session_name: String, theory_name: String, name: String): Boolean =
wenzelm@68116
    36
  {
wenzelm@68116
    37
    val select =
wenzelm@68116
    38
      Data.table.select(List(Data.name), Data.where_equal(session_name, theory_name, name))
wenzelm@68116
    39
    db.using_statement(select)(stmt => stmt.execute_query().next())
wenzelm@68092
    40
  }
wenzelm@68092
    41
wenzelm@68092
    42
  def read_names(db: SQL.Database, session_name: String, theory_name: String): List[String] =
wenzelm@68092
    43
  {
wenzelm@68092
    44
    val select = Data.table.select(List(Data.name), Data.where_equal(session_name, theory_name))
wenzelm@68092
    45
    db.using_statement(select)(stmt =>
wenzelm@68092
    46
      stmt.execute_query().iterator(res => res.string(Data.name)).toList)
wenzelm@68092
    47
  }
wenzelm@68092
    48
wenzelm@68116
    49
  def read_theory_names(db: SQL.Database, session_name: String): List[(String, String)] =
wenzelm@68115
    50
  {
wenzelm@68116
    51
    val select = Data.table.select(List(Data.theory_name, Data.name), Data.where_equal(session_name))
wenzelm@68116
    52
    db.using_statement(select)(stmt =>
wenzelm@68116
    53
      stmt.execute_query().iterator(res =>
wenzelm@68116
    54
        (res.string(Data.theory_name), res.string(Data.name))).toList)
wenzelm@68115
    55
  }
wenzelm@68115
    56
wenzelm@68104
    57
  def message(msg: String, theory_name: String, name: String): String =
wenzelm@68104
    58
    msg + " " + quote(name) + " for theory " + quote(theory_name)
wenzelm@68104
    59
wenzelm@68116
    60
  def compound_name(a: String, b: String): String = a + ":" + b
wenzelm@68116
    61
wenzelm@68092
    62
  sealed case class Entry(
wenzelm@68103
    63
    session_name: String,
wenzelm@68103
    64
    theory_name: String,
wenzelm@68103
    65
    name: String,
wenzelm@68167
    66
    body: Future[(Boolean, Bytes)])
wenzelm@68092
    67
  {
wenzelm@68116
    68
    override def toString: String = compound_name(theory_name, name)
wenzelm@68092
    69
wenzelm@68092
    70
    def write(db: SQL.Database)
wenzelm@68092
    71
    {
wenzelm@68167
    72
      val (compressed, bytes) = body.join
wenzelm@68092
    73
      db.using_statement(Data.table.insert())(stmt =>
wenzelm@68092
    74
      {
wenzelm@68092
    75
        stmt.string(1) = session_name
wenzelm@68092
    76
        stmt.string(2) = theory_name
wenzelm@68092
    77
        stmt.string(3) = name
wenzelm@68092
    78
        stmt.bool(4) = compressed
wenzelm@68103
    79
        stmt.bytes(5) = bytes
wenzelm@68092
    80
        stmt.execute()
wenzelm@68092
    81
      })
wenzelm@68092
    82
    }
wenzelm@68116
    83
wenzelm@68167
    84
    def uncompressed(cache: XZ.Cache = XZ.cache()): Bytes =
wenzelm@68167
    85
    {
wenzelm@68167
    86
      val (compressed, bytes) = body.join
wenzelm@68167
    87
      if (compressed) bytes.uncompress(cache = cache) else bytes
wenzelm@68167
    88
    }
wenzelm@68171
    89
wenzelm@68171
    90
    def uncompressed_yxml(cache: XZ.Cache = XZ.cache()): XML.Body =
wenzelm@68171
    91
      YXML.parse_body(UTF8.decode_permissive(uncompressed(cache = cache)))
wenzelm@68116
    92
  }
wenzelm@68116
    93
wenzelm@68116
    94
  def make_regex(pattern: String): Regex =
wenzelm@68116
    95
  {
wenzelm@68116
    96
    @tailrec def make(result: List[String], depth: Int, chs: List[Char]): Regex =
wenzelm@68116
    97
      chs match {
wenzelm@68116
    98
        case '*' :: '*' :: rest => make("[^:]*" :: result, depth, rest)
wenzelm@68116
    99
        case '*' :: rest => make("[^:/]*" :: result, depth, rest)
wenzelm@68116
   100
        case '?' :: rest => make("[^:/]" :: result, depth, rest)
wenzelm@68116
   101
        case '\\' :: c :: rest => make(("\\" + c) :: result, depth, rest)
wenzelm@68116
   102
        case '{' :: rest => make("(" :: result, depth + 1, rest)
wenzelm@68116
   103
        case ',' :: rest if depth > 0 => make("|" :: result, depth, rest)
wenzelm@68116
   104
        case '}' :: rest if depth > 0 => make(")" :: result, depth - 1, rest)
wenzelm@68116
   105
        case c :: rest if ".+()".contains(c) => make(("\\" + c) :: result, depth, rest)
wenzelm@68116
   106
        case c :: rest => make(c.toString :: result, depth, rest)
wenzelm@68116
   107
        case Nil => result.reverse.mkString.r
wenzelm@68116
   108
      }
wenzelm@68116
   109
    make(Nil, 0, pattern.toList)
wenzelm@68092
   110
  }
wenzelm@68092
   111
wenzelm@68151
   112
  def make_matcher(pattern: String): (String, String) => Boolean =
wenzelm@68151
   113
  {
wenzelm@68151
   114
    val regex = make_regex(pattern)
wenzelm@68151
   115
    (theory_name: String, name: String) =>
wenzelm@68151
   116
      regex.pattern.matcher(compound_name(theory_name, name)).matches
wenzelm@68151
   117
  }
wenzelm@68151
   118
wenzelm@68166
   119
  def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes,
wenzelm@68166
   120
    cache: XZ.Cache = XZ.cache()): Entry =
wenzelm@68101
   121
  {
wenzelm@68167
   122
    Entry(session_name, args.theory_name, args.name,
wenzelm@68167
   123
      if (args.compress) Future.fork(body.maybe_compress(cache = cache))
wenzelm@68167
   124
      else Future.value((false, body)))
wenzelm@68101
   125
  }
wenzelm@68101
   126
wenzelm@68202
   127
  def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String)
wenzelm@68202
   128
    : Option[Entry] =
wenzelm@68092
   129
  {
wenzelm@68092
   130
    val select =
wenzelm@68092
   131
      Data.table.select(List(Data.compressed, Data.body),
wenzelm@68116
   132
        Data.where_equal(session_name, theory_name, name))
wenzelm@68092
   133
    db.using_statement(select)(stmt =>
wenzelm@68092
   134
    {
wenzelm@68092
   135
      val res = stmt.execute_query()
wenzelm@68092
   136
      if (res.next()) {
wenzelm@68092
   137
        val compressed = res.bool(Data.compressed)
wenzelm@68092
   138
        val body = res.bytes(Data.body)
wenzelm@68202
   139
        Some(Entry(session_name, theory_name, name, Future.value(compressed, body)))
wenzelm@68092
   140
      }
wenzelm@68202
   141
      else None
wenzelm@68092
   142
    })
wenzelm@68092
   143
  }
wenzelm@68092
   144
wenzelm@68092
   145
wenzelm@68092
   146
  /* database consumer thread */
wenzelm@68092
   147
wenzelm@68092
   148
  def consumer(db: SQL.Database): Consumer = new Consumer(db)
wenzelm@68092
   149
wenzelm@68092
   150
  class Consumer private[Export](db: SQL.Database)
wenzelm@68092
   151
  {
wenzelm@68166
   152
    val xz_cache = XZ.make_cache()
wenzelm@68166
   153
wenzelm@68092
   154
    db.create_table(Data.table)
wenzelm@68092
   155
wenzelm@68092
   156
    private val export_errors = Synchronized[List[String]](Nil)
wenzelm@68092
   157
wenzelm@68092
   158
    private val consumer =
wenzelm@68103
   159
      Consumer_Thread.fork(name = "export")(consume = (entry: Entry) =>
wenzelm@68092
   160
        {
wenzelm@68103
   161
          entry.body.join
wenzelm@68092
   162
          db.transaction {
wenzelm@68115
   163
            if (read_name(db, entry.session_name, entry.theory_name, entry.name)) {
wenzelm@68104
   164
              val err = message("Duplicate export", entry.theory_name, entry.name)
wenzelm@68104
   165
              export_errors.change(errs => err :: errs)
wenzelm@68092
   166
            }
wenzelm@68092
   167
            else entry.write(db)
wenzelm@68092
   168
          }
wenzelm@68092
   169
          true
wenzelm@68092
   170
        })
wenzelm@68092
   171
wenzelm@68103
   172
    def apply(session_name: String, args: Markup.Export.Args, body: Bytes): Unit =
wenzelm@68166
   173
      consumer.send(make_entry(session_name, args, body, cache = xz_cache))
wenzelm@68092
   174
wenzelm@68092
   175
    def shutdown(close: Boolean = false): List[String] =
wenzelm@68092
   176
    {
wenzelm@68092
   177
      consumer.shutdown()
wenzelm@68092
   178
      if (close) db.close()
wenzelm@68092
   179
      export_errors.value.reverse
wenzelm@68092
   180
    }
wenzelm@68092
   181
  }
wenzelm@68116
   182
wenzelm@68116
   183
wenzelm@68116
   184
  /* Isabelle tool wrapper */
wenzelm@68116
   185
wenzelm@68116
   186
  val default_export_dir = Path.explode("export")
wenzelm@68116
   187
wenzelm@68116
   188
  val isabelle_tool = Isabelle_Tool("export", "retrieve theory exports", args =>
wenzelm@68116
   189
  {
wenzelm@68116
   190
    /* arguments */
wenzelm@68116
   191
wenzelm@68116
   192
    var export_dir = default_export_dir
wenzelm@68116
   193
    var dirs: List[Path] = Nil
wenzelm@68116
   194
    var export_list = false
wenzelm@68116
   195
    var no_build = false
wenzelm@68116
   196
    var options = Options.init()
wenzelm@68116
   197
    var system_mode = false
wenzelm@68116
   198
    var export_pattern = ""
wenzelm@68116
   199
wenzelm@68116
   200
    val getopts = Getopts("""
wenzelm@68116
   201
Usage: isabelle export [OPTIONS] SESSION
wenzelm@68116
   202
wenzelm@68116
   203
  Options are:
wenzelm@68116
   204
    -D DIR       target directory for exported files (default: """ + default_export_dir + """)
wenzelm@68116
   205
    -d DIR       include session directory
wenzelm@68116
   206
    -l           list exports
wenzelm@68116
   207
    -n           no build of session
wenzelm@68116
   208
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
wenzelm@68116
   209
    -s           system build mode for session image
wenzelm@68116
   210
    -x PATTERN   extract files matching pattern (e.g. "*:**" for all)
wenzelm@68116
   211
wenzelm@68116
   212
  List or export theory exports for SESSION: named blobs produced by
wenzelm@68116
   213
  isabelle build. Option -l or -x is required.
wenzelm@68116
   214
wenzelm@68116
   215
  The PATTERN language resembles glob patterns in the shell, with ? and *
wenzelm@68116
   216
  (both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc],
wenzelm@68116
   217
  and variants {pattern1,pattern2,pattern3}.
wenzelm@68116
   218
""",
wenzelm@68116
   219
      "D:" -> (arg => export_dir = Path.explode(arg)),
wenzelm@68116
   220
      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
wenzelm@68116
   221
      "l" -> (_ => export_list = true),
wenzelm@68116
   222
      "n" -> (_ => no_build = true),
wenzelm@68116
   223
      "o:" -> (arg => options = options + arg),
wenzelm@68116
   224
      "s" -> (_ => system_mode = true),
wenzelm@68116
   225
      "x:" -> (arg => export_pattern = arg))
wenzelm@68116
   226
wenzelm@68116
   227
    val more_args = getopts(args)
wenzelm@68116
   228
    val session_name =
wenzelm@68116
   229
      more_args match {
wenzelm@68116
   230
        case List(session_name) if export_list || export_pattern != "" => session_name
wenzelm@68116
   231
        case _ => getopts.usage()
wenzelm@68116
   232
      }
wenzelm@68116
   233
wenzelm@68116
   234
wenzelm@68116
   235
    /* build */
wenzelm@68116
   236
wenzelm@68116
   237
    val progress = new Console_Progress()
wenzelm@68116
   238
wenzelm@68116
   239
    if (!no_build &&
wenzelm@68116
   240
        !Build.build(options, no_build = true, dirs = dirs, system_mode = system_mode,
wenzelm@68116
   241
          sessions = List(session_name)).ok)
wenzelm@68116
   242
    {
wenzelm@68116
   243
      progress.echo("Build started for Isabelle/" + session_name + " ...")
wenzelm@68116
   244
      progress.interrupt_handler {
wenzelm@68116
   245
        val res =
wenzelm@68116
   246
          Build.build(options, progress = progress, dirs = dirs, system_mode = system_mode,
wenzelm@68116
   247
            sessions = List(session_name))
wenzelm@68116
   248
        if (!res.ok) sys.exit(res.rc)
wenzelm@68116
   249
      }
wenzelm@68116
   250
    }
wenzelm@68116
   251
wenzelm@68116
   252
wenzelm@68116
   253
    /* database */
wenzelm@68116
   254
wenzelm@68116
   255
    val store = Sessions.store(system_mode)
wenzelm@68116
   256
    val database =
wenzelm@68116
   257
      store.find_database(session_name) match {
wenzelm@68116
   258
        case None => error("Missing database for session " + quote(session_name))
wenzelm@68116
   259
        case Some(database) => database
wenzelm@68116
   260
      }
wenzelm@68116
   261
wenzelm@68116
   262
    using(SQLite.open_database(database))(db =>
wenzelm@68116
   263
    {
wenzelm@68116
   264
      db.transaction {
wenzelm@68116
   265
        val export_names = read_theory_names(db, session_name)
wenzelm@68116
   266
wenzelm@68116
   267
        // list
wenzelm@68116
   268
        if (export_list) {
wenzelm@68116
   269
          (for ((theory_name, name) <- export_names) yield compound_name(theory_name, name)).
wenzelm@68116
   270
            sorted.foreach(Output.writeln(_, stdout = true))
wenzelm@68116
   271
        }
wenzelm@68116
   272
wenzelm@68116
   273
        // export
wenzelm@68116
   274
        if (export_pattern != "") {
wenzelm@68166
   275
          val xz_cache = XZ.make_cache()
wenzelm@68166
   276
wenzelm@68151
   277
          val matcher = make_matcher(export_pattern)
wenzelm@68202
   278
          for {
wenzelm@68202
   279
            (theory_name, name) <- export_names if matcher(theory_name, name)
wenzelm@68202
   280
            entry <- read_entry(db, session_name, theory_name, name)
wenzelm@68202
   281
          } {
wenzelm@68116
   282
            val path = export_dir + Path.basic(theory_name) + Path.explode(name)
wenzelm@68116
   283
            progress.echo("exporting " + path)
wenzelm@68116
   284
            Isabelle_System.mkdirs(path.dir)
wenzelm@68167
   285
            Bytes.write(path, entry.uncompressed(cache = xz_cache))
wenzelm@68116
   286
          }
wenzelm@68116
   287
        }
wenzelm@68116
   288
      }
wenzelm@68116
   289
    })
wenzelm@68116
   290
  })
wenzelm@68092
   291
}