src/Pure/Thy/export.scala
author wenzelm
Wed Jan 16 17:55:26 2019 +0100 (10 months ago)
changeset 69671 2486792eaf61
parent 69635 95dc926fa39c
child 69756 1907222d974e
permissions -rw-r--r--
support pruning of export names;
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@69634
    16
  /* structured name */
wenzelm@69634
    17
wenzelm@69634
    18
  val sep_char: Char = '/'
wenzelm@69634
    19
  val sep: String = sep_char.toString
wenzelm@69634
    20
wenzelm@69634
    21
  def explode_name(s: String): List[String] = space_explode(sep_char, s)
wenzelm@69634
    22
  def implode_name(elems: Iterable[String]): String = elems.mkString(sep)
wenzelm@69634
    23
wenzelm@69634
    24
wenzelm@68092
    25
  /* SQL data model */
wenzelm@68092
    26
wenzelm@68092
    27
  object Data
wenzelm@68092
    28
  {
wenzelm@68092
    29
    val session_name = SQL.Column.string("session_name").make_primary_key
wenzelm@68092
    30
    val theory_name = SQL.Column.string("theory_name").make_primary_key
wenzelm@68092
    31
    val name = SQL.Column.string("name").make_primary_key
wenzelm@68092
    32
    val compressed = SQL.Column.bool("compressed")
wenzelm@68092
    33
    val body = SQL.Column.bytes("body")
wenzelm@68092
    34
wenzelm@68092
    35
    val table =
wenzelm@68092
    36
      SQL.Table("isabelle_exports", List(session_name, theory_name, name, compressed, body))
wenzelm@68092
    37
wenzelm@68116
    38
    def where_equal(session_name: String, theory_name: String = "", name: String = ""): SQL.Source =
wenzelm@68092
    39
      "WHERE " + Data.session_name.equal(session_name) +
wenzelm@68116
    40
        (if (theory_name == "") "" else " AND " + Data.theory_name.equal(theory_name)) +
wenzelm@68116
    41
        (if (name == "") "" else " AND " + Data.name.equal(name))
wenzelm@68116
    42
  }
wenzelm@68116
    43
wenzelm@68116
    44
  def read_name(db: SQL.Database, session_name: String, theory_name: String, name: String): Boolean =
wenzelm@68116
    45
  {
wenzelm@68116
    46
    val select =
wenzelm@68116
    47
      Data.table.select(List(Data.name), Data.where_equal(session_name, theory_name, name))
wenzelm@68116
    48
    db.using_statement(select)(stmt => stmt.execute_query().next())
wenzelm@68092
    49
  }
wenzelm@68092
    50
wenzelm@68092
    51
  def read_names(db: SQL.Database, session_name: String, theory_name: String): List[String] =
wenzelm@68092
    52
  {
wenzelm@68092
    53
    val select = Data.table.select(List(Data.name), Data.where_equal(session_name, theory_name))
wenzelm@68092
    54
    db.using_statement(select)(stmt =>
wenzelm@68092
    55
      stmt.execute_query().iterator(res => res.string(Data.name)).toList)
wenzelm@68092
    56
  }
wenzelm@68092
    57
wenzelm@68222
    58
  def read_theory_names(db: SQL.Database, session_name: String): List[String] =
wenzelm@68222
    59
  {
wenzelm@68222
    60
    val select =
wenzelm@68222
    61
      Data.table.select(List(Data.theory_name), Data.where_equal(session_name), distinct = true)
wenzelm@68222
    62
    db.using_statement(select)(stmt =>
wenzelm@68222
    63
      stmt.execute_query().iterator(_.string(Data.theory_name)).toList)
wenzelm@68222
    64
  }
wenzelm@68222
    65
wenzelm@68222
    66
  def read_theory_exports(db: SQL.Database, session_name: String): List[(String, String)] =
wenzelm@68115
    67
  {
wenzelm@68116
    68
    val select = Data.table.select(List(Data.theory_name, Data.name), Data.where_equal(session_name))
wenzelm@68116
    69
    db.using_statement(select)(stmt =>
wenzelm@68116
    70
      stmt.execute_query().iterator(res =>
wenzelm@68116
    71
        (res.string(Data.theory_name), res.string(Data.name))).toList)
wenzelm@68115
    72
  }
wenzelm@68115
    73
wenzelm@68104
    74
  def message(msg: String, theory_name: String, name: String): String =
wenzelm@68104
    75
    msg + " " + quote(name) + " for theory " + quote(theory_name)
wenzelm@68104
    76
wenzelm@68116
    77
  def compound_name(a: String, b: String): String = a + ":" + b
