superceded by isatest-statistics;
authorwenzelm
Tue Sep 19 22:00:53 2006 +0200 (2006-09-19)
changeset 20616b36a4e843d0e
parent 20615 0d71cc267e0d
child 20617 ca59894f70dc
superceded by isatest-statistics;
Admin/isatest_statistics.ML
     1.1 --- a/Admin/isatest_statistics.ML	Tue Sep 19 22:00:32 2006 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,120 +0,0 @@
     1.4 -(*  Title:      Admin/isatest_statistics.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Stefan Berghofer, TU Muenchen
     1.7 -
     1.8 -Script for producing Gnuplot data files describing runtimes of Isabelle
     1.9 -sessions from the logfiles generated by isatest.
    1.10 -*)
    1.11 -
    1.12 -structure Statistics =
    1.13 -struct
    1.14 -
    1.15 -fun read_dir s =
    1.16 -  let
    1.17 -    val d = OS.FileSys.openDir s;
    1.18 -    fun read_all () = (case OS.FileSys.readDir d of
    1.19 -        NONE => []
    1.20 -      | SOME s => s :: read_all ());
    1.21 -    val xs = read_all ();
    1.22 -    val _ = OS.FileSys.closeDir d
    1.23 -  in xs end;
    1.24 -
    1.25 -fun is_suffix eq xs ys = is_prefix eq (rev xs) (rev ys);
    1.26 -
    1.27 -fun int_of_string s = the (Int.fromString s);
    1.28 -
    1.29 -fun get_files dir year compiler =
    1.30 -  let
    1.31 -    val fs = read_dir dir;
    1.32 -    val subdirs = filter (is_prefix op = (explode year) o explode) fs
    1.33 -    val fs' = List.concat (map (fn d =>
    1.34 -      map (pair (dir ^ "/" ^ d)) (read_dir (dir ^ "/" ^ d))) subdirs);
    1.35 -    val prfx = explode ("isatest-makeall-" ^ compiler ^ "-");
    1.36 -    val sfx = explode ".gz";
    1.37 -    val k = length prfx;
    1.38 -    val fs'' = List.mapPartial (fn (d, f) =>
    1.39 -      let val xs = explode f
    1.40 -      in
    1.41 -        if is_prefix op = prfx xs andalso is_suffix op = sfx xs then
    1.42 -          let
    1.43 -            val (_, xs1) = chop k xs;
    1.44 -            val (year', xs2) = chop 4 xs1;
    1.45 -            val (_ :: month, xs3) = chop 3 xs2;
    1.46 -            val (_ :: day, _) = chop 3 xs3
    1.47 -          in
    1.48 -            if year = implode year' then SOME (d, f,
    1.49 -              (int_of_string (implode year'),
    1.50 -               (int_of_string (implode month),
    1.51 -                int_of_string (implode day))))
    1.52 -            else NONE
    1.53 -          end
    1.54 -        else NONE
    1.55 -      end) (map (pair dir) fs @ fs')
    1.56 -  in sort (prod_ord int_ord (prod_ord int_ord int_ord) o pairself #3) fs'' end;
    1.57 -
    1.58 -fun get_times f =
    1.59 -  let
    1.60 -    val s = execute ("zcat " ^ f ^ " | grep Finished | grep \"elapsed time\"");
    1.61 -    val xs = filter_out (equal "") (space_explode "\n" s);
    1.62 -    fun get_time s =
    1.63 -      let
    1.64 -        val xs = explode s;
    1.65 -        val (_, _ :: xs1) = take_prefix (not o equal " ") xs;
    1.66 -        val (logic, _ :: _ :: h :: _ :: m1 :: m2 :: _ :: s1 :: s2 :: xs2) =
    1.67 -          take_prefix (not o equal " ") xs1;
    1.68 -        val cpu = case take_prefix (not o equal ",") xs2 of
    1.69 -            (_, _ :: _ :: h' :: _ :: m1' :: m2' :: _ :: s1' :: s2' :: _) =>
    1.70 -              SOME (int_of_string h',
    1.71 -                int_of_string (m1' ^ m2'), int_of_string (s1' ^ s2'))
    1.72 -          | _ => NONE
    1.73 -      in (implode logic,
    1.74 -        ((int_of_string h, int_of_string (m1 ^ m2), int_of_string (s1 ^ s2)),
    1.75 -         cpu))
    1.76 -      end
    1.77 -  in
    1.78 -    map get_time xs
    1.79 -  end;
    1.80 -
    1.81 -fun mk_table tab logic =
    1.82 -  let
    1.83 -    fun mk_entry (times, (y, (M, D))) = (case AList.lookup op = times logic of
    1.84 -        SOME (t, t') =>
    1.85 -          let
    1.86 -            val (h, m, s) = the_default t t';
    1.87 -            val date = (100 * ((M - 1) * 31 + D - 1)) div 31;
    1.88 -            val time = (100 * (h * 3600 + 60 * m + s)) div 60
    1.89 -          in
    1.90 -            SOME (Int.toString (date div 100) ^ "." ^ Int.toString (date mod 100) ^ " " ^
    1.91 -              Int.toString (time div 100) ^ "." ^ Int.toString (time mod 100))
    1.92 -          end
    1.93 -      | NONE => (warning ("No session " ^ quote logic ^ " in logfile for " ^
    1.94 -          Int.toString y ^ "-" ^ Int.toString M ^ "-" ^ Int.toString D); NONE));
    1.95 -  in
    1.96 -    space_implode "\n" (List.mapPartial mk_entry tab) ^ "\n"
    1.97 -  end;
    1.98 -
    1.99 -fun mk_tables dir targetdir year compiler =
   1.100 -  let
   1.101 -    val files = get_files dir year compiler;
   1.102 -    val tab = map (fn (d, f, date) => (get_times (d ^ "/" ^ f), date)) files;
   1.103 -    val logics = map fst (fst (hd tab))
   1.104 -  in
   1.105 -    Library.seq (fn logic =>
   1.106 -      File.write (Path.append (Path.unpack targetdir) (Path.unpack (logic ^ ".dat")))
   1.107 -        (mk_table tab logic)) logics
   1.108 -  end;
   1.109 -
   1.110 -end
   1.111 -
   1.112 -
   1.113 -(**** Example *****
   1.114 -
   1.115 -In ML:
   1.116 -
   1.117 -Statistics.mk_tables "/home/isatest/log" "/tmp" "2006" "at-poly";
   1.118 -
   1.119 -In Gnuplot:
   1.120 -
   1.121 -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"
   1.122 -
   1.123 -*******************)
   1.124 \ No newline at end of file