diff --git a/src/Pure/Admin/build_doc.scala b/src/Pure/Admin/build_doc.scala --- a/src/Pure/Admin/build_doc.scala +++ b/src/Pure/Admin/build_doc.scala @@ -1,112 +1,112 @@ /* Title: Pure/Admin/build_doc.scala Author: Makarius Build Isabelle documentation. */ package isabelle object Build_Doc { /* build_doc */ def build_doc( options: Options, progress: Progress = new Progress, all_docs: Boolean = false, max_jobs: Int = 1, sequential: Boolean = false, docs: List[String] = Nil): Unit = { val store = Sessions.store(options) val sessions_structure = Sessions.load_structure(options) val selected = for { session <- sessions_structure.build_topological_order info = sessions_structure(session) if info.groups.contains("doc") doc = info.options.string("document_variants") if all_docs || docs.contains(doc) } yield (doc, session) val documents = selected.map(_._1) val selection = Sessions.Selection(sessions = selected.map(_._2)) docs.filter(doc => !documents.contains(doc)) match { case Nil => case bad => error("No documentation session for " + commas_quote(bad)) } progress.echo("Build started for sessions " + commas_quote(selection.sessions)) Build.build(options, selection = selection, progress = progress, max_jobs = max_jobs).ok || error("Build failed") progress.echo("Build started for documentation " + commas_quote(documents)) val doc_options = options + "document=pdf" val deps = Sessions.load_structure(doc_options).selection_deps(selection) val errs = Par_List.map[(String, String), Option[String]]( { case (doc, session) => try { progress.echo("Documentation " + quote(doc) + " ...") using(store.open_database_context())(db_context => - Document_Build.build_documents(session, deps, db_context, + Document_Build.build_documents(Document_Build.context(session, deps, db_context), output_pdf = Some(Path.explode("~~/doc")))) None } catch { case Exn.Interrupt.ERROR(msg) => val sep = if (msg.contains('\n')) "\n" else " " Some("Documentation " + quote(doc) + " failed:" + sep + msg) } }, selected, sequential = sequential).flatten if (errs.nonEmpty) error(cat_lines(errs)) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_doc", "build Isabelle documentation", Scala_Project.here, args => { var all_docs = false var max_jobs = 1 var sequential = false var options = Options.init() val getopts = Getopts(""" Usage: isabelle build_doc [OPTIONS] [DOCS ...] Options are: -a select all documentation sessions -j INT maximum number of parallel jobs (default 1) -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -s sequential LaTeX jobs Build Isabelle documentation from documentation sessions with suitable document_variants entry. """, "a" -> (_ => all_docs = true), "j:" -> (arg => max_jobs = Value.Int.parse(arg)), "o:" -> (arg => options = options + arg), "s" -> (_ => sequential = true)) val docs = getopts(args) if (!all_docs && docs.isEmpty) getopts.usage() val progress = new Console_Progress() progress.interrupt_handler { build_doc(options, progress = progress, all_docs = all_docs, max_jobs = max_jobs, sequential = sequential, docs = docs) } }) } diff --git a/src/Pure/Thy/document_build.scala b/src/Pure/Thy/document_build.scala --- a/src/Pure/Thy/document_build.scala +++ b/src/Pure/Thy/document_build.scala @@ -1,378 +1,439 @@ /* Title: Pure/Thy/document_build.scala Author: Makarius Build theory document (PDF) from session database. */ package isabelle object Document_Build { /* document variants */ abstract class Document_Name { def name: String def path: Path = Path.basic(name) override def toString: String = name } object Document_Variant { def parse(name: String, tags: String): Document_Variant = Document_Variant(name, Library.space_explode(',', tags)) def parse(opt: String): Document_Variant = Library.space_explode('=', opt) match { case List(name) => Document_Variant(name, Nil) case List(name, tags) => parse(name, tags) case _ => error("Malformed document variant: " + quote(opt)) } } sealed case class Document_Variant(name: String, tags: List[String]) extends Document_Name { def print_tags: String = tags.mkString(",") def print: String = if (tags.isEmpty) name else name + "=" + print_tags def latex_sty: String = Library.terminate_lines( tags.map(tag => tag.toList match { case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}" case '-' :: cs => "\\isadroptag{" + cs.mkString + "}" case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}" case cs => "\\isakeeptag{" + cs.mkString + "}" })) } sealed case class Document_Input(name: String, sources: SHA1.Digest) extends Document_Name sealed case class Document_Output(name: String, sources: SHA1.Digest, log_xz: Bytes, pdf: Bytes) extends Document_Name { def log: String = log_xz.uncompress().text def log_lines: List[String] = split_lines(log) def write(db: SQL.Database, session_name: String): Unit = write_document(db, session_name, this) + + def write(dir: Path): Path = + { + val path = dir + Path.basic(name).pdf + Isabelle_System.make_directory(path.expand.dir) + Bytes.write(path, pdf) + path + } } /* SQL data model */ object Data { val session_name = SQL.Column.string("session_name").make_primary_key val name = SQL.Column.string("name").make_primary_key val sources = SQL.Column.string("sources") val log_xz = SQL.Column.bytes("log_xz") val pdf = SQL.Column.bytes("pdf") val table = SQL.Table("isabelle_documents", List(session_name, name, sources, log_xz, pdf)) def where_equal(session_name: String, name: String = ""): SQL.Source = "WHERE " + Data.session_name.equal(session_name) + (if (name == "") "" else " AND " + Data.name.equal(name)) } def read_documents(db: SQL.Database, session_name: String): List[Document_Input] = { val select = Data.table.select(List(Data.name, Data.sources), Data.where_equal(session_name)) db.using_statement(select)(stmt => stmt.execute_query().iterator(res => { val name = res.string(Data.name) val sources = res.string(Data.sources) Document_Input(name, SHA1.fake(sources)) }).toList) } def read_document(db: SQL.Database, session_name: String, name: String): Option[Document_Output] = { val select = Data.table.select(sql = Data.where_equal(session_name, name)) db.using_statement(select)(stmt => { val res = stmt.execute_query() if (res.next()) { val name = res.string(Data.name) val sources = res.string(Data.sources) val log_xz = res.bytes(Data.log_xz) val pdf = res.bytes(Data.pdf) Some(Document_Output(name, SHA1.fake(sources), log_xz, pdf)) } else None }) } def write_document(db: SQL.Database, session_name: String, doc: Document_Output): Unit = { db.using_statement(Data.table.insert())(stmt => { stmt.string(1) = session_name stmt.string(2) = doc.name stmt.string(3) = doc.sources.toString stmt.bytes(4) = doc.log_xz stmt.bytes(5) = doc.pdf stmt.execute() }) } + /* context */ + + def context( + session: String, + deps: Sessions.Deps, + db_context: Sessions.Database_Context, + progress: Progress = new Progress): Context = + { + val info = deps.sessions_structure(session) + val base = deps(session) + val hierarchy = deps.sessions_structure.hierarchy(session) + new Context(info, base, hierarchy, db_context, progress) + } + + final class Context private[Document_Build]( + info: Sessions.Info, + base: Sessions.Base, + hierarchy: List[String], + db_context: Sessions.Database_Context, + val progress: Progress = new Progress) + { + /* session info */ + + def session: String = info.name + def options: Options = info.options + + def get_export(theory: String, name: String): Export.Entry = + db_context.get_export(hierarchy, theory, name) + + + /* document content */ + + def documents: List[Document_Variant] = info.documents + + def session_theories: List[Document.Node.Name] = base.session_theories + def document_theories: List[Document.Node.Name] = session_theories ::: base.document_theories + + lazy val tex_files: List[Content] = + for (name <- document_theories) + yield { + val path = Path.basic(tex_name(name)) + val bytes = get_export(name.theory, document_tex_name(name)).uncompressed + Content(path, bytes) + } + + lazy val session_graph: Content = + { + val path = Presentation.session_graph_path + val bytes = graphview.Graph_File.make_pdf(options, base.session_graph_display) + Content(path, bytes) + } + + lazy val session_tex: Content = + { + val path = Path.basic("session.tex") + val text = + Library.terminate_lines( + base.session_theories.map(name => "\\input{" + tex_name(name) + "}")) + Content(path, Bytes(text)) + } + + + /* document directory */ + + def prepare_directory(dir: Path, doc: Document_Variant): Directory = + { + val doc_dir = dir + Path.basic(doc.name) + Isabelle_System.make_directory(doc_dir) + + + /* sources */ + + Isabelle_System.bash("isabelle latex -o sty", cwd = doc_dir.file).check + File.write(doc_dir + Path.explode("isabelletags.sty"), doc.latex_sty) + for ((base_dir, src) <- info.document_files) { + Isabelle_System.copy_file_base(info.dir + base_dir, src, doc_dir) + } + + session_tex.write(doc_dir) + tex_files.foreach(_.write(doc_dir)) + + val root_name1 = "root_" + doc.name + val root_name = if ((doc_dir + Path.explode(root_name1).tex).is_file) root_name1 else "root" + + val sources = + SHA1.digest_set(File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest)) + + + /* derived material */ + + session_graph.write(doc_dir) + + Directory(doc_dir, doc, root_name, sources) + } + + def old_document(directory: Directory): Option[Document_Output] = + for { + old_doc <- db_context.input_database(session)(read_document(_, _, directory.doc.name)) + if old_doc.sources == directory.sources + } + yield { + old_doc.write(directory.doc_dir) + old_doc + } + } + + sealed case class Content(path: Path, bytes: Bytes) + { + def write(dir: Path): Unit = Bytes.write(dir + path, bytes) + } + + sealed case class Directory( + doc_dir: Path, + doc: Document_Variant, + root_name: String, + sources: SHA1.Digest) + { + def log_errors(): List[String] = + Latex.latex_errors(doc_dir, root_name) ::: + Bibtex.bibtex_errors(doc_dir, root_name) + + def make_document(log: List[String], errors: List[String]): Document_Output = + { + val root_pdf = Path.basic(root_name).pdf + val result_pdf = doc_dir + root_pdf + + if (errors.nonEmpty) { + val errors1 = errors ::: List("Failed to build document " + quote(doc.name)) + throw new Build_Error(log, Exn.cat_message(errors1: _*)) + } + else if (!result_pdf.is_file) { + val message = "Bad document result: expected to find " + root_pdf + throw new Build_Error(log, message) + } + else { + val log_xz = Bytes(cat_lines(log)).compress() + val pdf = Bytes.read(result_pdf) + Document_Output(doc.name, sources, log_xz, pdf) + } + } + } + /* build documents */ - val session_tex_path = Path.explode("session.tex") - def tex_name(name: Document.Node.Name): String = name.theory_base_name + ".tex" def document_tex_name(name: Document.Node.Name): String = "document/" + tex_name(name) class Build_Error(val log_lines: List[String], val message: String) extends Exn.User_Error(message) def build_documents( - session: String, - deps: Sessions.Deps, - db_context: Sessions.Database_Context, - progress: Progress = new Progress, + context: Context, output_sources: Option[Path] = None, output_pdf: Option[Path] = None, verbose: Boolean = false, verbose_latex: Boolean = false): List[Document_Output] = { - /* session info */ - - val info = deps.sessions_structure(session) - val hierarchy = deps.sessions_structure.hierarchy(session) - val options = info.options - val base = deps(session) - val graph_pdf = graphview.Graph_File.make_pdf(options, base.session_graph_display) - - - /* prepare document directory */ - - lazy val tex_files = - for (name <- base.session_theories ::: base.document_theories) - yield { - val entry = db_context.get_export(hierarchy, name.theory, document_tex_name(name)) - Path.basic(tex_name(name)) -> entry.uncompressed - } - - def prepare_dir1(dir: Path, doc: Document_Variant): (Path, String) = - { - val doc_dir = dir + Path.basic(doc.name) - Isabelle_System.make_directory(doc_dir) - - Isabelle_System.bash("isabelle latex -o sty", cwd = doc_dir.file).check - File.write(doc_dir + Path.explode("isabelletags.sty"), doc.latex_sty) - for ((base_dir, src) <- info.document_files) { - Isabelle_System.copy_file_base(info.dir + base_dir, src, doc_dir) - } - - File.write(doc_dir + session_tex_path, - Library.terminate_lines( - base.session_theories.map(name => "\\input{" + tex_name(name) + "}"))) - - for ((path, tex) <- tex_files) Bytes.write(doc_dir + path, tex) - - val root1 = "root_" + doc.name - val root = if ((doc_dir + Path.explode(root1).tex).is_file) root1 else "root" - - (doc_dir, root) - } - - def prepare_dir2(dir: Path, doc: Document_Variant): Unit = - { - val doc_dir = dir + Path.basic(doc.name) - - // non-deterministic, but irrelevant - Bytes.write(doc_dir + Presentation.session_graph_path, graph_pdf) - } - - - /* produce documents */ + val progress = context.progress val documents = - for (doc <- info.documents) + for (doc <- context.documents) yield { Isabelle_System.with_tmp_dir("document")(tmp_dir => { - progress.echo("Preparing " + session + "/" + doc.name + " ...") + progress.echo("Preparing " + context.session + "/" + doc.name + " ...") val start = Time.now() - // prepare sources + // prepare directory - val (doc_dir, root) = prepare_dir1(tmp_dir, doc) - val digests = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest) - val sources = SHA1.digest_set(digests) - prepare_dir2(tmp_dir, doc) - - for (dir <- output_sources) { - prepare_dir1(dir, doc) - prepare_dir2(dir, doc) - } + output_sources.foreach(context.prepare_directory(_, doc)) + val directory = context.prepare_directory(tmp_dir, doc) + val doc_dir = directory.doc_dir + val root = directory.root_name - // old document from database + // prepare document - val old_document = - for { - old_doc <- db_context.input_database(session)(read_document(_, _, doc.name)) - if old_doc.sources == sources - } - yield { - Bytes.write(doc_dir + doc.path.pdf, old_doc.pdf) - old_doc - } - - old_document getOrElse { + context.old_document(directory) getOrElse { // bash scripts def root_bash(ext: String): String = Bash.string(root + "." + ext) def latex_bash(fmt: String = "pdf", ext: String = "tex"): String = "isabelle latex -o " + Bash.string(fmt) + " " + Bash.string(root + "." + ext) def bash(items: String*): Process_Result = progress.bash(items.mkString(" && "), cwd = doc_dir.file, echo = verbose_latex, watchdog = Time.seconds(0.5)) // prepare document val result = if ((doc_dir + Path.explode("build")).is_file) { bash("./build pdf " + Bash.string(doc.name)) } else { bash( latex_bash(), "{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }", "{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }", latex_bash(), latex_bash()) } + val stop = Time.now() + val timing = stop - start + // result - val root_pdf = Path.basic(root).pdf - val result_path = doc_dir + root_pdf - - val log_lines = result.out_lines ::: result.err_lines - - val errors = - (if (result.ok) Nil else List(result.err)) ::: - Latex.latex_errors(doc_dir, root) ::: - Bibtex.bibtex_errors(doc_dir, root) + val log = result.out_lines ::: result.err_lines + val errors = (if (result.ok) Nil else List(result.err)) ::: directory.log_errors() + val document = directory.make_document(log, errors) - if (errors.nonEmpty) { - val message = - Exn.cat_message( - (errors ::: List("Failed to build document " + quote(doc.name))):_*) - throw new Build_Error(log_lines, message) - } - else if (!result_path.is_file) { - val message = "Bad document result: expected to find " + root_pdf - throw new Build_Error(log_lines, message) - } - else { - val stop = Time.now() - val timing = stop - start - progress.echo("Finished " + session + "/" + doc.name + - " (" + timing.message_hms + " elapsed time)") + progress.echo("Finished " + context.session + "/" + doc.name + + " (" + timing.message_hms + " elapsed time)") - val log_xz = Bytes(cat_lines(log_lines)).compress() - val pdf = Bytes.read(result_path) - Document_Output(doc.name, sources, log_xz, pdf) - } + document } }) } for (dir <- output_pdf; doc <- documents) { - Isabelle_System.make_directory(dir) - val path = dir + doc.path.pdf - Bytes.write(path, doc.pdf) + val path = doc.write(dir) progress.echo("Document at " + path.absolute) } documents } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("document", "prepare session theory document", Scala_Project.here, args => { var output_sources: Option[Path] = None var output_pdf: Option[Path] = None var verbose_latex = false var dirs: List[Path] = Nil var options = Options.init() var verbose_build = false val getopts = Getopts( """ Usage: isabelle document [OPTIONS] SESSION Options are: -O DIR output directory for LaTeX sources and resulting PDF -P DIR output directory for resulting PDF -S DIR output directory for LaTeX sources -V verbose latex -d DIR include session directory -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v verbose build Prepare the theory document of a session. """, "O:" -> (arg => { val dir = Path.explode(arg) output_sources = Some(dir) output_pdf = Some(dir) }), "P:" -> (arg => { output_pdf = Some(Path.explode(arg)) }), "S:" -> (arg => { output_sources = Some(Path.explode(arg)) }), "V" -> (_ => verbose_latex = true), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "o:" -> (arg => options = options + arg), "v" -> (_ => verbose_build = true)) val more_args = getopts(args) val session = more_args match { case List(a) => a case _ => getopts.usage() } val progress = new Console_Progress(verbose = verbose_build) val store = Sessions.store(options) progress.interrupt_handler { val res = Build.build(options, selection = Sessions.Selection.session(session), dirs = dirs, progress = progress, verbose = verbose_build) if (!res.ok) error("Failed to build session " + quote(session)) val deps = Sessions.load_structure(options + "document=pdf", dirs = dirs). selection_deps(Sessions.Selection.session(session)) if (output_sources.isEmpty && output_pdf.isEmpty) { progress.echo_warning("No output directory") } using(store.open_database_context())(db_context => - build_documents(session, deps, db_context, progress = progress, + { + build_documents(context(session, deps, db_context, progress = progress), output_sources = output_sources, output_pdf = output_pdf, - verbose = true, verbose_latex = verbose_latex)) + verbose = true, verbose_latex = verbose_latex) + }) } }) } 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,537 +1,537 @@ /* Title: Pure/Tools/build_job.scala Author: Makarius Build job running prover process, with rudimentary PIDE session. */ package isabelle import scala.collection.mutable object Build_Job { /* theory markup/messages from database */ def read_theory( db_context: Sessions.Database_Context, resources: Resources, session: String, theory: String, unicode_symbols: Boolean = false): Option[Command] = { def read(name: String): Export.Entry = db_context.get_export(List(session), theory, name) def read_xml(name: String): XML.Body = YXML.parse_body( Symbol.output(unicode_symbols, UTF8.decode_permissive(read(name).uncompressed)), cache = db_context.cache) (read(Export.DOCUMENT_ID).text, split_lines(read(Export.FILES).text)) match { case (Value.Long(id), thy_file :: blobs_files) => val node_name = resources.file_node(Path.explode(thy_file), theory = theory) val results = Command.Results.make( for (elem @ XML.Elem(Markup(_, Markup.Serial(i)), _) <- read_xml(Export.MESSAGES)) yield i -> elem) val blobs = blobs_files.map(file => { val path = Path.explode(file) val name = resources.file_node(path) val src_path = File.relative_path(node_name.master_dir_path, path).getOrElse(path) Command.Blob(name, src_path, None) }) val blobs_xml = for (i <- (1 to blobs.length).toList) yield read_xml(Export.MARKUP + i) val blobs_info = Command.Blobs_Info( for { (Command.Blob(name, src_path, _), xml) <- blobs zip blobs_xml } yield { val text = XML.content(xml) val chunk = Symbol.Text_Chunk(text) val digest = SHA1.digest(Symbol.encode(text)) Exn.Res(Command.Blob(name, src_path, Some((digest, chunk)))) }) val thy_xml = read_xml(Export.MARKUP) val thy_source = XML.content(thy_xml) val markups_index = Command.Markup_Index.markup :: blobs.map(Command.Markup_Index.blob) val markups = Command.Markups.make( for ((index, xml) <- markups_index.zip(thy_xml :: blobs_xml)) yield index -> Markup_Tree.from_XML(xml)) val command = Command.unparsed(thy_source, theory = true, id = id, node_name = node_name, blobs_info = blobs_info, results = results, markups = markups) Some(command) case _ => None } } /* print messages */ def print_log( options: Options, session_name: String, theories: List[String] = Nil, verbose: Boolean = false, progress: Progress = new Progress, margin: Double = Pretty.default_margin, breakgain: Double = Pretty.default_breakgain, metric: Pretty.Metric = Symbol.Metric, unicode_symbols: Boolean = false): Unit = { val store = Sessions.store(options) val resources = Resources.empty val session = new Session(options, resources) using(store.open_database_context())(db_context => { val result = db_context.input_database(session_name)((db, _) => { val theories = store.read_theories(db, session_name) val errors = store.read_errors(db, session_name) store.read_build(db, session_name).map(info => (theories, errors, info.return_code)) }) result match { case None => error("Missing build database for session " + quote(session_name)) case Some((used_theories, errors, rc)) => val bad_theories = theories.filterNot(used_theories.toSet) if (bad_theories.nonEmpty) error("Unknown theories " + commas_quote(bad_theories)) val print_theories = if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet) for (thy <- print_theories) { val thy_heading = "\nTheory " + quote(thy) + ":" read_theory(db_context, resources, session_name, thy, unicode_symbols = unicode_symbols) match { case None => progress.echo(thy_heading + " MISSING") case Some(command) => val snapshot = Document.State.init.snippet(command) val rendering = new Rendering(snapshot, options, session) val messages = rendering.text_messages(Text.Range.full) .filter(message => verbose || Protocol.is_exported(message.info)) if (messages.nonEmpty) { val line_document = Line.Document(command.source) progress.echo(thy_heading) for (Text.Info(range, elem) <- messages) { val line = line_document.position(range.start).line1 val pos = Position.Line_File(line, command.node_name.node) progress.echo( Protocol.message_text(elem, heading = true, pos = pos, margin = margin, breakgain = breakgain, metric = metric)) } } } } if (errors.nonEmpty) { val msg = Symbol.output(unicode_symbols, cat_lines(errors)) progress.echo("\nBuild errors:\n" + Output.error_message_text(msg)) } if (rc != 0) progress.echo("\n" + Process_Result.print_return_code(rc)) } }) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("log", "print messages from build database", Scala_Project.here, args => { /* arguments */ var unicode_symbols = false var theories: List[String] = Nil var margin = Pretty.default_margin var options = Options.init() var verbose = false val getopts = Getopts(""" Usage: isabelle log [OPTIONS] SESSION Options are: -T NAME restrict to given theories (multiple options possible) -U output Unicode symbols -m MARGIN margin for pretty printing (default: """ + margin + """) -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v print all messages, including information, tracing etc. Print messages from the build database of the given session, without any checks against current sources: results from a failed build can be printed as well. """, "T:" -> (arg => theories = theories ::: List(arg)), "U" -> (_ => unicode_symbols = true), "m:" -> (arg => margin = Value.Double.parse(arg)), "o:" -> (arg => options = options + arg), "v" -> (_ => verbose = true)) val more_args = getopts(args) val session_name = more_args match { case List(session_name) => session_name case _ => getopts.usage() } val progress = new Console_Progress() print_log(options, session_name, theories = theories, verbose = verbose, margin = margin, progress = progress, unicode_symbols = unicode_symbols) }) } 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 result_base = deps(session_name) 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 cache: XML.Cache = store.cache override def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = { result_base.load_commands.get(name.expand) match { case Some(spans) => val syntax = result_base.theory_syntax(name) Command.build_blobs_info(syntax, name, spans) case None => Command.Blobs_Info.none } } } 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]): Unit = { try { promise.fulfill(errs) } catch { case _: IllegalStateException => } } } val export_consumer = Export.consumer(store.open_database(session_name, output = true), store.cache) val stdout = new StringBuilder(1000) val stderr = new StringBuilder(1000) 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(): Unit = 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.chunk) 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 = new Rendering(snapshot, options, session) def export(name: String, xml: XML.Body, compress: Boolean = true): Unit = { val theory_name = snapshot.node_name.theory val args = Protocol.Export.Args(theory_name = theory_name, name = name, compress = compress) val bytes = Bytes(Symbol.encode(YXML.string_of_body(xml))) if (!bytes.is_empty) export_consumer(session_name, args, bytes) } def export_text(name: String, text: String, compress: Boolean = true): Unit = export(name, List(XML.Text(text)), compress = compress) for (command <- snapshot.snippet_command) { export_text(Export.DOCUMENT_ID, command.id.toString, compress = false) } export_text(Export.FILES, cat_lines(snapshot.node_files.map(_.symbolic.node)), compress = false) for (((_, xml), i) <- snapshot.xml_markup_blobs().zipWithIndex) { export(Export.MARKUP + (i + 1), xml) } 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 (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())(db_context => { val documents = - Document_Build.build_documents(session_name, deps, db_context, + Document_Build.build_documents( + Document_Build.context(session_name, deps, db_context, progress = progress), 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) }) } else (Nil, Nil) } catch { case exn: Document_Build.Build_Error => (exn.log_lines, List(exn.message)) case Exn.Interrupt.ERROR(msg) => (Nil, List(msg)) } val result = { val theory_timing = theory_timings.iterator.map( { case props @ Markup.Name(name) => name -> props }).toMap val used_theory_timings = for { (name, _) <- deps(session_name).used_theories } yield theory_timing.getOrElse(name.theory, Markup.Name(name.theory)) val more_output = Library.trim_line(stdout.toString) :: command_timings.toList.map(Protocol.Command_Timing_Marker.apply) ::: used_theory_timings.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_ignored) None else Some(Event_Timer.request(Time.now() + info.timeout) { terminate() }) } 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.ok) result1 else if (was_timeout) result1.error(Output.error_message_text("Timeout")).timeout_rc else if (result1.interrupted) 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) } }