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