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