diff --git a/src/Pure/PIDE/protocol_message.scala b/src/Pure/PIDE/protocol_message.scala --- a/src/Pure/PIDE/protocol_message.scala +++ b/src/Pure/PIDE/protocol_message.scala @@ -1,112 +1,120 @@ /* Title: Pure/PIDE/protocol_message.scala Author: Makarius Auxiliary operations on protocol messages. */ package isabelle object Protocol_Message { /* message markers */ object Marker { def apply(a: String): Marker = new Marker { override def name: String = a } def test(line: String): Boolean = line.startsWith("\f") } abstract class Marker private { def name: String val prefix: String = "\f" + name + " = " def apply(text: String): String = prefix + Library.encode_lines(text) def apply(props: Properties.T): String = apply(YXML.string_of_body(XML.Encode.properties(props))) def test(line: String): Boolean = line.startsWith(prefix) def test_yxml(line: String): Boolean = test(line) && YXML.detect(line) def unapply(line: String): Option[String] = Library.try_unprefix(prefix, line).map(Library.decode_lines) override def toString: String = "Marker(" + quote(name) + ")" } /* inlined reports */ private val report_elements = Markup.Elements(Markup.REPORT, Markup.NO_REPORT) def clean_reports(body: XML.Body): XML.Body = body filter { case XML.Wrapped_Elem(Markup(name, _), _, _) => !report_elements(name) case XML.Elem(Markup(name, _), _) => !report_elements(name) case _ => true } map { case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_reports(ts)) case XML.Elem(markup, ts) => XML.Elem(markup, clean_reports(ts)) case t => t } + def expose_no_reports(body: XML.Body): XML.Body = + body flatMap { + case XML.Wrapped_Elem(markup, body, ts) => List(XML.Wrapped_Elem(markup, body, expose_no_reports(ts))) + case XML.Elem(Markup(Markup.NO_REPORT, _), ts) => ts + case XML.Elem(markup, ts) => List(XML.Elem(markup, expose_no_reports(ts))) + case t => List(t) + } + def reports(props: Properties.T, body: XML.Body): List[XML.Elem] = body flatMap { case XML.Wrapped_Elem(Markup(Markup.REPORT, ps), body, ts) => List(XML.Wrapped_Elem(Markup(Markup.REPORT, props ::: ps), body, ts)) case XML.Elem(Markup(Markup.REPORT, ps), ts) => List(XML.Elem(Markup(Markup.REPORT, props ::: ps), ts)) case XML.Wrapped_Elem(_, _, ts) => reports(props, ts) case XML.Elem(_, ts) => reports(props, ts) case XML.Text(_) => Nil } /* reported positions */ private val position_elements = Markup.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION) def positions( self_id: Document_ID.Generic => Boolean, command_position: Position.T, chunk_name: Symbol.Text_Chunk.Name, chunk: Symbol.Text_Chunk, message: XML.Elem): Set[Text.Range] = { def elem(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] = props match { case Position.Identified(id, name) if self_id(id) && name == chunk_name => val opt_range = Position.Range.unapply(props) orElse { if (name == Symbol.Text_Chunk.Default) Position.Range.unapply(command_position) else None } opt_range match { case Some(symbol_range) => chunk.incorporate(symbol_range) match { case Some(range) => set + range case _ => set } case None => set } case _ => set } def tree(set: Set[Text.Range], t: XML.Tree): Set[Text.Range] = t match { case XML.Wrapped_Elem(Markup(name, props), _, body) => body.foldLeft(if (position_elements(name)) elem(props, set) else set)(tree) case XML.Elem(Markup(name, props), body) => body.foldLeft(if (position_elements(name)) elem(props, set) else set)(tree) case XML.Text(_) => set } val set = tree(Set.empty, message) if (set.isEmpty) elem(message.markup.properties, set) else set } } diff --git a/src/Pure/System/command_line.ML b/src/Pure/System/command_line.ML --- a/src/Pure/System/command_line.ML +++ b/src/Pure/System/command_line.ML @@ -1,27 +1,30 @@ (* Title: Pure/System/command_line.ML Author: Makarius Support for Isabelle/ML command line tools. *) signature COMMAND_LINE = sig + exception EXIT of int val tool: (unit -> int) -> unit val tool0: (unit -> unit) -> unit end; structure Command_Line: COMMAND_LINE = struct +exception EXIT of int; + fun tool body = Thread_Attributes.uninterruptible (fn restore_attributes => fn () => let val rc = - restore_attributes body () handle exn => - Exn.capture_exit 2 (fn () => (Runtime.exn_error_message exn; raise exn)) (); + restore_attributes body () + handle EXIT rc => rc + | exn => Exn.capture_exit 2 (fn () => (Runtime.exn_error_message exn; raise exn)) (); in exit rc end) (); fun tool0 body = tool (fn () => (body (); 0)); end; - diff --git a/src/Pure/System/isabelle_process.ML b/src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML +++ b/src/Pure/System/isabelle_process.ML @@ -1,231 +1,234 @@ (* Title: Pure/System/isabelle_process.ML Author: Makarius Isabelle process wrapper. *) signature ISABELLE_PROCESS = sig val is_active: unit -> bool val protocol_command: string -> (string list -> unit) -> unit val reset_tracing: Document_ID.exec -> unit + exception EXIT of exn val crashes: exn list Synchronized.var val init_options: unit -> unit val init_options_interactive: unit -> unit val init: unit -> unit end; structure Isabelle_Process: ISABELLE_PROCESS = struct (* print mode *) val isabelle_processN = "isabelle_process"; fun is_active () = Print_Mode.print_mode_active isabelle_processN; val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape; val _ = Markup.add_mode isabelle_processN YXML.output_markup; (* protocol commands *) local val commands = Synchronized.var "Isabelle_Process.commands" (Symtab.empty: (string list -> unit) Symtab.table); in fun protocol_command name cmd = Synchronized.change commands (fn cmds => (if not (Symtab.defined cmds name) then () else warning ("Redefining Isabelle protocol command " ^ quote name); Symtab.update (name, cmd) cmds)); fun run_command name args = (case Symtab.lookup (Synchronized.value commands) name of NONE => error ("Undefined Isabelle protocol command " ^ quote name) | SOME cmd => (Runtime.exn_trace_system (fn () => cmd args) handle _ (*sic!*) => error ("Isabelle protocol command failure: " ^ quote name))); end; (* restricted tracing messages *) val tracing_messages = Synchronized.var "tracing_messages" (Inttab.empty: int Inttab.table); fun reset_tracing exec_id = Synchronized.change tracing_messages (Inttab.delete_safe exec_id); fun update_tracing () = (case Position.parse_id (Position.thread_data ()) of NONE => () | SOME exec_id => let val ok = Synchronized.change_result tracing_messages (fn tab => let val n = the_default 0 (Inttab.lookup tab exec_id) + 1; val limit = Options.default_int "editor_tracing_messages"; val ok = limit <= 0 orelse n <= limit; in (ok, Inttab.update (exec_id, n) tab) end); in if ok then () else let val (text, promise) = Active.dialog_text (); val _ = writeln ("Tracing paused. " ^ text "Stop" ^ ", or continue with next " ^ text "100" ^ ", " ^ text "1000" ^ ", " ^ text "10000" ^ " messages?") val m = Value.parse_int (Future.join promise) handle Fail _ => error "Stopped"; in Synchronized.change tracing_messages (Inttab.map_default (exec_id, 0) (fn k => k - m)) end end); (* output channels *) val serial_props = Markup.serial_properties o serial; fun init_channels out_stream = let val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF); val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF); val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF); val msg_channel = Message_Channel.make out_stream; fun message name props body = Message_Channel.send msg_channel (Message_Channel.message name props body); fun standard_message props name ss = if forall (fn s => s = "") ss then () else let val props' = (case (Properties.defined props Markup.idN, Position.get_id (Position.thread_data ())) of (false, SOME id') => props @ [(Markup.idN, id')] | _ => props); in message name props' (XML.blob ss) end; in Private_Output.status_fn := standard_message [] Markup.statusN; Private_Output.report_fn := standard_message [] Markup.reportN; Private_Output.result_fn := (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s); Private_Output.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s); Private_Output.state_fn := (fn s => standard_message (serial_props ()) Markup.stateN s); Private_Output.information_fn := (fn s => standard_message (serial_props ()) Markup.informationN s); Private_Output.tracing_fn := (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s)); Private_Output.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s); Private_Output.legacy_fn := (fn s => standard_message (serial_props ()) Markup.legacyN s); Private_Output.error_message_fn := (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s); Private_Output.system_message_fn := (fn ss => message Markup.systemN [] (XML.blob ss)); Private_Output.protocol_message_fn := (fn props => fn body => message Markup.protocolN props body); Session.init_protocol_handlers (); message Markup.initN [] [XML.Text (Session.welcome ())]; msg_channel end; (* protocol loop -- uninterruptible *) +exception EXIT of exn; + val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list); local fun recover crash = (Synchronized.change crashes (cons crash); Output.physical_stderr "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n"); +fun shutdown () = (Future.shutdown (); ignore (Execution.reset ())); + in fun loop stream = let val continue = (case Byte_Message.read_message stream of NONE => false | SOME [] => (Output.system_message "Isabelle process: no input"; true) | SOME (name :: args) => (run_command name args; true)) - handle exn => (Runtime.exn_system_message exn handle crash => recover crash; true); - in - if continue then loop stream - else (Future.shutdown (); Execution.reset (); ()) - end; + handle EXIT exn => (shutdown (); Exn.reraise exn) + | exn => (Runtime.exn_system_message exn handle crash => recover crash; true); + in if continue then loop stream else shutdown () end; end; (* init protocol *) val default_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN]; val default_modes2 = [isabelle_processN, Pretty.symbolicN]; val init_protocol = Thread_Attributes.uninterruptible (fn _ => fn (address, password) => let val _ = SHA1.test_samples () handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn); val _ = Output.physical_stderr Symbol.STX; val _ = Context.put_generic_context NONE; val _ = Unsynchronized.change print_mode (fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2); val (in_stream, out_stream) = Socket_IO.open_streams address; val _ = Byte_Message.write_line out_stream password; val msg_channel = init_channels out_stream; val _ = loop in_stream; val _ = Message_Channel.shutdown msg_channel; val _ = Private_Output.init_channels (); val _ = print_mode := []; in () end); (* init options *) fun init_options () = (ML_Print_Depth.set_print_depth (Options.default_int "ML_print_depth"); Future.ML_statistics := Options.default_bool "ML_statistics"; Multithreading.trace := Options.default_int "threads_trace"; Multithreading.max_threads_update (Options.default_int "threads"); Multithreading.parallel_proofs := Options.default_int "parallel_proofs"; if Options.default_bool "export_standard_proofs" then Proofterm.proofs := 2 else (); let val proofs = Options.default_int "record_proofs" in if proofs < 0 then () else Proofterm.proofs := proofs end; Printer.show_markup_default := false); fun init_options_interactive () = (init_options (); Multithreading.parallel_proofs := (if Options.default_int "parallel_proofs" > 0 then 3 else 0); Printer.show_markup_default := true); (* generic init *) fun init () = let val address = Options.default_string \<^system_option>\system_channel_address\; val password = Options.default_string \<^system_option>\system_channel_password\; in if address <> "" andalso password <> "" then init_protocol (address, password) else init_options () end; end; diff --git a/src/Pure/System/process_result.scala b/src/Pure/System/process_result.scala --- a/src/Pure/System/process_result.scala +++ b/src/Pure/System/process_result.scala @@ -1,51 +1,53 @@ /* Title: Pure/System/process_result.scala Author: Makarius Result of system process. */ package isabelle final case class Process_Result( rc: Int, out_lines: List[String] = Nil, err_lines: List[String] = Nil, timeout: Boolean = false, timing: Timing = Timing.zero) { def out: String = cat_lines(out_lines) def err: String = cat_lines(err_lines) + + def output(outs: List[String]): Process_Result = copy(out_lines = out_lines ::: outs) def errors(errs: List[String]): Process_Result = copy(err_lines = err_lines ::: errs) def error(err: String): Process_Result = errors(List(err)) def was_timeout: Process_Result = copy(rc = 1, timeout = true) def ok: Boolean = rc == 0 def interrupted: Boolean = rc == Exn.Interrupt.return_code def error_rc: Process_Result = if (interrupted) this else copy(rc = rc max 1) def check_rc(pred: Int => Boolean): Process_Result = if (pred(rc)) this else if (interrupted) throw Exn.Interrupt() else Exn.error(err) def check: Process_Result = check_rc(_ == 0) def print: Process_Result = { Output.warning(err) Output.writeln(out) copy(out_lines = Nil, err_lines = Nil) } def print_stdout: Process_Result = { Output.warning(err, stdout = true) Output.writeln(out, stdout = true) copy(out_lines = Nil, err_lines = Nil) } def print_if(b: Boolean): Process_Result = if (b) print else this def print_stdout_if(b: Boolean): Process_Result = if (b) print_stdout else this } diff --git a/src/Pure/Tools/build.ML b/src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML +++ b/src/Pure/Tools/build.ML @@ -1,254 +1,266 @@ (* Title: Pure/Tools/build.ML Author: Makarius Build Isabelle sessions. *) signature BUILD = sig val build: string -> unit end; structure Build: BUILD = struct (* command timings *) type timings = ((string * Time.time) Inttab.table) Symtab.table; (*file -> offset -> name, time*) val empty_timings: timings = Symtab.empty; fun update_timings props = (case Markup.parse_command_timing_properties props of SOME ({file, offset, name}, time) => Symtab.map_default (file, Inttab.empty) (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, t + time))) | NONE => I); fun approximative_id name pos = (case (Position.file_of pos, Position.offset_of pos) of (SOME file, SOME offset) => if name = "" then NONE else SOME {file = file, offset = offset, name = name} | _ => NONE); fun get_timings timings tr = (case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of SOME {file, offset, name} => (case Symtab.lookup timings file of SOME offsets => (case Inttab.lookup offsets offset of SOME (name', time) => if name = name' then SOME time else NONE | NONE => NONE) | NONE => NONE) | NONE => NONE) |> the_default Time.zeroTime; (* session timing *) fun session_timing name verbose f x = let val start = Timing.start (); val y = f x; val timing = Timing.result start; val threads = string_of_int (Multithreading.max_threads ()); val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing) |> Real.fmt (StringCvt.FIX (SOME 2)); val timing_props = [("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)]; val _ = Protocol_Message.marker "Timing" timing_props; val _ = if verbose then Output.physical_stderr ("Timing " ^ name ^ " (" ^ threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n") else (); 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 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) = let val context = {options = options, symbols = symbols, bibtex_entries = bibtex_entries, last_timing = last_timing}; val condition = space_explode "," (Options.string options "condition"); val conds = filter_out (can getenv_strict) condition; in if null conds then (Options.set_default options; Isabelle_Process.init_options (); Future.fork I; (Thy_Info.use_theories context qualifier master_dir |> (case Options.string options "profiling" of "" => I | "time" => profile_time | "allocations" => profile_allocations | bad => error ("Bad profiling option: " ^ quote bad)) |> Unsynchronized.setmp print_mode (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys) else Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^ " (undefined " ^ commas conds ^ ")\n") end; (* build session *) datatype args = Args of {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, 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 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, (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 {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, name = 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 {symbol_codes, command_timings, verbose, browser_info, document_files, graph_file, parent_name, chapter, 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_base {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, 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 name master_dir) |> session_timing name verbose |> Exn.capture); val res2 = Exn.capture Session.finish (); val _ = Resources.finish_session_base (); val _ = Par_Exn.release_all [res1, res2]; val _ = if 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)); -(*command-line tool*) fun build args_file = let val _ = SHA1.test_samples (); val _ = Options.load_default (); val _ = Isabelle_Process.init_options (); val args = decode_args (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*) + +(* PIDE version *) + +fun build_session_finished errs = + XML.Encode.list XML.Encode.string errs + |> Output.protocol_message Markup.build_session_finished; + val _ = Isabelle_Process.protocol_command "build_session" (fn [args_yxml] => let val args = decode_args args_yxml; - val result = (build_session args; "") handle exn => - (Runtime.exn_message exn handle _ (*sic!*) => - "Exception raised, but failed to print details!"); - in Output.protocol_message Markup.build_session_finished [XML.Text result] end + val errs = + Future.interruptible_task (fn () => + (build_session args; []) handle exn => + (Runtime.exn_message_list exn handle _ (*sic!*) => + (build_session_finished ["CRASHED"]; + raise Isabelle_Process.EXIT exn))) (); + val _ = build_session_finished errs; + in if null errs then () else raise Isabelle_Process.EXIT (Command_Line.EXIT 1) end | _ => raise Match); end; diff --git a/src/Pure/Tools/build.scala b/src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala +++ b/src/Pure/Tools/build.scala @@ -1,870 +1,873 @@ /* Title: Pure/Tools/build.scala Author: Makarius Options: :folding=explicit: Build and manage Isabelle sessions. */ package isabelle import scala.collection.SortedSet import scala.annotation.tailrec object Build { /** auxiliary **/ /* persistent build info */ sealed case class Session_Info( sources: String, input_heaps: List[String], output_heap: Option[String], return_code: Int) { def ok: Boolean = return_code == 0 } /* queue with scheduling information */ private object Queue { type Timings = (List[Properties.T], Double) def load_timings(progress: Progress, store: Sessions.Store, name: String): Timings = { val no_timings: Timings = (Nil, 0.0) store.access_database(name) match { case None => no_timings case Some(db) => def ignore_error(msg: String) = { progress.echo_warning("Ignoring bad database " + db + (if (msg == "") "" else "\n" + msg)) no_timings } try { val command_timings = store.read_command_timings(db, name) val session_timing = store.read_session_timing(db, name) match { case Markup.Elapsed(t) => t case _ => 0.0 } (command_timings, session_timing) } catch { case ERROR(msg) => ignore_error(msg) case exn: java.lang.Error => ignore_error(Exn.message(exn)) case _: XML.Error => ignore_error("") } finally { db.close } } } def make_session_timing(sessions_structure: Sessions.Structure, timing: Map[String, Double]) : Map[String, Double] = { val maximals = sessions_structure.build_graph.maximals.toSet def desc_timing(name: String): Double = { if (maximals.contains(name)) timing(name) else { val descendants = sessions_structure.build_descendants(List(name)).toSet val g = sessions_structure.build_graph.restrict(descendants) (0.0 :: g.maximals.flatMap(desc => { val ps = g.all_preds(List(desc)) if (ps.exists(p => timing.get(p).isEmpty)) None else Some(ps.map(timing(_)).sum) })).max } } timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0) } def apply(progress: Progress, sessions_structure: Sessions.Structure, store: Sessions.Store) : Queue = { val graph = sessions_structure.build_graph val names = graph.keys val timings = names.map(name => (name, load_timings(progress, store, name))) val command_timings = timings.map({ case (name, (ts, _)) => (name, ts) }).toMap.withDefaultValue(Nil) val session_timing = make_session_timing(sessions_structure, timings.map({ case (name, (_, t)) => (name, t) }).toMap) object Ordering extends scala.math.Ordering[String] { def compare_timing(name1: String, name2: String): Int = { val t1 = session_timing(name1) val t2 = session_timing(name2) if (t1 == 0.0 || t2 == 0.0) 0 else t1 compare t2 } def compare(name1: String, name2: String): Int = compare_timing(name2, name1) match { case 0 => sessions_structure(name2).timeout compare sessions_structure(name1).timeout match { case 0 => name1 compare name2 case ord => ord } case ord => ord } } new Queue(graph, SortedSet(names: _*)(Ordering), command_timings) } } private class Queue( graph: Graph[String, Sessions.Info], order: SortedSet[String], val command_timings: String => List[Properties.T]) { def is_inner(name: String): Boolean = !graph.is_maximal(name) def is_empty: Boolean = graph.is_empty def - (name: String): Queue = new Queue(graph.del_node(name), order - name, // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!? command_timings) def dequeue(skip: String => Boolean): Option[(String, Sessions.Info)] = { val it = order.iterator.dropWhile(name => skip(name) || !graph.defined(name) // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!? || !graph.is_minimal(name)) if (it.hasNext) { val name = it.next; Some((name, graph.get_node(name))) } else None } } /* PIDE protocol handler */ class Handler(progress: Progress, session: Session, session_name: String) extends Session.Protocol_Handler { - val result_error: Promise[String] = Future.promise + val build_session_errors: Promise[List[String]] = Future.promise - override def exit() { result_error.cancel } + override def exit() { build_session_errors.cancel } private def build_session_finished(msg: Prover.Protocol_Output): Boolean = { - val error_message = - try { Pretty.string_of(Symbol.decode_yxml(msg.text)) } - catch { case ERROR(msg) => msg } - result_error.fulfill(error_message) + val errors = + try { + XML.Decode.list(x => x)(Symbol.decode_yxml(msg.text)). + map(err => Pretty.string_of(Protocol_Message.expose_no_reports(err))) + } + catch { case ERROR(err) => List(err) } + build_session_errors.fulfill(errors) session.send_stop() 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 } val functions = List( Markup.BUILD_SESSION_FINISHED -> build_session_finished, Markup.LOADING_THEORY -> loading_theory) } /* job: running prover process */ private class Job(progress: Progress, name: String, val info: Sessions.Info, deps: Sessions.Deps, store: Sessions.Store, do_store: Boolean, verbose: Boolean, pide: Boolean, val numa_node: Option[Int], command_timings: List[Properties.T]) { private val options = NUMA.policy_options(info.options, numa_node) private val sessions_structure = deps.sessions_structure private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf") isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph_display) private val export_tmp_dir = Isabelle_System.tmp_dir("export") private val export_consumer = Export.consumer(store.open_database(name, output = true), cache = store.xz_cache) private val future_result: Future[Process_Result] = Future.thread("build") { val parent = info.parent.getOrElse("") val base = deps(name) val args_yxml = YXML.string_of_body( { import XML.Encode._ pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string, pair(string, pair(string, pair(Path.encode, pair(list(pair(Options.encode, list(pair(string, properties)))), pair(list(pair(string, properties)), pair(list(pair(string, string)), pair(list(string), pair(list(pair(string, string)), pair(list(string), list(string)))))))))))))))))( (Symbol.codes, (command_timings, (verbose, (store.browser_info, (info.document_files, (File.standard_path(graph_file), (parent, (info.chapter, (name, (Path.current, (info.theories, (sessions_structure.session_positions, (sessions_structure.dest_session_directories, (base.doc_names, (base.global_theories.toList, (base.loaded_theories.keys, info.bibtex_entries.map(_.info)))))))))))))))))) }) val env = Isabelle_System.settings() + ("ISABELLE_EXPORT_TMP" -> File.standard_path(export_tmp_dir)) + ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString) val is_pure = Sessions.is_pure(name) val eval_store = if (!do_store) Nil else { (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(name)))) } if (pide && !is_pure) { val resources = new Resources(sessions_structure, deps(parent)) val session = new Session(options, resources) val handler = new Handler(progress, session, name) session.init_protocol_handler(handler) val process = Isabelle_Process(session, options, sessions_structure, store, logic = parent, cwd = info.dir.file, env = env).await_startup session.protocol_command("build_session", args_yxml) val result = process.join - handler.result_error.join match { - case "" => result - case msg => - result.copy( - rc = result.rc max 1, - out_lines = result.out_lines ::: split_lines(Output.error_message_text(msg))) + handler.build_session_errors.join match { + case Nil => result + case errors => + result.error_rc.output( + errors.flatMap(s => split_lines(Output.error_message_text(s))) ::: + errors.map(Protocol.Error_Message_Marker.apply)) } } 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 = Command_Line.ML_tool0(eval_build :: eval_store) val process = if (is_pure) { ML_Process(options, deps.sessions_structure, store, raw_ml_system = true, args = (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten ::: List("--eval", eval), cwd = info.dir.file, env = env, cleanup = () => args_file.delete) } else { ML_Process(options, deps.sessions_structure, store, logic = parent, args = List("--eval", eval), cwd = info.dir.file, env = env, cleanup = () => args_file.delete) } process.result( progress_stdout = { case Protocol.Loading_Theory_Marker(theory) => progress.theory(Progress.Theory(theory, 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(name, args, body) case _ => }, progress_limit = options.int("process_output_limit") match { case 0 => None case m => Some(m * 1000000L) }, strict = false) } } def terminate: Unit = future_result.cancel def is_finished: Boolean = future_result.is_finished private val timeout_request: Option[Event_Timer.Request] = { if (info.timeout > Time.zero) Some(Event_Timer.request(Time.now() + info.timeout) { terminate }) else None } def join: (Process_Result, Option[String]) = { val result0 = future_result.join val result1 = export_consumer.shutdown(close = true).map(Output.error_message_text) match { case Nil => result0 case errs => result0.errors(errs).error_rc } Isabelle_System.rm_tree(export_tmp_dir) if (result1.ok) Present.finish(progress, store.browser_info, graph_file, info, name) graph_file.delete val was_timeout = timeout_request match { case None => false case Some(request) => !request.cancel } val result2 = if (result1.interrupted) { if (was_timeout) result1.error(Output.error_message_text("Timeout")).was_timeout else result1.error(Output.error_message_text("Interrupt")) } else result1 val heap_digest = if (result2.ok && do_store && store.output_heap(name).is_file) Some(Sessions.write_heap_digest(store.output_heap(name))) else None (result2, heap_digest) } } /** build with results **/ class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)]) { def sessions: Set[String] = results.keySet def cancelled(name: String): Boolean = results(name)._1.isEmpty def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1)) def info(name: String): Sessions.Info = results(name)._2 val rc: Int = (0 /: results.iterator.map( { case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }))(_ max _) def ok: Boolean = rc == 0 override def toString: String = rc.toString } def build( options: Options, progress: Progress = No_Progress, check_unknown_files: Boolean = false, build_heap: Boolean = false, clean_build: Boolean = false, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil, infos: List[Sessions.Info] = Nil, numa_shuffling: Boolean = false, max_jobs: Int = 1, list_files: Boolean = false, check_keywords: Set[String] = Set.empty, fresh_build: Boolean = false, no_build: Boolean = false, soft_build: Boolean = false, verbose: Boolean = false, export_files: Boolean = false, pide: Boolean = false, requirements: Boolean = false, all_sessions: Boolean = false, base_sessions: List[String] = Nil, exclude_session_groups: List[String] = Nil, exclude_sessions: List[String] = Nil, session_groups: List[String] = Nil, sessions: List[String] = Nil, selection: Sessions.Selection = Sessions.Selection.empty): Results = { val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true) val store = Sessions.store(build_options) Isabelle_Fonts.init() /* session selection and dependencies */ val full_sessions = Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos) def sources_stamp(deps: Sessions.Deps, name: String): String = { val digests = full_sessions(name).meta_digest :: deps.sources(name) ::: deps.imported_sources(name) SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString } val selection1 = Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups, exclude_sessions, session_groups, sessions) ++ selection val deps = { val deps0 = Sessions.deps(full_sessions.selection(selection1), progress = progress, inlined_files = true, verbose = verbose, list_files = list_files, check_keywords = check_keywords).check_errors if (soft_build && !fresh_build) { val outdated = deps0.sessions_structure.build_topological_order.flatMap(name => store.access_database(name) match { case Some(db) => using(db)(store.read_build(_, name)) match { case Some(build) if build.ok && build.sources == sources_stamp(deps0, name) => None case _ => Some(name) } case None => Some(name) }) Sessions.deps(full_sessions.selection(Sessions.Selection(sessions = outdated)), progress = progress, inlined_files = true).check_errors } else deps0 } /* check unknown files */ if (check_unknown_files) { val source_files = (for { (_, base) <- deps.session_bases.iterator (path, _) <- base.sources.iterator } yield path).toList val exclude_files = List(Path.explode("$POLYML_EXE")).map(_.canonical_file) val unknown_files = Mercurial.check_files(source_files)._2. filterNot(path => exclude_files.contains(path.canonical_file)) if (unknown_files.nonEmpty) { progress.echo_warning("Unknown files (not part of the underlying Mercurial repository):" + unknown_files.map(path => path.expand.implode).sorted.mkString("\n ", "\n ", "")) } } /* main build process */ val queue = Queue(progress, deps.sessions_structure, store) store.prepare_output_dir() if (clean_build) { for (name <- full_sessions.imports_descendants(full_sessions.imports_selection(selection1))) { val (relevant, ok) = store.clean_output(name) if (relevant) { if (ok) progress.echo("Cleaned " + name) else progress.echo(name + " FAILED to clean") } } } // scheduler loop case class Result( current: Boolean, heap_digest: Option[String], process: Option[Process_Result], info: Sessions.Info) { def ok: Boolean = process match { case None => false case Some(res) => res.rc == 0 } } def sleep() { try { Thread.sleep(500) } catch { case Exn.Interrupt() => Exn.Interrupt.impose() } } val numa_nodes = new NUMA.Nodes(numa_shuffling) @tailrec def loop( pending: Queue, running: Map[String, (List[String], Job)], results: Map[String, Result]): Map[String, Result] = { def used_node(i: Int): Boolean = running.iterator.exists( { case (_, (_, job)) => job.numa_node.isDefined && job.numa_node.get == i }) if (pending.is_empty) results else { if (progress.stopped) for ((_, (_, job)) <- running) job.terminate running.find({ case (_, (_, job)) => job.is_finished }) match { case Some((name, (input_heaps, job))) => //{{{ finish job val (process_result, heap_digest) = job.join val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test) val process_result_tail = { val tail = job.info.options.int("process_output_tail") process_result.copy( out_lines = "(see also " + store.output_log(name).file.toString + ")" :: (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0))) } // write log file if (process_result.ok) { File.write_gzip(store.output_log_gz(name), terminate_lines(log_lines)) } else File.write(store.output_log(name), terminate_lines(log_lines)) // write database { val build_log = Build_Log.Log_File(name, process_result.out_lines). parse_session_info( command_timings = true, theory_timings = true, ml_statistics = true, task_statistics = true) using(store.open_database(name, output = true))(db => store.write_session_info(db, name, build_log = if (process_result.timeout) build_log.error("Timeout") else build_log, build = Session_Info(sources_stamp(deps, name), input_heaps, heap_digest, process_result.rc))) } // messages process_result.err_lines.foreach(progress.echo) if (process_result.ok) progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")") else { progress.echo(name + " FAILED") if (!process_result.interrupted) progress.echo(process_result_tail.out) } loop(pending - name, running - name, results + (name -> Result(false, heap_digest, Some(process_result_tail), job.info))) //}}} case None if running.size < (max_jobs max 1) => //{{{ check/start next job pending.dequeue(running.isDefinedAt) match { case Some((name, info)) => val ancestor_results = deps.sessions_structure.build_requirements(List(name)).filterNot(_ == name). map(results(_)) val ancestor_heaps = ancestor_results.flatMap(_.heap_digest) val do_store = build_heap || Sessions.is_pure(name) || queue.is_inner(name) val (current, heap_digest) = { store.access_database(name) match { case Some(db) => using(db)(store.read_build(_, name)) match { case Some(build) => val heap_digest = store.find_heap_digest(name) val current = !fresh_build && build.ok && build.sources == sources_stamp(deps, name) && build.input_heaps == ancestor_heaps && build.output_heap == heap_digest && !(do_store && heap_digest.isEmpty) (current, heap_digest) case None => (false, None) } case None => (false, None) } } val all_current = current && ancestor_results.forall(_.current) if (all_current) loop(pending - name, running, results + (name -> Result(true, heap_digest, Some(Process_Result(0)), info))) else if (no_build) { if (verbose) progress.echo("Skipping " + name + " ...") loop(pending - name, running, results + (name -> Result(false, heap_digest, Some(Process_Result(1)), info))) } else if (ancestor_results.forall(_.ok) && !progress.stopped) { progress.echo((if (do_store) "Building " else "Running ") + name + " ...") store.clean_output(name) using(store.open_database(name, output = true))(store.init_session_info(_, name)) val numa_node = numa_nodes.next(used_node) val job = new Job(progress, name, info, deps, store, do_store, verbose, pide = pide, numa_node, queue.command_timings(name)) loop(pending, running + (name -> (ancestor_heaps, job)), results) } else { progress.echo(name + " CANCELLED") loop(pending - name, running, results + (name -> Result(false, heap_digest, None, info))) } case None => sleep(); loop(pending, running, results) } ///}}} case None => sleep(); loop(pending, running, results) } } } /* build results */ val results0 = if (deps.is_empty) { progress.echo_warning("Nothing to build") Map.empty[String, Result] } else loop(queue, Map.empty, Map.empty) val results = new Results( (for ((name, result) <- results0.iterator) yield (name, (result.process, result.info))).toMap) if (export_files) { for (name <- full_sessions.imports_selection(selection1).iterator if results(name).ok) { val info = results.info(name) if (info.export_files.nonEmpty) { progress.echo("Exporting " + info.name + " ...") for ((dir, prune, pats) <- info.export_files) { Export.export_files(store, name, info.dir + dir, progress = if (verbose) progress else No_Progress, export_prune = prune, export_patterns = pats) } } } } if (results.rc != 0 && (verbose || !no_build)) { val unfinished = (for { name <- results.sessions.iterator if !results(name).ok } yield name).toList.sorted progress.echo("Unfinished session(s): " + commas(unfinished)) } /* global browser info */ if (!no_build) { val browser_chapters = (for { (name, result) <- results0.iterator if result.ok info = full_sessions(name) if info.options.bool("browser_info") } yield (info.chapter, (name, info.description))).toList.groupBy(_._1). map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty) for ((chapter, entries) <- browser_chapters) Present.update_chapter_index(store.browser_info, chapter, entries) if (browser_chapters.nonEmpty) Present.make_global_index(store.browser_info) } results } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions", args => { val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")) var base_sessions: List[String] = Nil var select_dirs: List[Path] = Nil var numa_shuffling = false var pide = false var requirements = false var soft_build = false var exclude_session_groups: List[String] = Nil var all_sessions = false var build_heap = false var clean_build = false var dirs: List[Path] = Nil var export_files = false var fresh_build = false var session_groups: List[String] = Nil var max_jobs = 1 var check_keywords: Set[String] = Set.empty var list_files = false var no_build = false var options = Options.init(opts = build_options) var verbose = false var exclude_sessions: List[String] = Nil val getopts = Getopts(""" Usage: isabelle build [OPTIONS] [SESSIONS ...] Options are: -B NAME include session NAME and all descendants -D DIR include session directory and select its sessions -N cyclic shuffling of NUMA CPU nodes (performance tuning) -P build via PIDE protocol -R operate on requirements of selected sessions -S soft build: only observe changes of sources, not heap images -X NAME exclude sessions from group NAME and all descendants -a select all sessions -b build heap images -c clean build -d DIR include session directory -e export files from session specification into file-system -f fresh build -g NAME select session group NAME -j INT maximum number of parallel jobs (default 1) -k KEYWORD check theory sources for conflicts with proposed keywords -l list session source files -n no build -- test dependencies only -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v verbose -x NAME exclude session NAME and all descendants Build and manage Isabelle sessions, depending on implicit settings: """ + Library.prefix_lines(" ", Build_Log.Settings.show()) + "\n", "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), "N" -> (_ => numa_shuffling = true), "P" -> (_ => pide = true), "R" -> (_ => requirements = true), "S" -> (_ => soft_build = true), "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), "a" -> (_ => all_sessions = true), "b" -> (_ => build_heap = true), "c" -> (_ => clean_build = true), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "e" -> (_ => export_files = true), "f" -> (_ => fresh_build = true), "g:" -> (arg => session_groups = session_groups ::: List(arg)), "j:" -> (arg => max_jobs = Value.Int.parse(arg)), "k:" -> (arg => check_keywords = check_keywords + arg), "l" -> (_ => list_files = true), "n" -> (_ => no_build = true), "o:" -> (arg => options = options + arg), "v" -> (_ => verbose = true), "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) val sessions = getopts(args) val progress = new Console_Progress(verbose = verbose) val start_date = Date.now() if (verbose) { progress.echo( "Started at " + Build_Log.print_date(start_date) + " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")") progress.echo(Build_Log.Settings.show() + "\n") } val results = progress.interrupt_handler { build(options, progress = progress, check_unknown_files = Mercurial.is_repository(Path.explode("~~")), build_heap = build_heap, clean_build = clean_build, dirs = dirs, select_dirs = select_dirs, numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling), max_jobs = max_jobs, list_files = list_files, check_keywords = check_keywords, fresh_build = fresh_build, no_build = no_build, soft_build = soft_build, verbose = verbose, export_files = export_files, pide = pide, 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) } val end_date = Date.now() val elapsed_time = end_date.time - start_date.time if (verbose) { progress.echo("\nFinished at " + Build_Log.print_date(end_date)) } val total_timing = (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _). copy(elapsed = elapsed_time) progress.echo(total_timing.message_resources) sys.exit(results.rc) }) /* build logic image */ def build_logic(options: Options, logic: String, progress: Progress = No_Progress, build_heap: Boolean = false, dirs: List[Path] = Nil, fresh: Boolean = false, strict: Boolean = false): Int = { val rc = if (!fresh && build(options, build_heap = build_heap, no_build = true, dirs = dirs, sessions = List(logic)).ok) 0 else { progress.echo("Build started for Isabelle/" + logic + " ...") Build.build(options, progress = progress, build_heap = build_heap, fresh_build = fresh, dirs = dirs, sessions = List(logic)).rc } if (strict && rc != 0) error("Failed to build Isabelle/" + logic) else rc } }