wenzelm@68116
    78
wenzelm@68092
    79
  sealed case class Entry(
wenzelm@68103
    80
    session_name: String,
wenzelm@68103
    81
    theory_name: String,
wenzelm@68103
    82
    name: String,
wenzelm@68167
    83
    body: Future[(Boolean, Bytes)])
wenzelm@68092
    84
  {
wenzelm@69635
    85
    override def toString: String = name
wenzelm@69630
    86
wenzelm@69634
    87
    val name_elems: List[String] = explode_name(name)
wenzelm@69634
    88
wenzelm@69634
    89
    def name_extends(elems: List[String]): Boolean =
wenzelm@69634
    90
      name_elems.startsWith(elems) && name_elems != elems
wenzelm@69634
    91
wenzelm@69630
    92
    def text: String = uncompressed().text
wenzelm@68092
    93
wenzelm@69629
    94
    def uncompressed(cache: XZ.Cache = XZ.cache()): Bytes =
wenzelm@69629
    95
    {
wenzelm@69629
    96
      val (compressed, bytes) = body.join
wenzelm@69629
    97
      if (compressed) bytes.uncompress(cache = cache) else bytes
wenzelm@69629
    98
    }
wenzelm@69629
    99
wenzelm@69629
   100
    def uncompressed_yxml(cache: XZ.Cache = XZ.cache()): XML.Body =
wenzelm@69629
   101
      YXML.parse_body(UTF8.decode_permissive(uncompressed(cache = cache)))
wenzelm@69629
   102
wenzelm@68092
   103
    def write(db: SQL.Database)
wenzelm@68092
   104
    {
wenzelm@68167
   105
      val (compressed, bytes) = body.join
wenzelm@68092
   106
      db.using_statement(Data.table.insert())(stmt =>
wenzelm@68092
   107
      {
wenzelm@68092
   108
        stmt.string(1) = session_name
wenzelm@68092
   109
        stmt.string(2) = theory_name
wenzelm@68092
   110
        stmt.string(3) = name
wenzelm@68092
   111
        stmt.bool(4) = compressed
wenzelm@68103
   112
        stmt.bytes(5) = bytes
wenzelm@68092
   113
        stmt.execute()
wenzelm@68092
   114
      })
wenzelm@68092
   115
    }
wenzelm@68116
   116
  }
wenzelm@68116
   117
wenzelm@68116
   118
  def make_regex(pattern: String): Regex =
wenzelm@68116
   119
  {
wenzelm@68116
   120
    @tailrec def make(result: List[String], depth: Int, chs: List[Char]): Regex =
wenzelm@68116
   121
      chs match {
wenzelm@68116
   122
        case '*' :: '*' :: rest => make("[^:]*" :: result, depth, rest)
wenzelm@68116
   123
        case '*' :: rest => make("[^:/]*" :: result, depth, rest)
wenzelm@68116
   124
        case '?' :: rest => make("[^:/]" :: result, depth, rest)
wenzelm@68116
   125
        case '\\' :: c :: rest => make(("\\" + c) :: result, depth, rest)
wenzelm@68116
   126
        case '{' :: rest => make("(" :: result, depth + 1, rest)
wenzelm@68116
   127
        case ',' :: rest if depth > 0 => make("|" :: result, depth, rest)
wenzelm@68116
   128
        case '}' :: rest if depth > 0 => make(")" :: result, depth - 1, rest)
wenzelm@68116
   129
        case c :: rest if ".+()".contains(c) => make(("\\" + c) :: result, depth, rest)
wenzelm@68116
   130
        case c :: rest => make(c.toString :: result, depth, rest)
wenzelm@68116
   131
        case Nil => result.reverse.mkString.r
wenzelm@68116
   132
      }
wenzelm@68116
   133
    make(Nil, 0, pattern.toList)
wenzelm@68092
   134
  }
wenzelm@68092
   135
wenzelm@68151
   136
  def make_matcher(pattern: String): (String, String) => Boolean =
wenzelm@68151
   137
  {
wenzelm@68151
   138
    val regex = make_regex(pattern)
wenzelm@68151
   139
    (theory_name: String, name: String) =>
wenzelm@68151
   140
      regex.pattern.matcher(compound_name(theory_name, name)).matches
wenzelm@68151
   141
  }
wenzelm@68151
   142
wenzelm@68166
   143
  def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes,
wenzelm@68166
   144
    cache: XZ.Cache = XZ.cache()): Entry =
wenzelm@68101
   145
  {
wenzelm@68167
   146
    Entry(session_name, args.theory_name, args.name,
wenzelm@68167
   147
      if (args.compress) Future.fork(body.maybe_compress(cache = cache))
wenzelm@68167
   148
      else Future.value((false, body)))
wenzelm@68101
   149
  }
