src/Pure/Thy/export.scala
author wenzelm
Sun May 13 16:26:01 2018 +0200 (13 months ago)
changeset 68167 327bb0f5f768
parent 68166 021c6fecaf5c
child 68171 13162bb3a677
permissions -rw-r--r--
clarified implicit compression;
     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 
    91   def make_regex(pattern: String): Regex =
    92   {
    93     @tailrec def make(result: List[String], depth: Int, chs: List[Char]): Regex =
    94       chs match {
    95         case '*' :: '*' :: rest => make("[^:]*" :: result, depth, rest)
    96         case '*' :: rest => make("[^:/]*" :: result, depth, rest)
    97         case '?' :: rest => make("[^:/]" :: result, depth, rest)
    98         case '\\' :: c :: rest => make(("\\" + c) :: result, depth, rest)
    99         case '{' :: rest => make("(" :: result, depth + 1, rest)
   100         case ',' :: rest if depth > 0 => make("|" :: result, depth, rest)
   101         case '}' :: rest if depth > 0 => make(")" :: result, depth - 1, rest)
   102         case c :: rest if ".+()".contains(c) => make(("\\" + c) :: result, depth, rest)
   103         case c :: rest => make(c.toString :: result, depth, rest)
   104         case Nil => result.reverse.mkString.r
   105       }
   106     make(Nil, 0, pattern.toList)
   107   }
   108 
   109   def make_matcher(pattern: String): (String, String) => Boolean =
   110   {
   111     val regex = make_regex(pattern)
   112     (theory_name: String, name: String) =>
   113       regex.pattern.matcher(compound_name(theory_name, name)).matches
   114   }
   115 
   116   def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes,
   117     cache: XZ.Cache = XZ.cache()): Entry =
   118   {
   119     Entry(session_name, args.theory_name, args.name,
   120       if (args.compress) Future.fork(body.maybe_compress(cache = cache))
   121       else Future.value((false, body)))
   122   }
   123 
   124   def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String): Entry =
   125   {
   126     val select =
   127       Data.table.select(List(Data.compressed, Data.body),
   128         Data.where_equal(session_name, theory_name, name))
   129     db.using_statement(select)(stmt =>
   130     {
   131       val res = stmt.execute_query()
   132       if (res.next()) {
   133         val compressed = res.bool(Data.compressed)
   134         val body = res.bytes(Data.body)
   135         Entry(session_name, theory_name, name, Future.value(compressed, body))
   136       }
   137       else error(message("Bad export", theory_name, name))
   138     })
   139   }
   140 
   141 
   142   /* database consumer thread */
   143 
   144   def consumer(db: SQL.Database): Consumer = new Consumer(db)
   145 
   146   class Consumer private[Export](db: SQL.Database)
   147   {
   148     val xz_cache = XZ.make_cache()
   149 
   150     db.create_table(Data.table)
   151 
   152     private val export_errors = Synchronized[List[String]](Nil)
   153 
   154     private val consumer =
   155       Consumer_Thread.fork(name = "export")(consume = (entry: Entry) =>
   156         {
   157           entry.body.join
   158           db.transaction {
   159             if (read_name(db, entry.session_name, entry.theory_name, entry.name)) {
   160               val err = message("Duplicate export", entry.theory_name, entry.name)
   161               export_errors.change(errs => err :: errs)
   162             }
   163             else entry.write(db)
   164           }
   165           true
   166         })
   167 
   168     def apply(session_name: String, args: Markup.Export.Args, body: Bytes): Unit =
   169       consumer.send(make_entry(session_name, args, body, cache = xz_cache))
   170 
   171     def shutdown(close: Boolean = false): List[String] =
   172     {
   173       consumer.shutdown()
   174       if (close) db.close()
   175       export_errors.value.reverse
   176     }
   177   }
   178 
   179 
   180   /* Isabelle tool wrapper */
   181 
   182   val default_export_dir = Path.explode("export")
   183 
   184   val isabelle_tool = Isabelle_Tool("export", "retrieve theory exports", args =>
   185   {
   186     /* arguments */
   187 
   188     var export_dir = default_export_dir
   189     var dirs: List[Path] = Nil
   190     var export_list = false
   191     var no_build = false
   192     var options = Options.init()
   193     var system_mode = false
   194     var export_pattern = ""
   195 
   196     val getopts = Getopts("""
   197 Usage: isabelle export [OPTIONS] SESSION
   198 
   199   Options are:
   200     -D DIR       target directory for exported files (default: """ + default_export_dir + """)
   201     -d DIR       include session directory
   202     -l           list exports
   203     -n           no build of session
   204     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   205     -s           system build mode for session image
   206     -x PATTERN   extract files matching pattern (e.g. "*:**" for all)
   207 
   208   List or export theory exports for SESSION: named blobs produced by
   209   isabelle build. Option -l or -x is required.
   210 
   211   The PATTERN language resembles glob patterns in the shell, with ? and *
   212   (both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc],
   213   and variants {pattern1,pattern2,pattern3}.
   214 """,
   215       "D:" -> (arg => export_dir = Path.explode(arg)),
   216       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   217       "l" -> (_ => export_list = true),
   218       "n" -> (_ => no_build = true),
   219       "o:" -> (arg => options = options + arg),
   220       "s" -> (_ => system_mode = true),
   221       "x:" -> (arg => export_pattern = arg))
   222 
   223     val more_args = getopts(args)
   224     val session_name =
   225       more_args match {
   226         case List(session_name) if export_list || export_pattern != "" => session_name
   227         case _ => getopts.usage()
   228       }
   229 
   230 
   231     /* build */
   232 
   233     val progress = new Console_Progress()
   234 
   235     if (!no_build &&
   236         !Build.build(options, no_build = true, dirs = dirs, system_mode = system_mode,
   237           sessions = List(session_name)).ok)
   238     {
   239       progress.echo("Build started for Isabelle/" + session_name + " ...")
   240       progress.interrupt_handler {
   241         val res =
   242           Build.build(options, progress = progress, dirs = dirs, system_mode = system_mode,
   243             sessions = List(session_name))
   244         if (!res.ok) sys.exit(res.rc)
   245       }
   246     }
   247 
   248 
   249     /* database */
   250 
   251     val store = Sessions.store(system_mode)
   252     val database =
   253       store.find_database(session_name) match {
   254         case None => error("Missing database for session " + quote(session_name))
   255         case Some(database) => database
   256       }
   257 
   258     using(SQLite.open_database(database))(db =>
   259     {
   260       db.transaction {
   261         val export_names = read_theory_names(db, session_name)
   262 
   263         // list
   264         if (export_list) {
   265           (for ((theory_name, name) <- export_names) yield compound_name(theory_name, name)).
   266             sorted.foreach(Output.writeln(_, stdout = true))
   267         }
   268 
   269         // export
   270         if (export_pattern != "") {
   271           val xz_cache = XZ.make_cache()
   272 
   273           val matcher = make_matcher(export_pattern)
   274           for { (theory_name, name) <- export_names if matcher(theory_name, name) }
   275           {
   276             val entry = read_entry(db, session_name, theory_name, name)
   277             val path = export_dir + Path.basic(theory_name) + Path.explode(name)
   278 
   279             progress.echo("exporting " + path)
   280             Isabelle_System.mkdirs(path.dir)
   281             Bytes.write(path, entry.uncompressed(cache = xz_cache))
   282           }
   283         }
   284       }
   285     })
   286   })
   287 }