bin/time_build.php

   1 <?php
   2
   3 $lines = file_get_contents($argv[1]);
   4 $lines = preg_split('/\n/', $lines);
   5
   6 $times = array();
   7 foreach ($lines as $line) {
   8   if (preg_match('/^([0-9\.]+) .* ([^ ]+\.cpp|c)$/', $line, $matches)) {
   9     $time = $matches[1];
  10     $file = $matches[2];
  11     $times[$file] = $time;
  12   } else if (preg_match('/^([0-9\.]+) (g\+\+ -o|ar -crs)/', $line, $matches)) {
  13     $linktime = $matches[1];
  14   } else {
  15     print "Unknown output: $line";
  16   }
  17 }
  18
  19 asort($times);
  20 foreach ($times as $file => $time) {
  21   print format_time($time)." compiling $file\n";
  22 }
  23 print format_time($linktime)." linking\n";
  24
  25 function format_time($time) {
  26   return (int)($time / 60) . "'" .
  27     (($time % 60) > 9 ? '':'0'). ($time % 60) . '"';
  28 }