wenzelm@68101
   150
wenzelm@68202
   151
  def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String)
wenzelm@68202
   152
    : Option[Entry] =
wenzelm@68092
   153
  {
wenzelm@68092
   154
    val select =
wenzelm@68092
   155
      Data.table.select(List(Data.compressed, Data.body),
wenzelm@68116
   156
        Data.where_equal(session_name, theory_name, name))
wenzelm@68092
   157
    db.using_statement(select)(stmt =>
wenzelm@68092
   158
    {
wenzelm@68092
   159
      val res = stmt.execute_query()
wenzelm@68092
   160
      if (res.next()) {
wenzelm@68092
   161
        val compressed = res.bool(Data.compressed)
wenzelm@68092
   162
        val body = res.bytes(Data.body)
wenzelm@68202
   163
        Some(Entry(session_name, theory_name, name, Future.value(compressed, body)))
wenzelm@68092
   164
      }
wenzelm@68202
   165
      else None
wenzelm@68092
   166
    })
wenzelm@68092
   167
  }
wenzelm@68092
   168
wenzelm@68831
   169
  def read_entry(dir: Path, session_name: String, theory_name: String, name: String): Option[Entry] =
wenzelm@68831
   170
  {
wenzelm@68831
   171
    val path = dir + Path.basic(theory_name) + Path.explode(name)
wenzelm@68831
   172
    if (path.is_file) {
wenzelm@68831
   173
      val uncompressed = Bytes.read(path)
wenzelm@68831
   174
      Some(Entry(session_name, theory_name, name, Future.value((false, uncompressed))))
wenzelm@68831
   175
    }
wenzelm@68831
   176
    else None
wenzelm@68831
   177
  }
wenzelm@68831
   178
wenzelm@68092
   179
wenzelm@68092
   180
  /* database consumer thread */
wenzelm@68092
   181
wenzelm@68289
   182
  def consumer(db: SQL.Database, cache: XZ.Cache = XZ.cache()): Consumer = new Consumer(db, cache)
wenzelm@68092
   183
wenzelm@68289
   184
  class Consumer private[Export](db: SQL.Database, cache: XZ.Cache)
wenzelm@68092
   185
  {
wenzelm@68924
   186
    private val errors = Synchronized[List[String]](Nil)
wenzelm@68092
   187
wenzelm@68092
   188
    private val consumer =
wenzelm@68103
   189
      Consumer_Thread.fork(name = "export")(consume = (entry: Entry) =>
wenzelm@68092
   190
        {
wenzelm@68103
   191
          entry.body.join
wenzelm@68092
   192
          db.transaction {
wenzelm@68115
   193
            if (read_name(db, entry.session_name, entry.theory_name, entry.name)) {
wenzelm@68924
   194
              val msg = message("Duplicate export", entry.theory_name, entry.name)
wenzelm@68924
   195
              errors.change(msg :: _)
wenzelm@68092
   196
            }
wenzelm@68092
   197
            else entry.write(db)
wenzelm@68092
   198
          }
wenzelm@68092
   199
          true
wenzelm@68092
   200
        })
wenzelm@68092
   201
wenzelm@68103
   202
    def apply(session_name: String, args: Markup.Export.Args, body: Bytes): Unit =
wenzelm@68289
   203
      consumer.send(make_entry(session_name, args, body, cache = cache))
wenzelm@68092
   204
wenzelm@68092
   205
    def shutdown(close: Boolean = false): List[String] =
wenzelm@68092
   206
    {
wenzelm@68092
   207
      consumer.shutdown()
wenzelm@68092
   208
      if (close) db.close()
wenzelm@68924
   209
      errors.value.reverse
wenzelm@68092
   210
    }
wenzelm@68092
   211
  }
wenzelm@68116
   212
wenzelm@68116
   213
wenzelm@68418
   214
  /* abstract provider */
wenzelm@68418
   215
wenzelm@68418
   216
  object Provider
