# HG changeset patch # User wenzelm # Date 1489851820 -3600 # Node ID 8f58102afa220f21ce7b1af6064aaef86b34a52c # Parent c1ba192b4f962d83759717fb58d7091e6b023acf support PIDE option (inactive); misc tuning; diff -r c1ba192b4f96 -r 8f58102afa22 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sat Mar 18 16:15:37 2017 +0100 +++ b/src/Pure/Tools/build.scala Sat Mar 18 16:43:40 2017 +0100 @@ -130,33 +130,34 @@ } - /* jobs */ + /* job: running prover process */ - private class Job(progress: Progress, name: String, val info: Sessions.Info, tree: Sessions.Tree, - store: Sessions.Store, do_output: Boolean, verbose: Boolean, val numa_node: Option[Int], - session_graph: Graph_Display.Graph, command_timings: List[Properties.T]) + private class Job(progress: Progress, + name: String, + val info: Sessions.Info, + tree: Sessions.Tree, + store: Sessions.Store, + do_output: Boolean, + verbose: Boolean, + pide: Boolean, + val numa_node: Option[Int], + session_graph: Graph_Display.Graph, + command_timings: List[Properties.T]) { val output = store.output_dir + Path.basic(name) def output_path: Option[Path] = if (do_output) Some(output) else None - def output_save_state: String = - if (do_output) "ML_Heap.save_child " + ML_Syntax.print_string0(File.platform_path(output)) - else "" output.file.delete - private val parent = info.parent.getOrElse("") - private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf") try { isabelle.graphview.Graph_File.write(info.options, graph_file, session_graph) } catch { case ERROR(_) => /*error should be exposed in ML*/ } - private val env = - Isabelle_System.settings() + - ("ISABELLE_ML_DEBUGGER" -> info.options.bool("ML_debugger").toString) - private val future_result: Future[Process_Result] = Future.thread("build") { - val args_file = Isabelle_System.tmp_file("build") - File.write(args_file, YXML.string_of_body( + val parent = info.parent.getOrElse("") + + val args_yxml = + YXML.string_of_body( { val theories = info.theories.map(x => (x._2, x._3)) import XML.Encode._ @@ -168,44 +169,59 @@ (store.browser_info, (info.document_files, (File.standard_path(graph_file), (parent, (info.chapter, (name, (Path.current, theories)))))))))))) - })) + }) + + val env = + Isabelle_System.settings() + + ("ISABELLE_ML_DEBUGGER" -> info.options.bool("ML_debugger").toString) + + def save_heap: String = + "ML_Heap.share_common_data (); ML_Heap.save_child " + + ML_Syntax.print_string0(File.platform_path(output)) - val eval = - "Command_Line.tool0 (fn () => (" + - "Build.build " + ML_Syntax.print_string0(File.standard_path(args_file)) + - (if (do_output) "; ML_Heap.share_common_data (); " + output_save_state - else "") + "));" + if (pide) { + error("FIXME") + } + else { + val args_file = Isabelle_System.tmp_file("build") + File.write(args_file, args_yxml) + + val eval = + "Command_Line.tool0 (fn () => (" + + "Build.build " + ML_Syntax.print_string0(File.standard_path(args_file)) + + (if (do_output) "; " + save_heap else "") + "));" - val process_options = - numa_node match { - case None => info.options - case Some(n) => info.options.string("ML_process_policy") = NUMA.policy(n) - } - val process = - if (Sessions.pure_name(name)) { - ML_Process(process_options, raw_ml_system = true, cwd = info.dir.file, - args = - (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten ::: - List("--eval", eval), - env = env, tree = Some(tree), store = store, cleanup = () => args_file.delete) - } - else { - ML_Process(process_options, parent, List("--eval", eval), cwd = info.dir.file, - env = env, tree = Some(tree), store = store, cleanup = () => args_file.delete) - } + val process_options = + numa_node match { + case None => info.options + case Some(n) => info.options.string("ML_process_policy") = NUMA.policy(n) + } + val process = + if (Sessions.pure_name(name)) { + ML_Process(process_options, raw_ml_system = true, cwd = info.dir.file, + args = + (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten ::: + List("--eval", eval), + env = env, tree = Some(tree), store = store, cleanup = () => args_file.delete) + } + else { + ML_Process(process_options, parent, List("--eval", eval), cwd = info.dir.file, + env = env, tree = Some(tree), store = store, cleanup = () => args_file.delete) + } - process.result( - progress_stdout = (line: String) => - Library.try_unprefix("\floading_theory = ", line) match { - case Some(theory) => progress.theory(name, theory) - case None => - }, - progress_limit = - info.options.int("process_output_limit") match { - case 0 => None - case m => Some(m * 1000000L) - }, - strict = false) + process.result( + progress_stdout = (line: String) => + Library.try_unprefix("\floading_theory = ", line) match { + case Some(theory) => progress.theory(name, theory) + case None => + }, + progress_limit = + info.options.int("process_output_limit") match { + case 0 => None + case m => Some(m * 1000000L) + }, + strict = false) + } } def terminate: Unit = future_result.cancel @@ -269,6 +285,7 @@ no_build: Boolean = false, system_mode: Boolean = false, verbose: Boolean = false, + pide: Boolean = false, requirements: Boolean = false, all_sessions: Boolean = false, exclude_session_groups: List[String] = Nil, @@ -290,6 +307,7 @@ no_build = no_build, system_mode = system_mode, verbose = verbose, + pide = pide, selection = { full_tree => full_tree.selection(requirements, all_sessions, exclude_session_groups, exclude_sessions, session_groups, sessions) }) @@ -309,6 +327,7 @@ no_build: Boolean = false, system_mode: Boolean = false, verbose: Boolean = false, + pide: Boolean = false, selection: Sessions.Tree => (List[String], Sessions.Tree) = (_.selection(all_sessions = true))): Results = { @@ -477,7 +496,7 @@ progress.echo((if (do_output) "Building " else "Running ") + name + " ...") val job = new Job(progress, name, info, selected_tree, store, do_output, verbose, - numa_node, deps(name).session_graph, queue.command_timings(name)) + pide, numa_node, deps(name).session_graph, queue.command_timings(name)) loop(pending, running + (name -> (ancestor_heaps, job)), results) } else { @@ -548,6 +567,7 @@ var select_dirs: List[Path] = Nil var numa_shuffling = false + var pide = false var requirements = false var exclude_session_groups: List[String] = Nil var all_sessions = false @@ -570,6 +590,7 @@ Options are: -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 -X NAME exclude sessions from group NAME and all descendants -a select all sessions @@ -591,6 +612,7 @@ """ + Library.prefix_lines(" ", Build_Log.Settings.show()) + "\n", "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), "N" -> (_ => numa_shuffling = true), + "P" -> (_ => pide = true), "R" -> (_ => requirements = true), "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), "a" -> (_ => all_sessions = true), @@ -634,6 +656,7 @@ no_build = no_build, system_mode = system_mode, verbose = verbose, + pide = pide, requirements = requirements, all_sessions = all_sessions, exclude_session_groups = exclude_session_groups,