1/* Title: Pure/Tools/dump.scala 2 Author: Makarius 3 4Dump cumulative PIDE session database. 5*/ 6 7package isabelle 8 9import java.io.{BufferedWriter, FileOutputStream, OutputStreamWriter} 10 11 12object Dump 13{ 14 /* aspects */ 15 16 sealed case class Aspect_Args( 17 options: Options, 18 deps: Sessions.Deps, 19 progress: Progress, 20 output_dir: Path, 21 snapshot: Document.Snapshot, 22 status: Document_Status.Node_Status) 23 { 24 def write_path(file_name: Path): Path = 25 { 26 val path = output_dir + Path.basic(snapshot.node_name.theory) + file_name 27 Isabelle_System.mkdirs(path.dir) 28 path 29 } 30 31 def write(file_name: Path, bytes: Bytes): Unit = 32 Bytes.write(write_path(file_name), bytes) 33 34 def write(file_name: Path, text: String): Unit = 35 write(file_name, Bytes(text)) 36 37 def write(file_name: Path, body: XML.Body): Unit = 38 using(File.writer(write_path(file_name).file))( 39 writer => YXML.traversal(s => writer.write(Symbol.encode(s)), body)) 40 } 41 42 sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit, 43 options: List[String] = Nil) 44 { 45 override def toString: String = name 46 } 47 48 val known_aspects: List[Aspect] = 49 List( 50 Aspect("markup", "PIDE markup (YXML format)", 51 { case args => 52 args.write(Path.explode("markup.yxml"), 53 args.snapshot.markup_to_XML(Text.Range.full, Markup.Elements.full)) 54 }), 55 Aspect("messages", "output messages (YXML format)", 56 { case args => 57 args.write(Path.explode("messages.yxml"), 58 args.snapshot.messages.iterator.map(_._1).toList) 59 }), 60 Aspect("latex", "generated LaTeX source", 61 { case args => 62 for (entry <- args.snapshot.exports if entry.name == "document.tex") 63 args.write(Path.explode(entry.name), entry.uncompressed()) 64 }, options = List("export_document")), 65 Aspect("theory", "foundational theory content", 66 { case args => 67 for { 68 entry <- args.snapshot.exports 69 if entry.name.startsWith(Export_Theory.export_prefix) 70 } args.write(Path.explode(entry.name), entry.uncompressed()) 71 }, options = List("export_theory")) 72 ).sortBy(_.name) 73 74 def show_aspects: String = 75 cat_lines(known_aspects.map(aspect => aspect.name + " - " + aspect.description)) 76 77 def the_aspect(name: String): Aspect = 78 known_aspects.find(aspect => aspect.name == name) getOrElse 79 error("Unknown aspect " + quote(name)) 80 81 82 /* context and session */ 83 84 sealed case class Args( 85 session: Headless.Session, 86 snapshot: Document.Snapshot, 87 status: Document_Status.Node_Status) 88 { 89 def print_node: String = snapshot.node_name.toString 90 } 91 92 object Context 93 { 94 def apply( 95 options: Options, 96 aspects: List[Aspect] = Nil, 97 progress: Progress = No_Progress, 98 dirs: List[Path] = Nil, 99 select_dirs: List[Path] = Nil, 100 selection: Sessions.Selection = Sessions.Selection.empty, 101 pure_base: Boolean = false, 102 skip_base: Boolean = false): Context = 103 { 104 val session_options: Options = 105 { 106 val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options 107 val options1 = 108 options0 + 109 "completion_limit=0" + 110 "ML_statistics=false" + 111 "parallel_proofs=0" + 112 "editor_tracing_messages=0" + 113 "editor_presentation" 114 (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) }) 115 } 116 117 val sessions_structure: Sessions.Structure = 118 Sessions.load_structure(session_options, dirs = dirs, select_dirs = select_dirs). 119 selection(selection) 120 121 { 122 val selection_size = sessions_structure.build_graph.size 123 if (selection_size > 1) progress.echo("Loading " + selection_size + " sessions ...") 124 } 125 126 val deps: Sessions.Deps = 127 Sessions.deps(sessions_structure, progress = progress).check_errors 128 129 new Context(options, progress, dirs, select_dirs, pure_base, skip_base, session_options, deps) 130 } 131 } 132 133 class Context private( 134 val options: Options, 135 val progress: Progress, 136 val dirs: List[Path], 137 val select_dirs: List[Path], 138 val pure_base: Boolean, 139 val skip_base: Boolean, 140 val session_options: Options, 141 val deps: Sessions.Deps) 142 { 143 context => 144 145 def session_dirs: List[Path] = dirs ::: select_dirs 146 147 def build_logic(logic: String) 148 { 149 Build.build_logic(options, logic, build_heap = true, progress = progress, 150 dirs = session_dirs, strict = true) 151 } 152 153 def sessions( 154 logic: String = default_logic, 155 log: Logger = No_Logger): List[Session] = 156 { 157 /* partitions */ 158 159 def session_info(session_name: String): Sessions.Info = 160 deps.sessions_structure(session_name) 161 162 val session_graph = deps.sessions_structure.build_graph 163 val all_sessions = session_graph.topological_order 164 165 val afp_sessions = 166 (for (name <- all_sessions if session_info(name).is_afp) yield name).toSet 167 168 val afp_bulky_sessions = 169 (for (name <- all_sessions if session_info(name).is_afp_bulky) yield name).toList 170 171 val base_sessions = 172 session_graph.all_preds(List(logic).filter(session_graph.defined)).reverse 173 174 val proof_sessions = 175 session_graph.all_succs( 176 for (name <- all_sessions if session_info(name).record_proofs) yield name) 177 178 179 /* resulting sessions */ 180 181 def make_session( 182 selected_sessions: List[String], 183 session_logic: String = logic, 184 strict: Boolean = false, 185 record_proofs: Boolean = false): List[Session] = 186 { 187 if (selected_sessions.isEmpty && !strict) Nil 188 else List(new Session(context, session_logic, log, selected_sessions, record_proofs)) 189 } 190 191 val PURE = isabelle.Thy_Header.PURE 192 193 val base = 194 if ((logic == PURE && !pure_base) || skip_base) Nil 195 else make_session(base_sessions, session_logic = PURE, strict = logic == PURE) 196 197 val main = 198 make_session( 199 session_graph.topological_order.filterNot(name => 200 afp_sessions.contains(name) || 201 base_sessions.contains(name) || 202 proof_sessions.contains(name))) 203 204 val proofs = make_session(proof_sessions, session_logic = PURE, record_proofs = true) 205 206 val afp = 207 if (afp_sessions.isEmpty) Nil 208 else { 209 val (part1, part2) = 210 { 211 val graph = session_graph.restrict(afp_sessions -- afp_bulky_sessions) 212 val force_partition1 = AFP.force_partition1.filter(graph.defined) 213 val force_part1 = graph.all_preds(graph.all_succs(force_partition1)).toSet 214 graph.keys.partition(a => force_part1(a) || graph.is_isolated(a)) 215 } 216 List(part1, part2, afp_bulky_sessions).flatMap(make_session(_)) 217 } 218 219 proofs ::: base ::: main ::: afp 220 } 221 222 223 /* processed theories */ 224 225 private val processed_theories = Synchronized(Set.empty[String]) 226 227 def process_theory(theory: String): Boolean = 228 processed_theories.change_result(processed => (!processed(theory), processed + theory)) 229 230 231 /* errors */ 232 233 private val errors = Synchronized(List.empty[String]) 234 235 def add_errors(more_errs: List[String]) 236 { 237 errors.change(errs => errs ::: more_errs) 238 } 239 240 def check_errors 241 { 242 val errs = errors.value 243 if (errs.nonEmpty) error(errs.mkString("\n\n")) 244 } 245 } 246 247 class Session private[Dump]( 248 val context: Context, 249 val logic: String, 250 log: Logger, 251 selected_sessions: List[String], 252 record_proofs: Boolean) 253 { 254 /* resources */ 255 256 val options: Options = 257 if (record_proofs) context.session_options + "record_proofs=2" 258 else context.session_options 259 260 private def deps = context.deps 261 private def progress = context.progress 262 263 val resources: Headless.Resources = 264 Headless.Resources.make(options, logic, progress = progress, log = log, 265 session_dirs = context.session_dirs, 266 include_sessions = deps.sessions_structure.imports_topological_order) 267 268 val used_theories: List[Document.Node.Name] = 269 { 270 for { 271 session_name <- 272 deps.sessions_structure.build_graph.restrict(selected_sessions.toSet).topological_order 273 (name, theory_options) <- deps(session_name).used_theories 274 if !resources.session_base.loaded_theory(name.theory) 275 if { 276 def warn(msg: String): Unit = 277 progress.echo_warning("Skipping theory " + name + " (" + msg + ")") 278 279 val conditions = 280 space_explode(',', theory_options.string("condition")). 281 filter(cond => Isabelle_System.getenv(cond) == "") 282 if (conditions.nonEmpty) { 283 warn("undefined " + conditions.mkString(", ")) 284 false 285 } 286 else if (options.bool("skip_proofs") && !theory_options.bool("skip_proofs")) { 287 warn("option skip_proofs") 288 false 289 } 290 else true 291 } 292 } yield name 293 } 294 295 296 /* process */ 297 298 def process(process_theory: Args => Unit, unicode_symbols: Boolean = false) 299 { 300 val session = resources.start_session(progress = progress) 301 302 303 // asynchronous consumer 304 305 object Consumer 306 { 307 sealed case class Bad_Theory( 308 name: Document.Node.Name, 309 status: Document_Status.Node_Status, 310 errors: List[String]) 311 312 private val consumer_bad_theories = Synchronized(List.empty[Bad_Theory]) 313 314 private val consumer = 315 Consumer_Thread.fork(name = "dump")( 316 consume = (args: (Document.Snapshot, Document_Status.Node_Status)) => 317 { 318 val (snapshot, status) = args 319 val name = snapshot.node_name 320 if (status.ok) { 321 try { 322 if (context.process_theory(name.theory)) { 323 process_theory(Args(session, snapshot, status)) 324 } 325 } 326 catch { 327 case exn: Throwable if !Exn.is_interrupt(exn) => 328 val msg = Exn.message(exn) 329 progress.echo("FAILED to process theory " + name) 330 progress.echo_error_message(msg) 331 consumer_bad_theories.change(Bad_Theory(name, status, List(msg)) :: _) 332 } 333 } 334 else { 335 val msgs = 336 for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree)) 337 yield { 338 "Error" + Position.here(pos) + ":\n" + 339 XML.content(Pretty.formatted(List(tree))) 340 } 341 progress.echo("FAILED to process theory " + name) 342 msgs.foreach(progress.echo_error_message) 343 consumer_bad_theories.change(Bad_Theory(name, status, msgs) :: _) 344 } 345 true 346 }) 347 348 def apply(snapshot: Document.Snapshot, status: Document_Status.Node_Status): Unit = 349 consumer.send((snapshot, status)) 350 351 def shutdown(): List[Bad_Theory] = 352 { 353 consumer.shutdown() 354 consumer_bad_theories.value.reverse 355 } 356 } 357 358 359 // synchronous body 360 361 try { 362 val use_theories_result = 363 session.use_theories(used_theories.map(_.theory), 364 unicode_symbols = unicode_symbols, 365 progress = progress, 366 commit = Some(Consumer.apply _)) 367 368 val bad_theories = Consumer.shutdown() 369 val bad_msgs = 370 bad_theories.map(bad => 371 Output.clean_yxml( 372 "FAILED theory " + bad.name + 373 (if (bad.status.consolidated) "" else ": " + bad.status.percentage + "% finished") + 374 (if (bad.errors.isEmpty) "" else bad.errors.mkString("\n", "\n", "")))) 375 376 val pending_msgs = 377 use_theories_result.nodes_pending match { 378 case Nil => Nil 379 case pending => List("Pending theories: " + commas(pending.map(p => p._1.toString))) 380 } 381 382 context.add_errors(bad_msgs ::: pending_msgs) 383 } 384 finally { session.stop() } 385 } 386 } 387 388 389 /* dump */ 390 391 val default_output_dir: Path = Path.explode("dump") 392 val default_logic: String = Thy_Header.PURE 393 394 def dump( 395 options: Options, 396 logic: String, 397 aspects: List[Aspect] = Nil, 398 progress: Progress = No_Progress, 399 log: Logger = No_Logger, 400 dirs: List[Path] = Nil, 401 select_dirs: List[Path] = Nil, 402 output_dir: Path = default_output_dir, 403 selection: Sessions.Selection = Sessions.Selection.empty) 404 { 405 val context = 406 Context(options, aspects = aspects, progress = progress, dirs = dirs, 407 select_dirs = select_dirs, selection = selection) 408 409 context.build_logic(logic) 410 411 for (session <- context.sessions(logic = logic, log = log)) { 412 session.process((args: Args) => 413 { 414 progress.echo("Processing theory " + args.print_node + " ...") 415 val aspect_args = 416 Aspect_Args(session.options, context.deps, progress, output_dir, 417 args.snapshot, args.status) 418 aspects.foreach(_.operation(aspect_args)) 419 }) 420 } 421 422 context.check_errors 423 } 424 425 426 /* Isabelle tool wrapper */ 427 428 val isabelle_tool = 429 Isabelle_Tool("dump", "dump cumulative PIDE session database", args => 430 { 431 var aspects: List[Aspect] = known_aspects 432 var base_sessions: List[String] = Nil 433 var select_dirs: List[Path] = Nil 434 var output_dir = default_output_dir 435 var requirements = false 436 var exclude_session_groups: List[String] = Nil 437 var all_sessions = false 438 var logic = default_logic 439 var dirs: List[Path] = Nil 440 var session_groups: List[String] = Nil 441 var options = Options.init() 442 var verbose = false 443 var exclude_sessions: List[String] = Nil 444 445 val getopts = Getopts(""" 446Usage: isabelle dump [OPTIONS] [SESSIONS ...] 447 448 Options are: 449 -A NAMES dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """) 450 -B NAME include session NAME and all descendants 451 -D DIR include session directory and select its sessions 452 -O DIR output directory for dumped files (default: """ + default_output_dir + """) 453 -R operate on requirements of selected sessions 454 -X NAME exclude sessions from group NAME and all descendants 455 -a select all sessions 456 -b NAME base logic image (default """ + isabelle.quote(default_logic) + """) 457 -d DIR include session directory 458 -g NAME select session group NAME 459 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) 460 -v verbose 461 -x NAME exclude session NAME and all descendants 462 463 Dump cumulative PIDE session database, with the following aspects: 464 465""" + Library.prefix_lines(" ", show_aspects) + "\n", 466 "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))), 467 "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), 468 "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), 469 "O:" -> (arg => output_dir = Path.explode(arg)), 470 "R" -> (_ => requirements = true), 471 "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), 472 "a" -> (_ => all_sessions = true), 473 "b:" -> (arg => logic = arg), 474 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), 475 "g:" -> (arg => session_groups = session_groups ::: List(arg)), 476 "o:" -> (arg => options = options + arg), 477 "v" -> (_ => verbose = true), 478 "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) 479 480 val sessions = getopts(args) 481 482 val progress = new Console_Progress(verbose = verbose) 483 484 val start_date = Date.now() 485 486 if (verbose) progress.echo("Started at " + Build_Log.print_date(start_date)) 487 488 progress.interrupt_handler { 489 dump(options, logic, 490 aspects = aspects, 491 progress = progress, 492 dirs = dirs, 493 select_dirs = select_dirs, 494 output_dir = output_dir, 495 selection = Sessions.Selection( 496 requirements = requirements, 497 all_sessions = all_sessions, 498 base_sessions = base_sessions, 499 exclude_session_groups = exclude_session_groups, 500 exclude_sessions = exclude_sessions, 501 session_groups = session_groups, 502 sessions = sessions)) 503 } 504 505 val end_date = Date.now() 506 val timing = end_date.time - start_date.time 507 508 if (verbose) progress.echo("\nFinished at " + Build_Log.print_date(end_date)) 509 progress.echo(timing.message_hms + " elapsed time") 510 }) 511} 512