wenzelm@68418
   217
  {
wenzelm@68418
   218
    def database(db: SQL.Database, session_name: String, theory_name: String): Provider =
wenzelm@68418
   219
      new Provider {
wenzelm@68418
   220
        def apply(export_name: String): Option[Entry] =
wenzelm@68418
   221
          read_entry(db, session_name, theory_name, export_name)
wenzelm@68832
   222
wenzelm@68832
   223
        override def toString: String = db.toString
wenzelm@68418
   224
      }
wenzelm@68418
   225
wenzelm@68418
   226
    def snapshot(snapshot: Document.Snapshot): Provider =
wenzelm@68418
   227
      new Provider {
wenzelm@68418
   228
        def apply(export_name: String): Option[Entry] =
wenzelm@68418
   229
          snapshot.exports_map.get(export_name)
wenzelm@68832
   230
wenzelm@68832
   231
        override def toString: String = snapshot.toString
wenzelm@68418
   232
      }
wenzelm@68831
   233
wenzelm@68831
   234
    def directory(dir: Path, session_name: String, theory_name: String): Provider =
wenzelm@68831
   235
      new Provider {
wenzelm@68831
   236
        def apply(export_name: String): Option[Entry] =
wenzelm@68831
   237
          read_entry(dir, session_name, theory_name, export_name)
wenzelm@68832
   238
wenzelm@68832
   239
        override def toString: String = dir.toString
wenzelm@68831
   240
      }
wenzelm@68418
   241
  }
wenzelm@68418
   242
wenzelm@68418
   243
  trait Provider
wenzelm@68418
   244
  {
wenzelm@68418
   245
    def apply(export_name: String): Option[Entry]
wenzelm@68418
   246
wenzelm@68418
   247
    def uncompressed_yxml(export_name: String, cache: XZ.Cache = XZ.cache()): XML.Body =
wenzelm@68418
   248
      apply(export_name) match {
wenzelm@68418
   249
        case Some(entry) => entry.uncompressed_yxml(cache = cache)
wenzelm@68418
   250
        case None => Nil
wenzelm@68418
   251
      }
wenzelm@68418
   252
  }
wenzelm@68418
   253
wenzelm@68418
   254
wenzelm@68288
   255
  /* export to file-system */
wenzelm@68288
   256
wenzelm@68288
   257
  def export_files(
wenzelm@68288
   258
    store: Sessions.Store,
wenzelm@68288
   259
    session_name: String,
wenzelm@68288
   260
    export_dir: Path,
wenzelm@68288
   261
    progress: Progress = No_Progress,
wenzelm@69671
   262
    export_prune: Int = 0,
wenzelm@68288
   263
    export_list: Boolean = false,
wenzelm@68291
   264
    export_patterns: List[String] = Nil,
wenzelm@68291
   265
    export_prefix: String = "")
wenzelm@68288
   266
  {
wenzelm@68288
   267
    using(store.open_database(session_name))(db =>
wenzelm@68288
   268
    {
wenzelm@68288
   269
      db.transaction {
wenzelm@68288
   270
        val export_names = read_theory_exports(db, session_name)
wenzelm@68288
   271
wenzelm@68288
   272
        // list
wenzelm@68288
   273
        if (export_list) {
wenzelm@68288
   274
          (for ((theory_name, name) <- export_names) yield compound_name(theory_name, name)).
wenzelm@68291
   275
            sorted.foreach(progress.echo(_))
wenzelm@68288
   276
        }
wenzelm@68288
   277
wenzelm@68288
   278
        // export
wenzelm@68290
   279
        if (export_patterns.nonEmpty) {
wenzelm@68290
   280
          val exports =
wenzelm@68290
   281
            (for {
wenzelm@68290
   282
              export_pattern <- export_patterns.iterator
wenzelm@68290
   283
              matcher = make_matcher(export_pattern)
wenzelm@68290
   284
              (theory_name, name) <- export_names if matcher(theory_name, name)
wenzelm@68290
   285
            } yield (theory_name, name)).toSet
wenzelm@68288
   286
          for {
wenzelm@68290
   287
            (theory_name, group) <- exports.toList.groupBy(_._1).toList.sortBy(_._1)
wenzelm@68290
   288
            name <- group.map(_._2).sorted
wenzelm@68288
   289
            entry <- read_entry(db, session_name, theory_name, name)
wenzelm@68288
   290
          } {
wenzelm@69671
   291
            val elems = theory_name :: space_explode('/', name)
wenzelm@69671
   292
            val path =
wenzelm@69671
   293
              if (elems.length < export_prune + 1) {
wenzelm@69671
   294
                error("Cannot prune path by " + export_prune + " element(s): " + Path.make(elems))
wenzelm@69671
   295
              }
wenzelm@69671
   296
              else export_dir + Path.make(elems.drop(export_prune))
wenzelm@69671
   297
wenzelm@68291
   298
            progress.echo(export_prefix + "export " + path)
wenzelm@68288
   299
            Isabelle_System.mkdirs(path.dir)
wenzelm@68289
   300
            Bytes.write(path, entry.uncompressed(cache = store.xz_cache))
wenzelm@68288
   301
          }
wenzelm@68288
   302
        }
wenzelm@68288
   303
      }
wenzelm@68288
   304
    })
wenzelm@68288
   305
  }
