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