Admin/isatest_statistics.ML
changeset 20359 517236b1bb1d
parent 20347 1ffbe17cef38
equal deleted inserted replaced
20358:ccad73da6f61 20359:517236b1bb1d
    52       end) (map (pair dir) fs @ fs')
    52       end) (map (pair dir) fs @ fs')
    53   in sort (prod_ord int_ord (prod_ord int_ord int_ord) o pairself #3) fs'' end;
    53   in sort (prod_ord int_ord (prod_ord int_ord int_ord) o pairself #3) fs'' end;
    54 
    54 
    55 fun get_times f =
    55 fun get_times f =
    56   let
    56   let
    57     val s = execute ("zcat " ^ f ^ " | grep Finished | grep \"cpu time\"");
    57     val s = execute ("zcat " ^ f ^ " | grep Finished | grep \"elapsed time\"");
    58     val xs = filter_out (equal "") (space_explode "\n" s);
    58     val xs = filter_out (equal "") (space_explode "\n" s);
    59     fun get_time s =
    59     fun get_time s =
    60       let
    60       let
    61         val xs = explode s;
    61         val xs = explode s;
    62         val (_, _ :: xs1) = take_prefix (not o equal " ") xs;
    62         val (_, _ :: xs1) = take_prefix (not o equal " ") xs;
    63         val (logic, _ :: _ :: h :: _ :: m1 :: m2 :: _ :: s1 :: s2 :: xs2) =
    63         val (logic, _ :: _ :: h :: _ :: m1 :: m2 :: _ :: s1 :: s2 :: xs2) =
    64           take_prefix (not o equal " ") xs1;
    64           take_prefix (not o equal " ") xs1;
    65         val (_, _ :: _ :: h' :: _ :: m1' :: m2' :: _ :: s1' :: s2' :: _) =
    65         val cpu = case take_prefix (not o equal ",") xs2 of
    66           take_prefix (not o equal ",") xs2
    66             (_, _ :: _ :: h' :: _ :: m1' :: m2' :: _ :: s1' :: s2' :: _) =>
       
    67               SOME (int_of_string h',
       
    68                 int_of_string (m1' ^ m2'), int_of_string (s1' ^ s2'))
       
    69           | _ => NONE
    67       in (implode logic,
    70       in (implode logic,
    68         ((int_of_string h, int_of_string (m1 ^ m2), int_of_string (s1 ^ s2)),
    71         ((int_of_string h, int_of_string (m1 ^ m2), int_of_string (s1 ^ s2)),
    69          (int_of_string h', int_of_string (m1' ^ m2'), int_of_string (s1' ^ s2'))))
    72          cpu))
    70       end
    73       end
    71   in
    74   in
    72     map get_time xs
    75     map get_time xs
    73   end;
    76   end;
    74 
    77 
    75 fun mk_table tab logic =
    78 fun mk_table tab logic =
    76   let
    79   let
    77     fun mk_entry (times, (y, (M, D))) = (case AList.lookup op = times logic of
    80     fun mk_entry (times, (y, (M, D))) = (case AList.lookup op = times logic of
    78         SOME (_, (h, m, s)) =>
    81         SOME (t, t') =>
    79           let
    82           let
       
    83             val (h, m, s) = the_default t t';
    80             val date = (100 * ((M - 1) * 31 + D - 1)) div 31;
    84             val date = (100 * ((M - 1) * 31 + D - 1)) div 31;
    81             val time = (100 * (h * 3600 + 60 * m + s)) div 60
    85             val time = (100 * (h * 3600 + 60 * m + s)) div 60
    82           in
    86           in
    83             SOME (Int.toString (date div 100) ^ "." ^ Int.toString (date mod 100) ^ " " ^
    87             SOME (Int.toString (date div 100) ^ "." ^ Int.toString (date mod 100) ^ " " ^
    84               Int.toString (time div 100) ^ "." ^ Int.toString (time mod 100))
    88               Int.toString (time div 100) ^ "." ^ Int.toString (time mod 100))