wenzelm@68288
   306
wenzelm@68288
   307
wenzelm@68116
   308
  /* Isabelle tool wrapper */
wenzelm@68116
   309
wenzelm@68116
   310
  val default_export_dir = Path.explode("export")
wenzelm@68116
   311
wenzelm@68116
   312
  val isabelle_tool = Isabelle_Tool("export", "retrieve theory exports", args =>
wenzelm@68116
   313
  {
wenzelm@68116
   314
    /* arguments */
wenzelm@68116
   315
wenzelm@68116
   316
    var export_dir = default_export_dir
wenzelm@68116
   317
    var dirs: List[Path] = Nil
wenzelm@68116
   318
    var export_list = false
wenzelm@68116
   319
    var no_build = false
wenzelm@68116
   320
    var options = Options.init()
wenzelm@69671
   321
    var export_prune = 0
wenzelm@68116
   322
    var system_mode = false
wenzelm@68290
   323
    var export_patterns: List[String] = Nil
wenzelm@68116
   324
wenzelm@68116
   325
    val getopts = Getopts("""
wenzelm@68116
   326
Usage: isabelle export [OPTIONS] SESSION
wenzelm@68116
   327
wenzelm@68116
   328
  Options are:
wenzelm@68314
   329
    -O DIR       output directory for exported files (default: """ + default_export_dir + """)
wenzelm@68116
   330
    -d DIR       include session directory
wenzelm@68116
   331
    -l           list exports
wenzelm@68116
   332
    -n           no build of session
wenzelm@68116
   333
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
wenzelm@69671
   334
    -p NUM       prune path of exported files by NUM elements
wenzelm@68116
   335
    -s           system build mode for session image
wenzelm@68116
   336
    -x PATTERN   extract files matching pattern (e.g. "*:**" for all)
wenzelm@68116
   337
wenzelm@68116
   338
  List or export theory exports for SESSION: named blobs produced by
wenzelm@68290
   339
  isabelle build. Option -l or -x is required; option -x may be repeated.
wenzelm@68116
   340
wenzelm@68116
   341
  The PATTERN language resembles glob patterns in the shell, with ? and *
wenzelm@68116
   342
  (both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc],
wenzelm@68116
   343
  and variants {pattern1,pattern2,pattern3}.
wenzelm@68116
   344
""",
wenzelm@68314
   345
      "O:" -> (arg => export_dir = Path.explode(arg)),
wenzelm@68116
   346
      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
wenzelm@68116
   347
      "l" -> (_ => export_list = true),
wenzelm@68116
   348
      "n" -> (_ => no_build = true),
wenzelm@68116
   349
      "o:" -> (arg => options = options + arg),
wenzelm@69671
   350
      "p:" -> (arg => export_prune = Value.Int.parse(arg)),
wenzelm@68116
   351
      "s" -> (_ => system_mode = true),
wenzelm@68290
   352
      "x:" -> (arg => export_patterns ::= arg))
wenzelm@68116
   353
wenzelm@68116
   354
    val more_args = getopts(args)
wenzelm@68116
   355
    val session_name =
wenzelm@68116
   356
      more_args match {
wenzelm@68290
   357
        case List(session_name) if export_list || export_patterns.nonEmpty => session_name
wenzelm@68116
   358
        case _ => getopts.usage()
wenzelm@68116
   359
      }
wenzelm@68116
   360
wenzelm@68305
   361
    val progress = new Console_Progress()
wenzelm@68305
   362
wenzelm@68116
   363
wenzelm@68116
   364
    /* build */
wenzelm@68116
   365
wenzelm@68305
   366
    if (!no_build) {
wenzelm@68305
   367
      val rc =
wenzelm@68331
   368
        progress.interrupt_handler {
wenzelm@68331
   369
          Build.build_logic(options, session_name, progress = progress,
wenzelm@68331
   370
            dirs = dirs, system_mode = system_mode)
wenzelm@68331
   371
        }
wenzelm@68305
   372
      if (rc != 0) sys.exit(rc)
wenzelm@68116
   373
    }
wenzelm@68116
   374
wenzelm@68116
   375
wenzelm@68288
   376
    /* export files */
wenzelm@68116
   377
wenzelm@68209
   378
    val store = Sessions.store(options, system_mode)
wenzelm@69671
   379
    export_files(store, session_name, export_dir, progress = progress, export_prune = export_prune,
wenzelm@68290
   380
      export_list = export_list, export_patterns = export_patterns)
wenzelm@68116
   381
  })
wenzelm@68092
   382
}