# HG changeset patch # User wenzelm # Date 1546105557 -3600 # Node ID da2726f78610c3b58fad0951239cb32ea5f37c58 # Parent 1ae0c822682c5773a4d5a86434a281e97ef222f4# Parent faf547d2834c2eeab276b4fb2161984552e7a251 merged diff -r 1ae0c822682c -r da2726f78610 src/Pure/PIDE/headless.scala --- a/src/Pure/PIDE/headless.scala Sat Dec 29 17:38:29 2018 +0100 +++ b/src/Pure/PIDE/headless.scala Sat Dec 29 18:45:57 2018 +0100 @@ -16,47 +16,6 @@ { /** session **/ - def start_session( - options: Options, - session_name: String, - session_dirs: List[Path] = Nil, - include_sessions: List[String] = Nil, - session_base: Option[Sessions.Base] = None, - print_mode: List[String] = Nil, - progress: Progress = No_Progress, - log: Logger = No_Logger): Session = - { - val base = - session_base getOrElse - Sessions.base_info(options, session_name, include_sessions = include_sessions, - progress = progress, dirs = session_dirs).check_base - val resources = new Resources(base, log = log) - val session = new Session(session_name, options, resources) - - val session_error = Future.promise[String] - var session_phase: Session.Consumer[Session.Phase] = null - session_phase = - Session.Consumer(getClass.getName) { - case Session.Ready => - session.phase_changed -= session_phase - session_error.fulfill("") - case Session.Terminated(result) if !result.ok => - session.phase_changed -= session_phase - session_error.fulfill("Session start failed: return code " + result.rc) - case _ => - } - session.phase_changed += session_phase - - progress.echo("Starting session " + session_name + " ...") - Isabelle_Process.start(session, options, - logic = session_name, dirs = session_dirs, modes = print_mode) - - session_error.join match { - case "" => session - case msg => session.stop(); error(msg) - } - } - private def stable_snapshot( state: Document.State, version: Document.Version, name: Document.Node.Name): Document.Snapshot = { @@ -330,6 +289,23 @@ object Resources { + def apply(base_info: Sessions.Base_Info, log: Logger = No_Logger): Resources = + new Resources(base_info, log = log) + + def make( + options: Options, + session_name: String, + session_dirs: List[Path] = Nil, + include_sessions: List[String] = Nil, + progress: Progress = No_Progress, + log: Logger = No_Logger): Resources = + { + val base_info = + Sessions.base_info(options, session_name, dirs = session_dirs, + include_sessions = include_sessions, progress = progress) + apply(base_info, log = log) + } + final class Theory private[Headless]( val node_name: Document.Node.Name, val node_header: Document.Node.Header, @@ -450,11 +426,49 @@ } } - class Resources(session_base: Sessions.Base, log: Logger = No_Logger) - extends isabelle.Resources(session_base, log = log) + class Resources private[Headless]( + val session_base_info: Sessions.Base_Info, + log: Logger = No_Logger) + extends isabelle.Resources(session_base_info.check_base, log = log) { resources => + def options: Options = session_base_info.options + + + /* session */ + + def start_session(print_mode: List[String] = Nil, progress: Progress = No_Progress): Session = + { + val session = new Session(session_base_info.session, options, resources) + + val session_error = Future.promise[String] + var session_phase: Session.Consumer[Session.Phase] = null + session_phase = + Session.Consumer(getClass.getName) { + case Session.Ready => + session.phase_changed -= session_phase + session_error.fulfill("") + case Session.Terminated(result) if !result.ok => + session.phase_changed -= session_phase + session_error.fulfill("Session start failed: return code " + result.rc) + case _ => + } + session.phase_changed += session_phase + + progress.echo("Starting session " + session_base_info.session + " ...") + Isabelle_Process.start(session, options, + logic = session_base_info.session, dirs = session_base_info.dirs, modes = print_mode) + + session_error.join match { + case "" => session + case msg => session.stop(); error(msg) + } + } + + + /* theories */ + private val state = Synchronized(Resources.State()) def load_theories( diff -r 1ae0c822682c -r da2726f78610 src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala Sat Dec 29 17:38:29 2018 +0100 +++ b/src/Pure/Tools/dump.scala Sat Dec 29 18:45:57 2018 +0100 @@ -17,7 +17,7 @@ deps: Sessions.Deps, output_dir: Path, snapshot: Document.Snapshot, - node_status: Document_Status.Node_Status) + status: Document_Status.Node_Status) { def write(file_name: Path, bytes: Bytes) { @@ -55,14 +55,14 @@ { case args => for (entry <- args.snapshot.exports if entry.name == "document.tex") args.write(Path.explode(entry.name), entry.uncompressed()) - }, options = List("editor_presentation", "export_document")), + }, options = List("export_document")), Aspect("theory", "foundational theory content", { case args => for { entry <- args.snapshot.exports if entry.name.startsWith(Export_Theory.export_prefix) } args.write(Path.explode(entry.name), entry.uncompressed()) - }, options = List("editor_presentation", "export_theory")) + }, options = List("export_theory")) ).sortBy(_.name) def show_aspects: String = @@ -73,83 +73,119 @@ error("Unknown aspect " + quote(name)) - /* session */ + /* dependencies */ - def session(dump_options: Options, logic: String, - consume: (Sessions.Deps, Document.Snapshot, Document_Status.Node_Status) => Unit, + def used_theories(options: Options, deps: Sessions.Deps, progress: Progress = No_Progress) + : List[Document.Node.Name] = + { + deps.used_theories_condition(options, progress.echo_warning).map(_._2) + } + + def dependencies( + options: Options, progress: Progress = No_Progress, - log: Logger = No_Logger, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil, - system_mode: Boolean = false, - selection: Sessions.Selection = Sessions.Selection.empty): Boolean = + selection: Sessions.Selection = Sessions.Selection.empty) + : (Sessions.Deps, List[Document.Node.Name]) = { - /* dependencies */ - val deps = - Sessions.load_structure(dump_options, dirs = dirs, select_dirs = select_dirs). - selection_deps(dump_options, selection, uniform_session = true, loading_sessions = true) + Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs). + selection_deps(options, selection, progress = progress, + uniform_session = true, loading_sessions = true) - val include_sessions = - deps.sessions_structure.imports_topological_order + val theories = used_theories(options, deps, progress = progress) - val use_theories = - for { (_, name) <- deps.used_theories_condition(dump_options, progress.echo_warning) } - yield name.theory + (deps, theories) + } - /* dump aspects asynchronously */ + /* session */ + + def session( + deps: Sessions.Deps, + resources: Headless.Resources, + process_theory: (Sessions.Deps, Document.Snapshot, Document_Status.Node_Status) => Unit, + progress: Progress = No_Progress) + { + /* asynchronous consumer */ object Consumer { - private val consumer_ok = Synchronized(true) + sealed case class Bad_Theory( + name: Document.Node.Name, + status: Document_Status.Node_Status, + errors: List[String]) + + private val consumer_bad_theories = Synchronized(List.empty[Bad_Theory]) private val consumer = Consumer_Thread.fork(name = "dump")( consume = (args: (Document.Snapshot, Document_Status.Node_Status)) => { - val (snapshot, node_status) = args - if (node_status.ok) consume(deps, snapshot, node_status) + val (snapshot, status) = args + val name = snapshot.node_name + if (status.ok) { + try { process_theory(deps, snapshot, status) } + catch { + case exn: Throwable if !Exn.is_interrupt(exn) => + val msg = Exn.message(exn) + progress.echo("FAILED to process theory " + name) + progress.echo_error_message(msg) + consumer_bad_theories.change(Bad_Theory(name, status, List(msg)) :: _) + } + } else { - consumer_ok.change(_ => false) - for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree)) { - val msg = XML.content(Pretty.formatted(List(tree))) - progress.echo_error_message("Error" + Position.here(pos) + ":\n" + msg) - } + val msgs = + for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree)) + yield { + "Error" + Position.here(pos) + ":\n" + + XML.content(Pretty.formatted(List(tree))) + } + progress.echo("FAILED to process theory " + name) + msgs.foreach(progress.echo_error_message) + consumer_bad_theories.change(Bad_Theory(name, status, msgs) :: _) } true }) - def apply(snapshot: Document.Snapshot, node_status: Document_Status.Node_Status): Unit = - consumer.send((snapshot, node_status)) + def apply(snapshot: Document.Snapshot, status: Document_Status.Node_Status): Unit = + consumer.send((snapshot, status)) - def shutdown(): Boolean = + def shutdown(): List[Bad_Theory] = { consumer.shutdown() - consumer_ok.value + consumer_bad_theories.value.reverse } } /* run session */ - val session = - Headless.start_session(dump_options, logic, session_dirs = dirs ::: select_dirs, - include_sessions = include_sessions, progress = progress, log = log) - - val use_theories_result = - session.use_theories(use_theories, progress = progress, commit = Some(Consumer.apply _)) - - session.stop() + val session = resources.start_session(progress = progress) + try { + val use_theories = used_theories(resources.options, deps).map(_.theory) + val use_theories_result = + session.use_theories(use_theories, progress = progress, commit = Some(Consumer.apply _)) - val consumer_ok = Consumer.shutdown() + val bad_theories = Consumer.shutdown() + val bad_msgs = + bad_theories.map(bad => + Output.clean_yxml( + "FAILED theory " + bad.name + + (if (bad.status.consolidated) "" else ": " + bad.status.percentage + "% finished") + + (if (bad.errors.isEmpty) "" else bad.errors.mkString("\n", "\n", "")))) - use_theories_result.nodes_pending match { - case Nil => - case pending => error("Pending theories " + commas_quote(pending.map(p => p._1.toString))) + val pending_msgs = + use_theories_result.nodes_pending match { + case Nil => Nil + case pending => List("Pending theories: " + commas(pending.map(p => p._1.toString))) + } + + val errors = bad_msgs ::: pending_msgs + if (errors.nonEmpty) error(errors.mkString("\n\n")) } - - use_theories_result.ok && consumer_ok + finally { session.stop() } } @@ -162,7 +198,7 @@ val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options val options1 = options0 + "completion_limit=0" + "ML_statistics=false" + - "parallel_proofs=0" + "editor_tracing_messages=0" + "parallel_proofs=0" + "editor_tracing_messages=0" + "editor_presentation" (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) }) } @@ -174,24 +210,29 @@ select_dirs: List[Path] = Nil, output_dir: Path = default_output_dir, system_mode: Boolean = false, - selection: Sessions.Selection = Sessions.Selection.empty): Boolean = + selection: Sessions.Selection = Sessions.Selection.empty) { if (Build.build_logic(options, logic, build_heap = true, progress = progress, dirs = dirs ::: select_dirs, system_mode = system_mode) != 0) error(logic + " FAILED") val dump_options = make_options(options, aspects) - def consume( - deps: Sessions.Deps, - snapshot: Document.Snapshot, - node_status: Document_Status.Node_Status) - { - val aspect_args = Aspect_Args(dump_options, progress, deps, output_dir, snapshot, node_status) - aspects.foreach(_.operation(aspect_args)) - } + val deps = + dependencies(dump_options, progress = progress, + dirs = dirs, select_dirs = select_dirs, selection = selection)._1 - session(dump_options, logic, consume _, - progress = progress, log = log, dirs = dirs, select_dirs = select_dirs, selection = selection) + val resources = + Headless.Resources.make(dump_options, logic, progress = progress, log = log, + session_dirs = dirs ::: select_dirs, + include_sessions = deps.sessions_structure.imports_topological_order) + + session(deps, resources, progress = progress, + process_theory = + (deps: Sessions.Deps, snapshot: Document.Snapshot, status: Document_Status.Node_Status) => + { + val aspect_args = Aspect_Args(dump_options, progress, deps, output_dir, snapshot, status) + aspects.foreach(_.operation(aspect_args)) + }) } @@ -256,24 +297,21 @@ val progress = new Console_Progress(verbose = verbose) - val ok = - progress.interrupt_handler { - dump(options, logic, - aspects = aspects, - progress = progress, - dirs = dirs, - select_dirs = select_dirs, - output_dir = output_dir, - selection = Sessions.Selection( - requirements = requirements, - all_sessions = all_sessions, - base_sessions = base_sessions, - exclude_session_groups = exclude_session_groups, - exclude_sessions = exclude_sessions, - session_groups = session_groups, - sessions = sessions)) - } - - if (!ok) sys.exit(2) + progress.interrupt_handler { + dump(options, logic, + aspects = aspects, + progress = progress, + dirs = dirs, + select_dirs = select_dirs, + output_dir = output_dir, + selection = Sessions.Selection( + requirements = requirements, + all_sessions = all_sessions, + base_sessions = base_sessions, + exclude_session_groups = exclude_session_groups, + exclude_sessions = exclude_sessions, + session_groups = session_groups, + sessions = sessions)) + } }) } diff -r 1ae0c822682c -r da2726f78610 src/Pure/Tools/server_commands.scala --- a/src/Pure/Tools/server_commands.scala Sat Dec 29 17:38:29 2018 +0100 +++ b/src/Pure/Tools/server_commands.scala Sat Dec 29 18:45:57 2018 +0100 @@ -113,15 +113,9 @@ try { Session_Build.command(args.build, progress = progress)._3 } catch { case exn: Server.Error => error(exn.message) } - val session = - Headless.start_session( - base_info.options, - base_info.session, - session_dirs = base_info.dirs, - session_base = Some(base_info.check_base), - print_mode = args.print_mode, - progress = progress, - log = log) + val resources = Headless.Resources(base_info, log = log) + + val session = resources.start_session(print_mode = args.print_mode, progress = progress) val id = UUID.random()