1/* Title: Pure/Thy/export.scala 2 Author: Makarius 3 4Manage theory exports: compressed blobs. 5*/ 6 7package isabelle 8 9 10import scala.annotation.tailrec 11import scala.util.matching.Regex 12 13 14object 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 def compound_name: String = Export.compound_name(theory_name, name) 88 89 val name_elems: List[String] = explode_name(name) 90 91 def name_extends(elems: List[String]): Boolean = 92 name_elems.startsWith(elems) && name_elems != elems 93 94 def text: String = uncompressed().text 95 96 def uncompressed(cache: XZ.Cache = XZ.cache()): Bytes = 97 { 98 val (compressed, bytes) = body.join 99 if (compressed) bytes.uncompress(cache = cache) else bytes 100 } 101 102 def uncompressed_yxml(cache: XZ.Cache = XZ.cache()): XML.Body = 103 YXML.parse_body(UTF8.decode_permissive(uncompressed(cache = cache))) 104 105 def write(db: SQL.Database) 106 { 107 val (compressed, bytes) = body.join 108 db.using_statement(Data.table.insert())(stmt => 109 { 110 stmt.string(1) = session_name 111 stmt.string(2) = theory_name 112 stmt.string(3) = name 113 stmt.bool(4) = executable 114 stmt.bool(5) = compressed 115 stmt.bytes(6) = bytes 116 stmt.execute() 117 }) 118 } 119 } 120 121 def make_regex(pattern: String): Regex = 122 { 123 @tailrec def make(result: List[String], depth: Int, chs: List[Char]): Regex = 124 chs match { 125 case '*' :: '*' :: rest => make("[^:]*" :: result, depth, rest) 126 case '*' :: rest => make("[^:/]*" :: result, depth, rest) 127 case '?' :: rest => make("[^:/]" :: result, depth, rest) 128 case '\\' :: c :: rest => make(("\\" + c) :: result, depth, rest) 129 case '{' :: rest => make("(" :: result, depth + 1, rest) 130 case ',' :: rest if depth > 0 => make("|" :: result, depth, rest) 131 case '}' :: rest if depth > 0 => make(")" :: result, depth - 1, rest) 132 case c :: rest if ".+()".contains(c) => make(("\\" + c) :: result, depth, rest) 133 case c :: rest => make(c.toString :: result, depth, rest) 134 case Nil => result.reverse.mkString.r 135 } 136 make(Nil, 0, pattern.toList) 137 } 138 139 def make_matcher(pattern: String): (String, String) => Boolean = 140 { 141 val regex = make_regex(pattern) 142 (theory_name: String, name: String) => 143 regex.pattern.matcher(compound_name(theory_name, name)).matches 144 } 145 146 def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes, 147 cache: XZ.Cache = XZ.cache()): Entry = 148 { 149 Entry(session_name, args.theory_name, args.name, args.executable, 150 if (args.compress) Future.fork(body.maybe_compress(cache = cache)) 151 else Future.value((false, body))) 152 } 153 154 def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String) 155 : Option[Entry] = 156 { 157 val select = 158 Data.table.select(List(Data.executable, Data.compressed, Data.body), 159 Data.where_equal(session_name, theory_name, name)) 160 db.using_statement(select)(stmt => 161 { 162 val res = stmt.execute_query() 163 if (res.next()) { 164 val executable = res.bool(Data.executable) 165 val compressed = res.bool(Data.compressed) 166 val body = res.bytes(Data.body) 167 Some(Entry(session_name, theory_name, name, executable, Future.value(compressed, body))) 168 } 169 else None 170 }) 171 } 172 173 def read_entry(dir: Path, session_name: String, theory_name: String, name: String): Option[Entry] = 174 { 175 val path = dir + Path.basic(theory_name) + Path.explode(name) 176 if (path.is_file) { 177 val executable = File.is_executable(path) 178 val uncompressed = Bytes.read(path) 179 Some(Entry(session_name, theory_name, name, executable, Future.value((false, uncompressed)))) 180 } 181 else None 182 } 183 184 185 /* database consumer thread */ 186 187 def consumer(db: SQL.Database, cache: XZ.Cache = XZ.cache()): Consumer = new Consumer(db, cache) 188 189 class Consumer private[Export](db: SQL.Database, cache: XZ.Cache) 190 { 191 private val errors = Synchronized[List[String]](Nil) 192 193 private val consumer = 194 Consumer_Thread.fork_bulk[(Entry, Boolean)](name = "export")( 195 bulk = { case (entry, _) => entry.body.is_finished }, 196 consume = 197 (args: List[(Entry, Boolean)]) => 198 { 199 val results = 200 db.transaction { 201 for ((entry, strict) <- args) 202 yield { 203 if (read_name(db, entry.session_name, entry.theory_name, entry.name)) { 204 if (strict) { 205 val msg = message("Duplicate export", entry.theory_name, entry.name) 206 errors.change(msg :: _) 207 } 208 Exn.Res(()) 209 } 210 else Exn.capture { entry.write(db) } 211 } 212 } 213 (results, true) 214 }) 215 216 def apply(session_name: String, args: Markup.Export.Args, body: Bytes): Unit = 217 consumer.send(make_entry(session_name, args, body, cache = cache) -> args.strict) 218 219 def shutdown(close: Boolean = false): List[String] = 220 { 221 consumer.shutdown() 222 if (close) db.close() 223 errors.value.reverse 224 } 225 } 226 227 228 /* abstract provider */ 229 230 object Provider 231 { 232 def none: Provider = 233 new Provider { 234 def apply(export_name: String): Option[Entry] = None 235 def focus(other_theory: String): Provider = this 236 237 override def toString: String = "none" 238 } 239 240 def database(db: SQL.Database, session_name: String, theory_name: String): Provider = 241 new Provider { 242 def apply(export_name: String): Option[Entry] = 243 read_entry(db, session_name, theory_name, export_name) 244 245 def focus(other_theory: String): Provider = 246 if (other_theory == theory_name) this 247 else Provider.database(db, session_name, other_theory) 248 249 override def toString: String = db.toString 250 } 251 252 def snapshot(snapshot: Document.Snapshot): Provider = 253 new Provider { 254 def apply(export_name: String): Option[Entry] = 255 snapshot.exports_map.get(export_name) 256 257 def focus(other_theory: String): Provider = 258 if (other_theory == snapshot.node_name.theory) this 259 else { 260 val node_name = 261 snapshot.version.nodes.theory_name(other_theory) getOrElse 262 error("Bad theory " + quote(other_theory)) 263 Provider.snapshot(snapshot.state.snapshot(node_name)) 264 } 265 266 override def toString: String = snapshot.toString 267 } 268 269 def directory(dir: Path, session_name: String, theory_name: String): Provider = 270 new Provider { 271 def apply(export_name: String): Option[Entry] = 272 read_entry(dir, session_name, theory_name, export_name) 273 274 def focus(other_theory: String): Provider = 275 if (other_theory == theory_name) this 276 else Provider.directory(dir, session_name, other_theory) 277 278 override def toString: String = dir.toString 279 } 280 } 281 282 trait Provider 283 { 284 def apply(export_name: String): Option[Entry] 285 286 def uncompressed_yxml(export_name: String, cache: XZ.Cache = XZ.cache()): XML.Body = 287 apply(export_name) match { 288 case Some(entry) => entry.uncompressed_yxml(cache = cache) 289 case None => Nil 290 } 291 292 def focus(other_theory: String): Provider 293 } 294 295 296 /* export to file-system */ 297 298 def export_files( 299 store: Sessions.Store, 300 session_name: String, 301 export_dir: Path, 302 progress: Progress = No_Progress, 303 export_prune: Int = 0, 304 export_list: Boolean = false, 305 export_patterns: List[String] = Nil) 306 { 307 using(store.open_database(session_name))(db => 308 { 309 db.transaction { 310 val export_names = read_theory_exports(db, session_name) 311 312 // list 313 if (export_list) { 314 (for ((theory_name, name) <- export_names) yield compound_name(theory_name, name)). 315 sorted.foreach(progress.echo(_)) 316 } 317 318 // export 319 if (export_patterns.nonEmpty) { 320 val exports = 321 (for { 322 export_pattern <- export_patterns.iterator 323 matcher = make_matcher(export_pattern) 324 (theory_name, name) <- export_names if matcher(theory_name, name) 325 } yield (theory_name, name)).toSet 326 for { 327 (theory_name, group) <- exports.toList.groupBy(_._1).toList.sortBy(_._1) 328 name <- group.map(_._2).sorted 329 entry <- read_entry(db, session_name, theory_name, name) 330 } { 331 val elems = theory_name :: space_explode('/', name) 332 val path = 333 if (elems.length < export_prune + 1) { 334 error("Cannot prune path by " + export_prune + " element(s): " + Path.make(elems)) 335 } 336 else export_dir + Path.make(elems.drop(export_prune)) 337 338 progress.echo("export " + path + (if (entry.executable) " (executable)" else "")) 339 Isabelle_System.mkdirs(path.dir) 340 Bytes.write(path, entry.uncompressed(cache = store.xz_cache)) 341 File.set_executable(path, entry.executable) 342 } 343 } 344 } 345 }) 346 } 347 348 349 /* Isabelle tool wrapper */ 350 351 val default_export_dir = Path.explode("export") 352 353 val isabelle_tool = Isabelle_Tool("export", "retrieve theory exports", args => 354 { 355 /* arguments */ 356 357 var export_dir = default_export_dir 358 var dirs: List[Path] = Nil 359 var export_list = false 360 var no_build = false 361 var options = Options.init() 362 var export_prune = 0 363 var export_patterns: List[String] = Nil 364 365 val getopts = Getopts(""" 366Usage: isabelle export [OPTIONS] SESSION 367 368 Options are: 369 -O DIR output directory for exported files (default: """ + default_export_dir + """) 370 -d DIR include session directory 371 -l list exports 372 -n no build of session 373 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) 374 -p NUM prune path of exported files by NUM elements 375 -x PATTERN extract files matching pattern (e.g. "*:**" for all) 376 377 List or export theory exports for SESSION: named blobs produced by 378 isabelle build. Option -l or -x is required; option -x may be repeated. 379 380 The PATTERN language resembles glob patterns in the shell, with ? and * 381 (both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc], 382 and variants {pattern1,pattern2,pattern3}. 383""", 384 "O:" -> (arg => export_dir = Path.explode(arg)), 385 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), 386 "l" -> (_ => export_list = true), 387 "n" -> (_ => no_build = true), 388 "o:" -> (arg => options = options + arg), 389 "p:" -> (arg => export_prune = Value.Int.parse(arg)), 390 "x:" -> (arg => export_patterns ::= arg)) 391 392 val more_args = getopts(args) 393 val session_name = 394 more_args match { 395 case List(session_name) if export_list || export_patterns.nonEmpty => session_name 396 case _ => getopts.usage() 397 } 398 399 val progress = new Console_Progress() 400 401 402 /* build */ 403 404 if (!no_build) { 405 val rc = 406 progress.interrupt_handler { 407 Build.build_logic(options, session_name, progress = progress, dirs = dirs) 408 } 409 if (rc != 0) sys.exit(rc) 410 } 411 412 413 /* export files */ 414 415 val store = Sessions.store(options) 416 export_files(store, session_name, export_dir, progress = progress, export_prune = export_prune, 417 export_list = export_list, export_patterns = export_patterns) 418 }) 419} 420