Admin/isatest_statistics.ML
author berghofe
Tue Aug 08 12:28:00 2006 +0200 (2006-08-08)
changeset 20359 517236b1bb1d
parent 20347 1ffbe17cef38
permissions -rw-r--r--
Adapted to older logfiles containing no cpu time.
     1 (*  Title:      Admin/isatest_statistics.ML
     2     ID:         $Id$
     3     Author:     Stefan Berghofer, TU Muenchen
     4 
     5 Script for producing Gnuplot data files describing runtimes of Isabelle
     6 sessions from the logfiles generated by isatest.
     7 *)
     8 
     9 structure Statistics =
    10 struct
    11 
    12 fun read_dir s =
    13   let
    14     val d = OS.FileSys.openDir s;
    15     fun read_all () = (case OS.FileSys.readDir d of
    16         NONE => []
    17       | SOME s => s :: read_all ());
    18     val xs = read_all ();
    19     val _ = OS.FileSys.closeDir d
    20   in xs end;
    21 
    22 fun is_suffix eq xs ys = is_prefix eq (rev xs) (rev ys);
    23 
    24 fun int_of_string s = the (Int.fromString s);
    25 
    26 fun get_files dir year compiler =
    27   let
    28     val fs = read_dir dir;
    29     val subdirs = filter (is_prefix op = (explode year) o explode) fs
    30     val fs' = List.concat (map (fn d =>
    31       map (pair (dir ^ "/" ^ d)) (read_dir (dir ^ "/" ^ d))) subdirs);
    32     val prfx = explode ("isatest-makeall-" ^ compiler ^ "-");
    33     val sfx = explode ".gz";
    34     val k = length prfx;
    35     val fs'' = List.mapPartial (fn (d, f) =>
    36       let val xs = explode f
    37       in
    38         if is_prefix op = prfx xs andalso is_suffix op = sfx xs then
    39           let
    40             val (_, xs1) = chop k xs;
    41             val (year', xs2) = chop 4 xs1;
    42             val (_ :: month, xs3) = chop 3 xs2;
    43             val (_ :: day, _) = chop 3 xs3
    44           in
    45             if year = implode year' then SOME (d, f,
    46               (int_of_string (implode year'),
    47                (int_of_string (implode month),
    48                 int_of_string (implode day))))
    49             else NONE
    50           end
    51         else NONE
    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;
    54 
    55 fun get_times f =
    56   let
    57     val s = execute ("zcat " ^ f ^ " | grep Finished | grep \"elapsed time\"");
    58     val xs = filter_out (equal "") (space_explode "\n" s);
    59     fun get_time s =
    60       let
    61         val xs = explode s;
    62         val (_, _ :: xs1) = take_prefix (not o equal " ") xs;
    63         val (logic, _ :: _ :: h :: _ :: m1 :: m2 :: _ :: s1 :: s2 :: xs2) =
    64           take_prefix (not o equal " ") xs1;
    65         val cpu = case take_prefix (not o equal ",") xs2 of
    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
    70       in (implode logic,
    71         ((int_of_string h, int_of_string (m1 ^ m2), int_of_string (s1 ^ s2)),
    72          cpu))
    73       end
    74   in
    75     map get_time xs
    76   end;
    77 
    78 fun mk_table tab logic =
    79   let
    80     fun mk_entry (times, (y, (M, D))) = (case AList.lookup op = times logic of
    81         SOME (t, t') =>
    82           let
    83             val (h, m, s) = the_default t t';
    84             val date = (100 * ((M - 1) * 31 + D - 1)) div 31;
    85             val time = (100 * (h * 3600 + 60 * m + s)) div 60
    86           in
    87             SOME (Int.toString (date div 100) ^ "." ^ Int.toString (date mod 100) ^ " " ^
    88               Int.toString (time div 100) ^ "." ^ Int.toString (time mod 100))
    89           end
    90       | NONE => (warning ("No session " ^ quote logic ^ " in logfile for " ^
    91           Int.toString y ^ "-" ^ Int.toString M ^ "-" ^ Int.toString D); NONE));
    92   in
    93     space_implode "\n" (List.mapPartial mk_entry tab) ^ "\n"
    94   end;
    95 
    96 fun mk_tables dir targetdir year compiler =
    97   let
    98     val files = get_files dir year compiler;
    99     val tab = map (fn (d, f, date) => (get_times (d ^ "/" ^ f), date)) files;
   100     val logics = map fst (fst (hd tab))
   101   in
   102     Library.seq (fn logic =>
   103       File.write (Path.append (Path.unpack targetdir) (Path.unpack (logic ^ ".dat")))
   104         (mk_table tab logic)) logics
   105   end;
   106 
   107 end
   108 
   109 
   110 (**** Example *****
   111 
   112 In ML:
   113 
   114 Statistics.mk_tables "/home/isatest/log" "/tmp" "2006" "at-poly";
   115 
   116 In Gnuplot:
   117 
   118 plot [0:8] [0:40] '/tmp/HOL.dat' smooth sbezier title "HOL", '/tmp/HOL-Auth.dat' smooth sbezier title "HOL-Auth", '/tmp/HOL-Complex.dat' smooth sbezier title "HOL-Complex", '/tmp/HOL-UNITY.dat' smooth sbezier title "HOL-UNITY", '/tmp/HOL-Bali.dat' smooth sbezier title "HOL-Bali", '/tmp/HOL-MicroJava.dat' smooth sbezier title "HOL-MicroJava"
   119 
   120 *******************)