1.1 --- a/src/Pure/Tools/build.ML Tue Feb 19 14:47:57 2013 +0100
1.2 +++ b/src/Pure/Tools/build.ML Tue Feb 19 16:49:40 2013 +0100
1.3 @@ -93,7 +93,7 @@
1.4
1.5 fun build args_file = Command_Line.tool (fn () =>
1.6 let
1.7 - val (timings, (do_output, (options, (verbose, (browser_info,
1.8 + val (command_timings, (do_output, (options, (verbose, (browser_info,
1.9 (parent_name, (name, theories))))))) =
1.10 File.read (Path.explode args_file) |> YXML.parse_body |>
1.11 let open XML.Decode in
1.12 @@ -126,7 +126,7 @@
1.13
1.14 val last_timing =
1.15 the_default Timing.zero o
1.16 - Timings.lookup (make_timings timings) o Toplevel.approximative_id;
1.17 + Timings.lookup (make_timings command_timings) o Toplevel.approximative_id;
1.18
1.19 val res1 =
1.20 theories |>
2.1 --- a/src/Pure/Tools/build.scala Tue Feb 19 14:47:57 2013 +0100
2.2 +++ b/src/Pure/Tools/build.scala Tue Feb 19 16:49:40 2013 +0100
2.3 @@ -288,9 +288,16 @@
2.4
2.5 object Queue
2.6 {
2.7 - def apply(tree: Session_Tree): Queue =
2.8 + def apply(tree: Session_Tree, get_timings: String => (List[Properties.T], Double)): Queue =
2.9 {
2.10 val graph = tree.graph
2.11 + val sessions = graph.keys.toList
2.12 +
2.13 + val timings = sessions.map(name => (name, get_timings(name)))
2.14 + val command_timings =
2.15 + Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
2.16 + val session_timing =
2.17 + Map(timings.map({ case (name, (_, t)) => (name, t) }): _*).withDefaultValue(0.0)
2.18
2.19 def outdegree(name: String): Int = graph.imm_succs(name).size
2.20 def timeout(name: String): Double = tree(name).options.real("timeout")
2.21 @@ -300,25 +307,32 @@
2.22 def compare(name1: String, name2: String): Int =
2.23 outdegree(name2) compare outdegree(name1) match {
2.24 case 0 =>
2.25 - timeout(name2) compare timeout(name1) match {
2.26 - case 0 => name1 compare name2
2.27 + session_timing(name2) compare session_timing(name1) match {
2.28 + case 0 =>
2.29 + timeout(name2) compare timeout(name1) match {
2.30 + case 0 => name1 compare name2
2.31 + case ord => ord
2.32 + }
2.33 case ord => ord
2.34 }
2.35 case ord => ord
2.36 }
2.37 }
2.38
2.39 - new Queue(graph, SortedSet(graph.keys.toList: _*)(Ordering))
2.40 + new Queue(graph, SortedSet(sessions: _*)(Ordering), command_timings)
2.41 }
2.42 }
2.43
2.44 - final class Queue private(graph: Graph[String, Session_Info], order: SortedSet[String])
2.45 + final class Queue private(
2.46 + graph: Graph[String, Session_Info],
2.47 + order: SortedSet[String],
2.48 + val command_timings: String => List[Properties.T])
2.49 {
2.50 def is_inner(name: String): Boolean = !graph.is_maximal(name)
2.51
2.52 def is_empty: Boolean = graph.is_empty
2.53
2.54 - def - (name: String): Queue = new Queue(graph.del_node(name), order - name)
2.55 + def - (name: String): Queue = new Queue(graph.del_node(name), order - name, command_timings)
2.56
2.57 def dequeue(skip: String => Boolean): Option[(String, Session_Info)] =
2.58 {
2.59 @@ -419,7 +433,7 @@
2.60
2.61 private class Job(progress: Build.Progress,
2.62 name: String, val info: Session_Info, output: Path, do_output: Boolean,
2.63 - verbose: Boolean, browser_info: Path)
2.64 + verbose: Boolean, browser_info: Path, command_timings: List[Properties.T])
2.65 {
2.66 // global browser info dir
2.67 if (info.options.bool("browser_info") && !(browser_info + Path.explode("index.html")).is_file)
2.68 @@ -445,7 +459,7 @@
2.69 import XML.Encode._
2.70 pair(list(properties), pair(bool, pair(Options.encode, pair(bool, pair(Path.encode,
2.71 pair(string, pair(string, list(pair(Options.encode, list(Path.encode))))))))))(
2.72 - (Nil /* FIXME */, (do_output, (info.options, (verbose, (browser_info,
2.73 + (command_timings, (do_output, (info.options, (verbose, (browser_info,
2.74 (parent, (name, info.theories))))))))
2.75 }))
2.76
2.77 @@ -546,17 +560,22 @@
2.78
2.79
2.80 sealed case class Log_Info(
2.81 - name: String, stats: List[Properties.T], tasks: List[Properties.T], timing: Properties.T)
2.82 + name: String,
2.83 + stats: List[Properties.T],
2.84 + tasks: List[Properties.T],
2.85 + command_timings: List[Properties.T],
2.86 + session_timing: Properties.T)
2.87
2.88 - def parse_log(text: String): Log_Info =
2.89 + def parse_log(full_stats: Boolean, text: String): Log_Info =
2.90 {
2.91 val lines = split_lines(text)
2.92 val name =
2.93 lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) getOrElse ""
2.94 - val stats = Props.parse_lines("\fML_statistics = ", lines)
2.95 - val tasks = Props.parse_lines("\ftask_statistics = ", lines)
2.96 - val timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
2.97 - Log_Info(name, stats, tasks, timing)
2.98 + val stats = if (full_stats) Props.parse_lines("\fML_statistics = ", lines) else Nil
2.99 + val tasks = if (full_stats) Props.parse_lines("\ftask_statistics = ", lines) else Nil
2.100 + val command_timings = Props.parse_lines("\fcommand_timing = ", lines)
2.101 + val session_timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
2.102 + Log_Info(name, stats, tasks, command_timings, session_timing)
2.103 }
2.104
2.105
2.106 @@ -612,16 +631,20 @@
2.107 verbose: Boolean = false,
2.108 sessions: List[String] = Nil): Int =
2.109 {
2.110 + /* session tree and dependencies */
2.111 +
2.112 val full_tree = find_sessions(options, more_dirs)
2.113 val (selected, selected_tree) =
2.114 full_tree.selection(requirements, all_sessions, session_groups, sessions)
2.115
2.116 val deps = dependencies(progress, true, verbose, list_files, selected_tree)
2.117 - val queue = Queue(selected_tree)
2.118
2.119 def make_stamp(name: String): String =
2.120 sources_stamp(selected_tree(name).entry_digest :: deps.sources(name))
2.121
2.122 +
2.123 + /* persistent information */
2.124 +
2.125 val (input_dirs, output_dir, browser_info) =
2.126 if (system_mode) {
2.127 val output_dir = Path.explode("~~/heaps/$ML_IDENTIFIER")
2.128 @@ -633,6 +656,33 @@
2.129 Path.explode("$ISABELLE_BROWSER_INFO"))
2.130 }
2.131
2.132 + def find_log(name: String): Option[Path] =
2.133 + input_dirs.find(dir => (dir + log_gz(name)).is_file).map(dir => dir + log_gz(name))
2.134 +
2.135 +
2.136 + /* queue with scheduling information */
2.137 +
2.138 + def get_timing(name: String): (List[Properties.T], Double) =
2.139 + find_log(name) match {
2.140 + case Some(path) =>
2.141 + try {
2.142 + val info = parse_log(false, File.read_gzip(path))
2.143 + val session_timing = Markup.Elapsed.unapply(info.session_timing) getOrElse 0.0
2.144 + (info.command_timings, session_timing)
2.145 + }
2.146 + catch {
2.147 + case ERROR(msg) =>
2.148 + java.lang.System.err.println("### Ignoring bad log file: " + path + "\n" + msg)
2.149 + (Nil, 0.0)
2.150 + }
2.151 + case None => (Nil, 0.0)
2.152 + }
2.153 +
2.154 + val queue = Queue(selected_tree, get_timing)
2.155 +
2.156 +
2.157 + /* main build process */
2.158 +
2.159 // prepare log dir
2.160 Isabelle_System.mkdirs(output_dir + LOG)
2.161
2.162 @@ -718,11 +768,11 @@
2.163
2.164 val (current, heap) =
2.165 {
2.166 - input_dirs.find(dir => (dir + log_gz(name)).is_file) match {
2.167 - case Some(dir) =>
2.168 - read_stamps(dir + log_gz(name)) match {
2.169 + find_log(name) match {
2.170 + case Some(path) =>
2.171 + read_stamps(path) match {
2.172 case Some((s, h1, h2)) =>
2.173 - val heap = heap_stamp(Some(dir + Path.basic(name)))
2.174 + val heap = heap_stamp(Some(path.dir + Path.basic(name)))
2.175 (s == make_stamp(name) && h1 == parent_result.heap && h2 == heap &&
2.176 !(do_output && heap == no_heap), heap)
2.177 case None => (false, no_heap)
2.178 @@ -740,7 +790,9 @@
2.179 }
2.180 else if (parent_result.rc == 0) {
2.181 progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
2.182 - val job = new Job(progress, name, info, output, do_output, verbose, browser_info)
2.183 + val job =
2.184 + new Job(progress, name, info, output, do_output, verbose, browser_info,
2.185 + queue.command_timings(name))
2.186 loop(pending, running + (name -> (parent_result.heap, job)), results)
2.187 }
2.188 else {
2.189 @@ -754,6 +806,9 @@
2.190 }
2.191 }
2.192
2.193 +
2.194 + /* build results */
2.195 +
2.196 val results =
2.197 if (deps.is_empty) {
2.198 progress.echo("### Nothing to build")