# HG changeset patch # User wenzelm # Date 1596746620 -7200 # Node ID 7b318273a4aa6658514d761958db94c059733eaf # Parent c65614b556b2c9e46590e875ecedf07210cb4c65 discontinued old batch-build functionality; diff -r c65614b556b2 -r 7b318273a4aa CONTRIBUTORS --- a/CONTRIBUTORS Thu Aug 06 17:51:37 2020 +0200 +++ b/CONTRIBUTORS Thu Aug 06 22:43:40 2020 +0200 @@ -10,8 +10,7 @@ Integration of Metis 2.4. * June 2020: Makarius Wenzel - System option pide_session is enabled by default, notably for standard - "isabelle build" to invoke Scala from ML. + Batch-builds via "isabelle build" allow to invoke Scala from ML. * May 2020: Makarius Wenzel Antiquotations for Isabelle systems programming, notably @{scala_function} diff -r c65614b556b2 -r 7b318273a4aa NEWS --- a/NEWS Thu Aug 06 17:51:37 2020 +0200 +++ b/NEWS Thu Aug 06 22:43:40 2020 +0200 @@ -130,10 +130,10 @@ *** System *** -* System option "pide_session" is enabled by default, notably for -standard "isabelle build": it allows to invoke Isabelle/Scala operations -from Isabelle/ML. Big build jobs (e.g. AFP) require extra heap space for -the java process, e.g. like this in $ISABELLE_HOME_USER/etc/settings: +* Batch-builds via "isabelle build" use a PIDE session with special +protocol: this allows to invoke Isabelle/Scala operations from +Isabelle/ML. Big build jobs (e.g. AFP) require extra heap space for the +java process, e.g. like this in $ISABELLE_HOME_USER/etc/settings: ISABELLE_TOOL_JAVA_OPTIONS="$ISABELLE_TOOL_JAVA_OPTIONS -Xmx8g" diff -r c65614b556b2 -r 7b318273a4aa etc/options --- a/etc/options Thu Aug 06 17:51:37 2020 +0200 +++ b/etc/options Thu Aug 06 22:43:40 2020 +0200 @@ -150,9 +150,6 @@ section "PIDE Build" -option pide_session : bool = true - -- "build session heaps via PIDE" - option pide_reports : bool = true -- "report PIDE markup" diff -r c65614b556b2 -r 7b318273a4aa src/Doc/ROOT --- a/src/Doc/ROOT Thu Aug 06 17:51:37 2020 +0200 +++ b/src/Doc/ROOT Thu Aug 06 22:43:40 2020 +0200 @@ -378,7 +378,7 @@ "root.tex" session System (doc) in "System" = Pure + - options [document_variants = "system", thy_output_source, pide_session] + options [document_variants = "system", thy_output_source] sessions "HOL-Library" theories diff -r c65614b556b2 -r 7b318273a4aa src/Doc/System/Scala.thy --- a/src/Doc/System/Scala.thy Thu Aug 06 17:51:37 2020 +0200 +++ b/src/Doc/System/Scala.thy Thu Aug 06 22:43:40 2020 +0200 @@ -202,8 +202,7 @@ text \ Isabelle/PIDE provides a protocol to invoke registered Scala functions in - ML: this requires a proper PIDE session context, e.g.\ within the Prover IDE - or in batch builds via option @{system_option pide_session}. + ML: this works both within the Prover IDE and in batch builds. The subsequent ML antiquotations refer to Scala functions in a formally-checked manner. diff -r c65614b556b2 -r 7b318273a4aa src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Thu Aug 06 17:51:37 2020 +0200 +++ b/src/Pure/PIDE/markup.ML Thu Aug 06 22:43:40 2020 +0200 @@ -165,10 +165,7 @@ val cpuN: string val gcN: string val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T - val parse_timing_properties: Properties.T -> {elapsed: Time.time, cpu: Time.time, gc: Time.time} val command_timingN: string - val command_timing_properties: - {file: string, offset: int, name: string} -> Time.time -> Properties.T val parse_command_timing_properties: Properties.T -> ({file: string, offset: int, name: string} * Time.time) option val timingN: string val timing: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> T @@ -225,7 +222,6 @@ val theory_timing: Properties.entry val session_timing: Properties.entry val loading_theory: string -> Properties.T - val dest_loading_theory: Properties.T -> string option val build_session_finished: Properties.T val print_operationsN: string val print_operations: Properties.T @@ -589,11 +585,6 @@ (cpuN, Value.print_time cpu), (gcN, Value.print_time gc)]; -fun parse_timing_properties props = - {elapsed = Properties.seconds props elapsedN, - cpu = Properties.seconds props cpuN, - gc = Properties.seconds props gcN}; - val timingN = "timing"; fun timing t = (timingN, timing_properties t); @@ -602,10 +593,6 @@ val command_timingN = "command_timing"; -fun command_timing_properties {file, offset, name} elapsed = - [(fileN, file), (offsetN, Value.print_int offset), - (nameN, name), (elapsedN, Value.print_time elapsed)]; - fun parse_command_timing_properties props = (case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of (SOME file, SOME offset, SOME name) => @@ -710,9 +697,6 @@ fun loading_theory name = [("function", "loading_theory"), ("name", name)]; -fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name - | dest_loading_theory _ = NONE; - val build_session_finished = [("function", "build_session_finished")]; val print_operationsN = "print_operations"; diff -r c65614b556b2 -r 7b318273a4aa src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Thu Aug 06 17:51:37 2020 +0200 +++ b/src/Pure/PIDE/protocol.ML Thu Aug 06 22:43:40 2020 +0200 @@ -32,8 +32,7 @@ YXML.parse_body #> let open XML.Decode in list (pair string properties) end; in Resources.init_session - {pide = true, - session_positions = decode_sessions session_positions_yxml, + {session_positions = decode_sessions session_positions_yxml, session_directories = decode_table session_directories_yxml, docs = decode_list doc_names_yxml, global_theories = decode_table global_theories_yxml, diff -r c65614b556b2 -r 7b318273a4aa src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Thu Aug 06 17:51:37 2020 +0200 +++ b/src/Pure/PIDE/resources.ML Thu Aug 06 22:43:40 2020 +0200 @@ -8,14 +8,12 @@ sig val default_qualifier: string val init_session: - {pide: bool, - session_positions: (string * Properties.T) list, + {session_positions: (string * Properties.T) list, session_directories: (string * string) list, docs: string list, global_theories: (string * string) list, loaded_theories: string list} -> unit val finish_session_base: unit -> unit - val is_pide: unit -> bool val global_theory: string -> string option val loaded_theory: string -> bool val check_session: Proof.context -> string * Position.T -> string @@ -54,8 +52,7 @@ {pos = Position.of_properties props, serial = serial ()}; val empty_session_base = - {pide = false, - session_positions = []: (string * entry) list, + {session_positions = []: (string * entry) list, session_directories = Symtab.empty: Path.T list Symtab.table, docs = []: (string * entry) list, global_theories = Symtab.empty: string Symtab.table, @@ -65,11 +62,10 @@ Synchronized.var "Sessions.base" empty_session_base; fun init_session - {pide, session_positions, session_directories, docs, global_theories, loaded_theories} = + {session_positions, session_directories, docs, global_theories, loaded_theories} = Synchronized.change global_session_base (fn _ => - {pide = pide, - session_positions = sort_by #1 (map (apsnd make_entry) session_positions), + {session_positions = sort_by #1 (map (apsnd make_entry) session_positions), session_directories = fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir)) session_directories Symtab.empty, @@ -80,8 +76,7 @@ fun finish_session_base () = Synchronized.change global_session_base (fn {global_theories, loaded_theories, ...} => - {pide = false, - session_positions = [], + {session_positions = [], session_directories = Symtab.empty, docs = [], global_theories = global_theories, @@ -89,8 +84,6 @@ fun get_session_base f = f (Synchronized.value global_session_base); -fun is_pide () = get_session_base #pide; - fun global_theory a = Symtab.lookup (get_session_base #global_theories) a; fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a; diff -r c65614b556b2 -r 7b318273a4aa src/Pure/System/scala.ML --- a/src/Pure/System/scala.ML Thu Aug 06 17:51:37 2020 +0200 +++ b/src/Pure/System/scala.ML Thu Aug 06 22:43:40 2020 +0200 @@ -33,7 +33,6 @@ fun promise_function name arg = let - val _ = if Resources.is_pide () then () else raise Fail "PIDE session required"; val id = new_id (); fun abort () = Output.protocol_message (Markup.cancel_scala id) []; val promise = Future.promise_name "invoke_scala" abort : string future; diff -r c65614b556b2 -r 7b318273a4aa src/Pure/Thy/export.ML --- a/src/Pure/Thy/export.ML Thu Aug 06 17:51:37 2020 +0200 +++ b/src/Pure/Thy/export.ML Thu Aug 06 22:43:40 2020 +0200 @@ -16,7 +16,6 @@ val export_executable_file: theory -> Path.binding -> Path.T -> unit val markup: theory -> Path.T -> Markup.T val message: theory -> Path.T -> string - val protocol_message: Output.protocol_message_fn end; structure Export: EXPORT = @@ -71,24 +70,4 @@ fun message thy path = "See " ^ Markup.markup (markup thy path) "theory exports"; - -(* protocol message (bootstrap) *) - -fun protocol_message props body = - (case props of - function :: args => - if function = (Markup.functionN, Markup.exportN) andalso - not (null args) andalso #1 (hd args) = Markup.idN - then - let - val path = Path.expand (Path.explode ("$ISABELLE_EXPORT_TMP/export" ^ serial_string ())); - val _ = YXML.write_body path body; - in Protocol_Message.marker (#2 function) (tl args @ [(Markup.fileN, Path.implode path)]) end - else raise Output.Protocol_Message props - | [] => raise Output.Protocol_Message props); - -val _ = - if Thread_Data.is_virtual then () - else Private_Output.protocol_message_fn := protocol_message; - end; diff -r c65614b556b2 -r 7b318273a4aa src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Thu Aug 06 17:51:37 2020 +0200 +++ b/src/Pure/Tools/build.ML Thu Aug 06 22:43:40 2020 +0200 @@ -4,12 +4,7 @@ Build Isabelle sessions. *) -signature BUILD = -sig - val build: string -> unit -end; - -structure Build: BUILD = +structure Build: sig end = struct (* command timings *) @@ -58,39 +53,6 @@ in y end; -(* protocol messages *) - -fun protocol_message props output = - (case props of - function :: args => - if function = Markup.ML_statistics orelse function = Markup.task_statistics then - Protocol_Message.marker (#2 function) args - else if function = Markup.command_timing then - let - val name = the_default "" (Properties.get args Markup.nameN); - val pos = Position.of_properties args; - val {elapsed, ...} = Markup.parse_timing_properties args; - val is_significant = - Timing.is_relevant_time elapsed andalso - elapsed >= Options.default_seconds "command_timing_threshold"; - in - if is_significant then - (case approximative_id name pos of - SOME id => - Protocol_Message.marker (#2 function) - (Markup.command_timing_properties id elapsed) - | NONE => ()) - else () - end - else if function = Markup.theory_timing orelse function = Markup.session_timing then - Protocol_Message.marker (#2 function) args - else - (case Markup.dest_loading_theory props of - SOME name => Protocol_Message.marker_text "loading_theory" name - | NONE => Export.protocol_message props output) - | [] => raise Output.Protocol_Message props); - - (* build theories *) fun build_theories symbols bibtex_entries last_timing qualifier master_dir (options, thys) = @@ -122,127 +84,72 @@ (* build session *) -datatype args = Args of - {pide: bool, - symbol_codes: (string * int) list, - command_timings: Properties.T list, - verbose: bool, - browser_info: Path.T, - document_files: (Path.T * Path.T) list, - graph_file: Path.T, - parent_name: string, - chapter: string, - session_name: string, - master_dir: Path.T, - theories: (Options.T * (string * Position.T) list) list, - session_positions: (string * Properties.T) list, - session_directories: (string * string) list, - doc_names: string list, - global_theories: (string * string) list, - loaded_theories: string list, - bibtex_entries: string list}; - -fun decode_args pide yxml = - let - open XML.Decode; - val position = Position.of_properties o properties; - val (symbol_codes, (command_timings, (verbose, (browser_info, - (document_files, (graph_file, (parent_name, (chapter, (session_name, (master_dir, - (theories, (session_positions, (session_directories, (doc_names, (global_theories, - (loaded_theories, bibtex_entries)))))))))))))))) = - pair (list (pair string int)) (pair (list properties) (pair bool (pair string - (pair (list (pair string string)) (pair string (pair string (pair string (pair string - (pair string - (pair (((list (pair Options.decode (list (pair string position)))))) - (pair (list (pair string properties)) - (pair (list (pair string string)) (pair (list string) - (pair (list (pair string string)) (pair (list string) (list string)))))))))))))))) - (YXML.parse_body yxml); - in - Args {pide = pide, symbol_codes = symbol_codes, command_timings = command_timings, - verbose = verbose, browser_info = Path.explode browser_info, - document_files = map (apply2 Path.explode) document_files, - graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter, - session_name = session_name, master_dir = Path.explode master_dir, theories = theories, - session_positions = session_positions, session_directories = session_directories, - doc_names = doc_names, global_theories = global_theories, loaded_theories = loaded_theories, - bibtex_entries = bibtex_entries} - end; - -fun build_session (Args {pide, symbol_codes, command_timings, verbose, browser_info, document_files, - graph_file, parent_name, chapter, session_name, master_dir, theories, session_positions, - session_directories, doc_names, global_theories, loaded_theories, bibtex_entries}) = - let - val symbols = HTML.make_symbols symbol_codes; - - val _ = - Resources.init_session - {pide = pide, - session_positions = session_positions, - session_directories = session_directories, - docs = doc_names, - global_theories = global_theories, - loaded_theories = loaded_theories}; - - val _ = - Session.init - symbols - (Options.default_bool "browser_info") - browser_info - (Options.default_string "document") - (Options.default_string "document_output") - (Present.document_variants (Options.default ())) - document_files - graph_file - parent_name - (chapter, session_name) - verbose; - - val last_timing = get_timings (fold update_timings command_timings empty_timings); - - val res1 = - theories |> - (List.app (build_theories symbols bibtex_entries last_timing session_name master_dir) - |> session_timing - |> Exn.capture); - val res2 = Exn.capture Session.finish (); - - val _ = Resources.finish_session_base (); - val _ = Par_Exn.release_all [res1, res2]; - val _ = - if session_name = Context.PureN - then Theory.install_pure (Thy_Info.get_theory Context.PureN) else (); - in () end; - - -(* command-line tool *) - -fun inline_errors exn = - Runtime.exn_message_list exn - |> List.app (fn msg => Protocol_Message.marker_text "error_message" (YXML.content_of msg)); - -fun build args_file = - let - val _ = SHA1.test_samples (); - val _ = Options.load_default (); - val _ = Isabelle_Process.init_options (); - val args = decode_args false (File.read (Path.explode args_file)); - val _ = - Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message - build_session args - handle exn => (inline_errors exn; Exn.reraise exn); - val _ = Private_Output.protocol_message_fn := Output.protocol_message_undefined; - val _ = Options.reset_default (); - in () end; - - -(* PIDE version *) - val _ = Isabelle_Process.protocol_command "build_session" (fn [args_yxml] => let - val args = decode_args true args_yxml; + val (symbol_codes, (command_timings, (verbose, (browser_info, + (document_files, (graph_file, (parent_name, (chapter, (session_name, (master_dir, + (theories, (session_positions, (session_directories, (doc_names, (global_theories, + (loaded_theories, bibtex_entries)))))))))))))))) = + YXML.parse_body args_yxml |> + let + open XML.Decode; + val position = Position.of_properties o properties; + val path = Path.explode o string; + in + pair (list (pair string int)) (pair (list properties) (pair bool (pair path + (pair (list (pair path path)) (pair path (pair string (pair string (pair string + (pair path + (pair (((list (pair Options.decode (list (pair string position)))))) + (pair (list (pair string properties)) + (pair (list (pair string string)) (pair (list string) + (pair (list (pair string string)) (pair (list string) (list string)))))))))))))))) + end; + + val symbols = HTML.make_symbols symbol_codes; + + fun build () = + let + val _ = + Resources.init_session + {session_positions = session_positions, + session_directories = session_directories, + docs = doc_names, + global_theories = global_theories, + loaded_theories = loaded_theories}; + + val _ = + Session.init + symbols + (Options.default_bool "browser_info") + browser_info + (Options.default_string "document") + (Options.default_string "document_output") + (Present.document_variants (Options.default ())) + document_files + graph_file + parent_name + (chapter, session_name) + verbose; + + val last_timing = get_timings (fold update_timings command_timings empty_timings); + + val res1 = + theories |> + (List.app + (build_theories symbols bibtex_entries last_timing session_name master_dir) + |> session_timing + |> Exn.capture); + val res2 = Exn.capture Session.finish (); + + val _ = Resources.finish_session_base (); + val _ = Par_Exn.release_all [res1, res2]; + val _ = + if session_name = Context.PureN + then Theory.install_pure (Thy_Info.get_theory Context.PureN) else (); + in () end; + fun exec e = if can Theory.get_pure () then Isabelle_Thread.fork @@ -252,7 +159,7 @@ else e (); in exec (fn () => - (Future.interruptible_task (fn () => (build_session args; (0, []))) () handle exn => + (Future.interruptible_task (fn () => (build (); (0, []))) () handle exn => ((1, Runtime.exn_message_list exn) handle _ (*sic!*) => (2, ["CRASHED"]))) |> let open XML.Encode in pair int (list string) end |> Output.protocol_message Markup.build_session_finished) diff -r c65614b556b2 -r 7b318273a4aa src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Thu Aug 06 17:51:37 2020 +0200 +++ b/src/Pure/Tools/build.scala Thu Aug 06 22:43:40 2020 +0200 @@ -160,7 +160,7 @@ do_store: Boolean, verbose: Boolean, val numa_node: Option[Int], - command_timings: List[Properties.T]) + command_timings0: List[Properties.T]) { val options: Options = NUMA.policy_options(info.options, numa_node) @@ -189,7 +189,7 @@ pair(list(pair(string, string)), pair(list(string), pair(list(pair(string, string)), pair(list(string), list(string)))))))))))))))))( - (Symbol.codes, (command_timings, (verbose, + (Symbol.codes, (command_timings0, (verbose, (store.browser_info, (info.document_files, (File.standard_path(graph_file), (parent, (info.chapter, (session_name, (Path.current, (info.theories, @@ -216,205 +216,164 @@ } else Nil - if (options.bool("pide_session") || true /* FIXME test */) { - val resources = new Resources(sessions_structure, deps(parent)) - val session = - new Session(options, resources) { - override val xml_cache: XML.Cache = store.xml_cache - override val xz_cache: XZ.Cache = store.xz_cache + val resources = new Resources(sessions_structure, deps(parent)) + val session = + new Session(options, resources) { + override val xml_cache: XML.Cache = store.xml_cache + override val xz_cache: XZ.Cache = store.xz_cache + } + + 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 stdout = 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 } - object Build_Session_Errors - { - private val promise: Promise[List[String]] = Future.promise + private def loading_theory(msg: Prover.Protocol_Output): Boolean = + msg.properties match { + case Markup.Loading_Theory(name) => + progress.theory(Progress.Theory(name, session = session_name)) + true + 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 + } + + val functions = + List( + Markup.Build_Session_Finished.name -> build_session_finished, + Markup.Loading_Theory.name -> loading_theory, + Markup.EXPORT -> export, + fun(Markup.Command_Timing.name, command_timings, Markup.Command_Timing.unapply), + fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply), + fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply), + fun(Markup.ML_Statistics.name, runtime_statistics, Markup.ML_Statistics.unapply), + fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply)) + }) - 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 => } + 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 (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 errors = + Isabelle_Thread.interrupt_handler(_ => process.terminate) { + Exn.capture { process.await_startup } match { + case Exn.Res(_) => + session.protocol_command("build_session", args_yxml) + Build_Session_Errors.result + case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn))) } } - val stdout = 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(name) => - progress.theory(Progress.Theory(name, session = session_name)) - true - 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 - } - - val functions = - List( - Markup.Build_Session_Finished.name -> build_session_finished, - Markup.Loading_Theory.name -> loading_theory, - Markup.EXPORT -> export, - fun(Markup.Command_Timing.name, command_timings, Markup.Command_Timing.unapply), - fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply), - fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply), - fun(Markup.ML_Statistics.name, runtime_statistics, Markup.ML_Statistics.unapply), - fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply)) - }) + val process_result = + Isabelle_Thread.interrupt_handler(_ => process.terminate) { process.await_shutdown } + val process_output = + 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) - 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 (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 errors = - Isabelle_Thread.interrupt_handler(_ => process.terminate) { - Exn.capture { process.await_startup } match { - case Exn.Res(_) => - session.protocol_command("build_session", 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 } - val process_output = - 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) + val result = process_result.output(process_output) - val result = process_result.output(process_output) - - errors match { - case Exn.Res(Nil) => result - case Exn.Res(errs) => - 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 - } - } - else { - val args_file = Isabelle_System.tmp_file("build") - File.write(args_file, args_yxml) - - val eval_build = - "Build.build " + ML_Syntax.print_string_bytes(File.standard_path(args_file)) - val eval_main = Command_Line.ML_tool(eval_build :: eval_store) - - val process = - ML_Process(options, deps.sessions_structure, store, - logic = parent, raw_ml_system = is_pure, - use_prelude = use_prelude, eval_main = eval_main, - cwd = info.dir.file, env = env, cleanup = () => args_file.delete) - - Isabelle_Thread.interrupt_handler(_ => process.terminate) { - process.result( - progress_stdout = - { - case Protocol.Loading_Theory_Marker(theory) => - progress.theory(Progress.Theory(theory, session = session_name)) - case Protocol.Export.Marker((args, path)) => - val body = - try { Bytes.read(path) } - catch { - case ERROR(msg) => - error("Failed to read export " + quote(args.compound_name) + "\n" + msg) - } - path.file.delete - export_consumer(session_name, args, body) - case _ => - }, - progress_limit = - options.int("process_output_limit") match { - case 0 => None - case m => Some(m * 1000000L) - }, - strict = false) - } + errors match { + case Exn.Res(Nil) => result + case Exn.Res(errs) => + 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 } }