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