--- 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}
--- 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"
--- 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"
--- 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
--- 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 \<open>
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.
--- 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";
--- 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,
--- 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;
--- 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;
--- 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;
--- 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)
--- 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
}
}