diff --git a/src/Pure/Thy/export.scala b/src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala +++ b/src/Pure/Thy/export.scala @@ -1,440 +1,441 @@ /* Title: Pure/Thy/export.scala Author: Makarius Manage theory exports: compressed blobs. */ package isabelle import scala.annotation.tailrec import scala.util.matching.Regex object Export { /* artefact names */ val MARKUP = "PIDE/markup" val MESSAGES = "PIDE/messages" val DOCUMENT_PREFIX = "document/" + val CITATIONS = DOCUMENT_PREFIX + "citations" val THEORY_PREFIX: String = "theory/" val PROOFS_PREFIX: String = "proofs/" def explode_name(s: String): List[String] = space_explode('/', s) def implode_name(elems: Iterable[String]): String = elems.mkString("/") /* SQL data model */ object Data { val session_name = SQL.Column.string("session_name").make_primary_key val theory_name = SQL.Column.string("theory_name").make_primary_key val name = SQL.Column.string("name").make_primary_key val executable = SQL.Column.bool("executable") val compressed = SQL.Column.bool("compressed") val body = SQL.Column.bytes("body") val table = SQL.Table("isabelle_exports", List(session_name, theory_name, name, executable, compressed, body)) def where_equal(session_name: String, theory_name: String = "", name: String = ""): SQL.Source = "WHERE " + Data.session_name.equal(session_name) + (if (theory_name == "") "" else " AND " + Data.theory_name.equal(theory_name)) + (if (name == "") "" else " AND " + Data.name.equal(name)) } def read_name(db: SQL.Database, session_name: String, theory_name: String, name: String): Boolean = { val select = Data.table.select(List(Data.name), Data.where_equal(session_name, theory_name, name)) db.using_statement(select)(stmt => stmt.execute_query().next()) } def read_names(db: SQL.Database, session_name: String, theory_name: String): List[String] = { val select = Data.table.select(List(Data.name), Data.where_equal(session_name, theory_name)) db.using_statement(select)(stmt => stmt.execute_query().iterator(res => res.string(Data.name)).toList) } def read_theory_names(db: SQL.Database, session_name: String): List[String] = { val select = Data.table.select(List(Data.theory_name), Data.where_equal(session_name), distinct = true) db.using_statement(select)(stmt => stmt.execute_query().iterator(_.string(Data.theory_name)).toList) } def read_theory_exports(db: SQL.Database, session_name: String): List[(String, String)] = { val select = Data.table.select(List(Data.theory_name, Data.name), Data.where_equal(session_name)) db.using_statement(select)(stmt => stmt.execute_query().iterator(res => (res.string(Data.theory_name), res.string(Data.name))).toList) } def message(msg: String, theory_name: String, name: String): String = msg + " " + quote(name) + " for theory " + quote(theory_name) def compound_name(a: String, b: String): String = a + ":" + b def empty_entry(session_name: String, theory_name: String, name: String): Entry = Entry(session_name, theory_name, name, false, Future.value(false, Bytes.empty)) sealed case class Entry( session_name: String, theory_name: String, name: String, executable: Boolean, body: Future[(Boolean, Bytes)]) { override def toString: String = name def compound_name: String = Export.compound_name(theory_name, name) def name_has_prefix(s: String): Boolean = name.startsWith(s) val name_elems: List[String] = explode_name(name) def name_extends(elems: List[String]): Boolean = name_elems.startsWith(elems) && name_elems != elems def text: String = uncompressed().text def uncompressed(cache: XZ.Cache = XZ.cache()): Bytes = { val (compressed, bytes) = body.join if (compressed) bytes.uncompress(cache = cache) else bytes } def uncompressed_yxml(cache: XZ.Cache = XZ.cache()): XML.Body = YXML.parse_body(UTF8.decode_permissive(uncompressed(cache = cache))) def write(db: SQL.Database) { val (compressed, bytes) = body.join db.using_statement(Data.table.insert())(stmt => { stmt.string(1) = session_name stmt.string(2) = theory_name stmt.string(3) = name stmt.bool(4) = executable stmt.bool(5) = compressed stmt.bytes(6) = bytes stmt.execute() }) } } def make_regex(pattern: String): Regex = { @tailrec def make(result: List[String], depth: Int, chs: List[Char]): Regex = chs match { case '*' :: '*' :: rest => make("[^:]*" :: result, depth, rest) case '*' :: rest => make("[^:/]*" :: result, depth, rest) case '?' :: rest => make("[^:/]" :: result, depth, rest) case '\\' :: c :: rest => make(("\\" + c) :: result, depth, rest) case '{' :: rest => make("(" :: result, depth + 1, rest) case ',' :: rest if depth > 0 => make("|" :: result, depth, rest) case '}' :: rest if depth > 0 => make(")" :: result, depth - 1, rest) case c :: rest if ".+()".contains(c) => make(("\\" + c) :: result, depth, rest) case c :: rest => make(c.toString :: result, depth, rest) case Nil => result.reverse.mkString.r } make(Nil, 0, pattern.toList) } def make_matcher(pattern: String): (String, String) => Boolean = { val regex = make_regex(pattern) (theory_name: String, name: String) => regex.pattern.matcher(compound_name(theory_name, name)).matches } def make_entry(session_name: String, args: Protocol.Export.Args, body: Bytes, cache: XZ.Cache = XZ.cache()): Entry = { Entry(session_name, args.theory_name, args.name, args.executable, if (args.compress) Future.fork(body.maybe_compress(cache = cache)) else Future.value((false, body))) } def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String) : Option[Entry] = { val select = Data.table.select(List(Data.executable, Data.compressed, Data.body), Data.where_equal(session_name, theory_name, name)) db.using_statement(select)(stmt => { val res = stmt.execute_query() if (res.next()) { val executable = res.bool(Data.executable) val compressed = res.bool(Data.compressed) val body = res.bytes(Data.body) Some(Entry(session_name, theory_name, name, executable, Future.value(compressed, body))) } else None }) } def read_entry(dir: Path, session_name: String, theory_name: String, name: String): Option[Entry] = { val path = dir + Path.basic(theory_name) + Path.explode(name) if (path.is_file) { val executable = File.is_executable(path) val uncompressed = Bytes.read(path) Some(Entry(session_name, theory_name, name, executable, Future.value((false, uncompressed)))) } else None } /* database consumer thread */ def consumer(db: SQL.Database, cache: XZ.Cache = XZ.cache()): Consumer = new Consumer(db, cache) class Consumer private[Export](db: SQL.Database, cache: XZ.Cache) { private val errors = Synchronized[List[String]](Nil) private val consumer = Consumer_Thread.fork_bulk[(Entry, Boolean)](name = "export")( bulk = { case (entry, _) => entry.body.is_finished }, consume = (args: List[(Entry, Boolean)]) => { val results = db.transaction { for ((entry, strict) <- args) yield { if (read_name(db, entry.session_name, entry.theory_name, entry.name)) { if (strict) { val msg = message("Duplicate export", entry.theory_name, entry.name) errors.change(msg :: _) } Exn.Res(()) } else Exn.capture { entry.write(db) } } } (results, true) }) def apply(session_name: String, args: Protocol.Export.Args, body: Bytes): Unit = consumer.send(make_entry(session_name, args, body, cache = cache) -> args.strict) def shutdown(close: Boolean = false): List[String] = { consumer.shutdown() if (close) db.close() errors.value.reverse } } /* abstract provider */ object Provider { def none: Provider = new Provider { def apply(export_name: String): Option[Entry] = None def focus(other_theory: String): Provider = this override def toString: String = "none" } def database_context( context: Sessions.Database_Context, session: String, theory_name: String): Provider = new Provider { def apply(export_name: String): Option[Entry] = context.read_export(session, theory_name, export_name) def focus(other_theory: String): Provider = this override def toString: String = context.toString } def database(db: SQL.Database, session_name: String, theory_name: String): Provider = new Provider { def apply(export_name: String): Option[Entry] = read_entry(db, session_name, theory_name, export_name) def focus(other_theory: String): Provider = if (other_theory == theory_name) this else Provider.database(db, session_name, other_theory) override def toString: String = db.toString } def snapshot(snapshot: Document.Snapshot): Provider = new Provider { def apply(export_name: String): Option[Entry] = snapshot.exports_map.get(export_name) def focus(other_theory: String): Provider = if (other_theory == snapshot.node_name.theory) this else { val node_name = snapshot.version.nodes.theory_name(other_theory) getOrElse error("Bad theory " + quote(other_theory)) Provider.snapshot(snapshot.state.snapshot(node_name)) } override def toString: String = snapshot.toString } def directory(dir: Path, session_name: String, theory_name: String): Provider = new Provider { def apply(export_name: String): Option[Entry] = read_entry(dir, session_name, theory_name, export_name) def focus(other_theory: String): Provider = if (other_theory == theory_name) this else Provider.directory(dir, session_name, other_theory) override def toString: String = dir.toString } } trait Provider { def apply(export_name: String): Option[Entry] def uncompressed_yxml(export_name: String, cache: XZ.Cache = XZ.cache()): XML.Body = apply(export_name) match { case Some(entry) => entry.uncompressed_yxml(cache = cache) case None => Nil } def focus(other_theory: String): Provider } /* export to file-system */ def export_files( store: Sessions.Store, session_name: String, export_dir: Path, progress: Progress = new Progress, export_prune: Int = 0, export_list: Boolean = false, export_patterns: List[String] = Nil) { using(store.open_database(session_name))(db => { db.transaction { val export_names = read_theory_exports(db, session_name) // list if (export_list) { (for ((theory_name, name) <- export_names) yield compound_name(theory_name, name)). sorted.foreach(progress.echo) } // export if (export_patterns.nonEmpty) { val exports = (for { export_pattern <- export_patterns.iterator matcher = make_matcher(export_pattern) (theory_name, name) <- export_names if matcher(theory_name, name) } yield (theory_name, name)).toSet for { (theory_name, group) <- exports.toList.groupBy(_._1).toList.sortBy(_._1) name <- group.map(_._2).sorted entry <- read_entry(db, session_name, theory_name, name) } { val elems = theory_name :: space_explode('/', name) val path = if (elems.length < export_prune + 1) { error("Cannot prune path by " + export_prune + " element(s): " + Path.make(elems)) } else export_dir + Path.make(elems.drop(export_prune)) progress.echo("export " + path + (if (entry.executable) " (executable)" else "")) Isabelle_System.make_directory(path.dir) Bytes.write(path, entry.uncompressed(cache = store.xz_cache)) File.set_executable(path, entry.executable) } } } }) } /* Isabelle tool wrapper */ val default_export_dir: Path = Path.explode("export") val isabelle_tool = Isabelle_Tool("export", "retrieve theory exports", args => { /* arguments */ var export_dir = default_export_dir var dirs: List[Path] = Nil var export_list = false var no_build = false var options = Options.init() var export_prune = 0 var export_patterns: List[String] = Nil val getopts = Getopts(""" Usage: isabelle export [OPTIONS] SESSION Options are: -O DIR output directory for exported files (default: """ + default_export_dir + """) -d DIR include session directory -l list exports -n no build of session -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -p NUM prune path of exported files by NUM elements -x PATTERN extract files matching pattern (e.g. "*:**" for all) List or export theory exports for SESSION: named blobs produced by isabelle build. Option -l or -x is required; option -x may be repeated. The PATTERN language resembles glob patterns in the shell, with ? and * (both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc], and variants {pattern1,pattern2,pattern3}. """, "O:" -> (arg => export_dir = Path.explode(arg)), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "l" -> (_ => export_list = true), "n" -> (_ => no_build = true), "o:" -> (arg => options = options + arg), "p:" -> (arg => export_prune = Value.Int.parse(arg)), "x:" -> (arg => export_patterns ::= arg)) val more_args = getopts(args) val session_name = more_args match { case List(session_name) if export_list || export_patterns.nonEmpty => session_name case _ => getopts.usage() } val progress = new Console_Progress() /* build */ if (!no_build) { val rc = progress.interrupt_handler { Build.build_logic(options, session_name, progress = progress, dirs = dirs) } if (rc != 0) sys.exit(rc) } /* export files */ val store = Sessions.store(options) export_files(store, session_name, export_dir, progress = progress, export_prune = export_prune, export_list = export_list, export_patterns = export_patterns) }) } diff --git a/src/Pure/Tools/build_job.scala b/src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala +++ b/src/Pure/Tools/build_job.scala @@ -1,320 +1,333 @@ /* Title: Pure/Tools/build_job.scala Author: Makarius Build job running prover process, with rudimentary PIDE session. */ package isabelle import scala.collection.mutable class Build_Job(progress: Progress, session_name: String, val info: Sessions.Info, deps: Sessions.Deps, store: Sessions.Store, do_store: Boolean, verbose: Boolean, val numa_node: Option[Int], command_timings0: List[Properties.T]) { val options: Options = NUMA.policy_options(info.options, numa_node) private val sessions_structure = deps.sessions_structure private val future_result: Future[Process_Result] = Future.thread("build", uninterruptible = true) { val parent = info.parent.getOrElse("") val base = deps(parent) val env = Isabelle_System.settings() + ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString) val is_pure = Sessions.is_pure(session_name) val use_prelude = if (is_pure) Thy_Header.ml_roots.map(_._1) else Nil val eval_store = if (do_store) { (if (info.theories.nonEmpty) List("ML_Heap.share_common_data ()") else Nil) ::: List("ML_Heap.save_child " + ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(session_name)))) } else Nil val resources = new Resources(sessions_structure, base, command_timings = command_timings0) val session = new Session(options, resources) { override val xml_cache: XML.Cache = store.xml_cache override val xz_cache: XZ.Cache = store.xz_cache } + def make_rendering(snapshot: Document.Snapshot): Rendering = + new Rendering(snapshot, options, session) { + override def model: Document.Model = ??? + } object Build_Session_Errors { private val promise: Promise[List[String]] = Future.promise def result: Exn.Result[List[String]] = promise.join_result def cancel: Unit = promise.cancel def apply(errs: List[String]) { try { promise.fulfill(errs) } catch { case _: IllegalStateException => } } } val export_consumer = Export.consumer(store.open_database(session_name, output = true), cache = store.xz_cache) val stdout = new StringBuilder(1000) val stderr = new StringBuilder(1000) val messages = new mutable.ListBuffer[XML.Elem] val command_timings = new mutable.ListBuffer[Properties.T] val theory_timings = new mutable.ListBuffer[Properties.T] val session_timings = new mutable.ListBuffer[Properties.T] val runtime_statistics = new mutable.ListBuffer[Properties.T] val task_statistics = new mutable.ListBuffer[Properties.T] def fun( name: String, acc: mutable.ListBuffer[Properties.T], unapply: Properties.T => Option[Properties.T]): (String, Session.Protocol_Function) = { name -> ((msg: Prover.Protocol_Output) => unapply(msg.properties) match { case Some(props) => acc += props; true case _ => false }) } session.init_protocol_handler(new Session.Protocol_Handler { override def exit() { Build_Session_Errors.cancel } private def build_session_finished(msg: Prover.Protocol_Output): Boolean = { val (rc, errors) = try { val (rc, errs) = { import XML.Decode._ pair(int, list(x => x))(Symbol.decode_yxml(msg.text)) } val errors = for (err <- errs) yield { val prt = Protocol_Message.expose_no_reports(err) Pretty.string_of(prt, metric = Symbol.Metric) } (rc, errors) } catch { case ERROR(err) => (2, List(err)) } session.protocol_command("Prover.stop", rc.toString) Build_Session_Errors(errors) true } private def loading_theory(msg: Prover.Protocol_Output): Boolean = msg.properties match { case Markup.Loading_Theory(Markup.Name(name)) => progress.theory(Progress.Theory(name, session = session_name)) false case _ => false } private def export(msg: Prover.Protocol_Output): Boolean = msg.properties match { case Protocol.Export(args) => export_consumer(session_name, args, msg.bytes) true case _ => false } override val functions = List( Markup.Build_Session_Finished.name -> build_session_finished, Markup.Loading_Theory.name -> loading_theory, Markup.EXPORT -> export, fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply), fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply), fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply)) }) session.command_timings += Session.Consumer("command_timings") { case Session.Command_Timing(props) => for { elapsed <- Markup.Elapsed.unapply(props) elapsed_time = Time.seconds(elapsed) if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold") } command_timings += props.filter(Markup.command_timing_property) } session.runtime_statistics += Session.Consumer("ML_statistics") { case Session.Runtime_Statistics(props) => runtime_statistics += props } session.finished_theories += Session.Consumer[Document.Snapshot]("finished_theories") { case snapshot => + val rendering = make_rendering(snapshot) + def export(name: String, xml: XML.Body) { val theory_name = snapshot.node_name.theory val args = Protocol.Export.Args(theory_name = theory_name, name = name) - export_consumer(session_name, args, Bytes(YXML.string_of_body(xml))) + val bytes = Bytes(YXML.string_of_body(xml)) + if (!bytes.is_empty) export_consumer(session_name, args, bytes) } + def export_text(name: String, text: String): Unit = + export(name, List(XML.Text(text))) + export(Export.MARKUP, snapshot.xml_markup()) export(Export.MESSAGES, snapshot.messages.map(_._1)) + + val citations = Library.distinct(rendering.citations(Text.Range.full).map(_.info)) + export_text(Export.CITATIONS, cat_lines(citations)) } session.all_messages += Session.Consumer[Any]("build_session_output") { case msg: Prover.Output => val message = msg.message if (msg.is_stdout) { stdout ++= Symbol.encode(XML.content(message)) } else if (msg.is_stderr) { stderr ++= Symbol.encode(XML.content(message)) } else if (Protocol.is_exported(message)) { messages += message } else if (msg.is_exit) { val err = "Prover terminated" + (msg.properties match { case Markup.Process_Result(result) => ": " + result.print_rc case _ => "" }) Build_Session_Errors(List(err)) } case _ => } val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store) val process = Isabelle_Process(session, options, sessions_structure, store, logic = parent, raw_ml_system = is_pure, use_prelude = use_prelude, eval_main = eval_main, cwd = info.dir.file, env = env) val build_errors = Isabelle_Thread.interrupt_handler(_ => process.terminate) { Exn.capture { process.await_startup } match { case Exn.Res(_) => val resources_yxml = resources.init_session_yxml val args_yxml = YXML.string_of_body( { import XML.Encode._ pair(string, list(pair(Options.encode, list(pair(string, properties)))))( (session_name, info.theories)) }) session.protocol_command("build_session", resources_yxml, args_yxml) Build_Session_Errors.result case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn))) } } val process_result = Isabelle_Thread.interrupt_handler(_ => process.terminate) { process.await_shutdown } session.stop() val export_errors = export_consumer.shutdown(close = true).map(Output.error_message_text) val (document_output, document_errors) = try { if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) { using(store.open_database_context(deps.sessions_structure))(db_context => { val documents = Presentation.build_documents(session_name, deps, db_context, output_sources = info.document_output, output_pdf = info.document_output, progress = progress, verbose = verbose) db_context.output_database(session_name)(db => documents.foreach(_.write(db, session_name))) (documents.flatMap(_.log_lines), Nil) }) } (Nil, Nil) } catch { case Exn.Interrupt.ERROR(msg) => (Nil, List(msg)) } val result = { val more_output = Library.trim_line(stdout.toString) :: messages.toList.map(message => Symbol.encode(Protocol.message_text(List(message), metric = Symbol.Metric))) ::: command_timings.toList.map(Protocol.Command_Timing_Marker.apply) ::: theory_timings.toList.map(Protocol.Theory_Timing_Marker.apply) ::: session_timings.toList.map(Protocol.Session_Timing_Marker.apply) ::: runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) ::: task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) ::: document_output process_result.output(more_output) .error(Library.trim_line(stderr.toString)) .errors_rc(export_errors ::: document_errors) } build_errors match { case Exn.Res(build_errs) => val errs = build_errs ::: document_errors if (errs.isEmpty) result else { result.error_rc.output( errs.flatMap(s => split_lines(Output.error_message_text(s))) ::: errs.map(Protocol.Error_Message_Marker.apply)) } case Exn.Exn(Exn.Interrupt()) => if (result.ok) result.copy(rc = Exn.Interrupt.return_code) else result case Exn.Exn(exn) => throw exn } } def terminate: Unit = future_result.cancel def is_finished: Boolean = future_result.is_finished private val timeout_request: Option[Event_Timer.Request] = { if (info.timeout > Time.zero) Some(Event_Timer.request(Time.now() + info.timeout) { terminate }) else None } def join: (Process_Result, Option[String]) = { val result1 = future_result.join val was_timeout = timeout_request match { case None => false case Some(request) => !request.cancel } val result2 = if (result1.interrupted) { if (was_timeout) result1.error(Output.error_message_text("Timeout")).was_timeout else result1.error(Output.error_message_text("Interrupt")) } else result1 val heap_digest = if (result2.ok && do_store && store.output_heap(session_name).is_file) Some(Sessions.write_heap_digest(store.output_heap(session_name))) else None (result2, heap_digest) } }