recover timing information from old log files;
authorwenzelm
Tue Feb 19 16:49:40 2013 +0100 (2013-02-19 ago)
changeset 51220e140c8fa485a
parent 51219 2464ba6e6fc9
child 51221 e8ac22bb2b28
recover timing information from old log files;
use session timing for queue ordering;
pass command timings to ML process (still unused);
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
     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")