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 /* 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 154 /* database consumer thread */ 155 156 def consumer(db: SQL.Database, cache: XZ.Cache = XZ.cache()): Consumer = new Consumer(db, cache) 157 158 class Consumer private[Export](db: SQL.Database, cache: XZ.Cache) 159 { 160 private val export_errors = Synchronized[List[String]](Nil) 161 162 private val consumer = 163 Consumer_Thread.fork(name = "export")(consume = (entry: Entry) => 164 { 165 entry.body.join 166 db.transaction { 167 if (read_name(db, entry.session_name, entry.theory_name, entry.name)) { 168 val err = message("Duplicate export", entry.theory_name, entry.name) 169 export_errors.change(errs => err :: errs) 170 } 171 else entry.write(db) 172 } 173 true 174 }) 175 176 def apply(session_name: String, args: Markup.Export.Args, body: Bytes): Unit = 177 consumer.send(make_entry(session_name, args, body, cache = cache)) 178 179 def shutdown(close: Boolean = false): List[String] = 180 { 181 consumer.shutdown() 182 if (close) db.close() 183 export_errors.value.reverse 184 } 185 } 186 187 188 /* abstract provider */ 189 190 object Provider 191 { 192 def database(db: SQL.Database, session_name: String, theory_name: String): Provider = 193 new Provider { 194 def apply(export_name: String): Option[Entry] = 195 read_entry(db, session_name, theory_name, export_name) 196 } 197 198 def snapshot(snapshot: Document.Snapshot): Provider = 199 new Provider { 200 def apply(export_name: String): Option[Entry] = 201 snapshot.exports_map.get(export_name) 202 } 203 } 204 205 trait Provider 206 { 207 def apply(export_name: String): Option[Entry] 208 209 def uncompressed_yxml(export_name: String, cache: XZ.Cache = XZ.cache()): XML.Body = 210 apply(export_name) match { 211 case Some(entry) => entry.uncompressed_yxml(cache = cache) 212 case None => Nil 213 } 214 } 215 216 217 /* export to file-system */ 218 219 def export_files( 220 store: Sessions.Store, 221 session_name: String, 222 export_dir: Path, 223 progress: Progress = No_Progress, 224 export_list: Boolean = false, 225 export_patterns: List[String] = Nil, 226 export_prefix: String = "") 227 { 228 using(store.open_database(session_name))(db => 229 { 230 db.transaction { 231 val export_names = read_theory_exports(db, session_name) 232 233 // list 234 if (export_list) { 235 (for ((theory_name, name) <- export_names) yield compound_name(theory_name, name)). 236 sorted.foreach(progress.echo(_)) 237 } 238 239 // export 240 if (export_patterns.nonEmpty) { 241 val exports = 242 (for { 243 export_pattern <- export_patterns.iterator 244 matcher = make_matcher(export_pattern) 245 (theory_name, name) <- export_names if matcher(theory_name, name) 246 } yield (theory_name, name)).toSet 247 for { 248 (theory_name, group) <- exports.toList.groupBy(_._1).toList.sortBy(_._1) 249 name <- group.map(_._2).sorted 250 entry <- read_entry(db, session_name, theory_name, name) 251 } { 252 val path = export_dir + Path.basic(theory_name) + Path.explode(name) 253 progress.echo(export_prefix + "export " + path) 254 Isabelle_System.mkdirs(path.dir) 255 Bytes.write(path, entry.uncompressed(cache = store.xz_cache)) 256 } 257 } 258 } 259 }) 260 } 261 262 263 /* Isabelle tool wrapper */ 264 265 val default_export_dir = Path.explode("export") 266 267 val isabelle_tool = Isabelle_Tool("export", "retrieve theory exports", args => 268 { 269 /* arguments */ 270 271 var export_dir = default_export_dir 272 var dirs: List[Path] = Nil 273 var export_list = false 274 var no_build = false 275 var options = Options.init() 276 var system_mode = false 277 var export_patterns: List[String] = Nil 278 279 val getopts = Getopts(""" 280Usage: isabelle export [OPTIONS] SESSION 281 282 Options are: 283 -O DIR output directory for exported files (default: """ + default_export_dir + """) 284 -d DIR include session directory 285 -l list exports 286 -n no build of session 287 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) 288 -s system build mode for session image 289 -x PATTERN extract files matching pattern (e.g. "*:**" for all) 290 291 List or export theory exports for SESSION: named blobs produced by 292 isabelle build. Option -l or -x is required; option -x may be repeated. 293 294 The PATTERN language resembles glob patterns in the shell, with ? and * 295 (both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc], 296 and variants {pattern1,pattern2,pattern3}. 297""", 298 "O:" -> (arg => export_dir = Path.explode(arg)), 299 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), 300 "l" -> (_ => export_list = true), 301 "n" -> (_ => no_build = true), 302 "o:" -> (arg => options = options + arg), 303 "s" -> (_ => system_mode = true), 304 "x:" -> (arg => export_patterns ::= arg)) 305 306 val more_args = getopts(args) 307 val session_name = 308 more_args match { 309 case List(session_name) if export_list || export_patterns.nonEmpty => session_name 310 case _ => getopts.usage() 311 } 312 313 val progress = new Console_Progress() 314 315 316 /* build */ 317 318 if (!no_build) { 319 val rc = 320 progress.interrupt_handler { 321 Build.build_logic(options, session_name, progress = progress, 322 dirs = dirs, system_mode = system_mode) 323 } 324 if (rc != 0) sys.exit(rc) 325 } 326 327 328 /* export files */ 329 330 val store = Sessions.store(options, system_mode) 331 export_files(store, session_name, export_dir, progress = progress, 332 export_list = export_list, export_patterns = export_patterns) 333 }) 334} 335