# HG changeset patch
# User wenzelm
# Date 1158696053 -7200
# Node ID b36a4e843d0e5dcd6d1a1b54db35b2b1ef8293ee
# Parent  0d71cc267e0dd8a8af95e177af09a4f6790581f1
superceded by isatest-statistics;

diff -r 0d71cc267e0d -r b36a4e843d0e Admin/isatest_statistics.ML
--- a/Admin/isatest_statistics.ML	Tue Sep 19 22:00:32 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,120 +0,0 @@
-(*  Title:      Admin/isatest_statistics.ML
-    ID:         $Id$
-    Author:     Stefan Berghofer, TU Muenchen
-
-Script for producing Gnuplot data files describing runtimes of Isabelle
-sessions from the logfiles generated by isatest.
-*)
-
-structure Statistics =
-struct
-
-fun read_dir s =
-  let
-    val d = OS.FileSys.openDir s;
-    fun read_all () = (case OS.FileSys.readDir d of
-        NONE => []
-      | SOME s => s :: read_all ());
-    val xs = read_all ();
-    val _ = OS.FileSys.closeDir d
-  in xs end;
-
-fun is_suffix eq xs ys = is_prefix eq (rev xs) (rev ys);
-
-fun int_of_string s = the (Int.fromString s);
-
-fun get_files dir year compiler =
-  let
-    val fs = read_dir dir;
-    val subdirs = filter (is_prefix op = (explode year) o explode) fs
-    val fs' = List.concat (map (fn d =>
-      map (pair (dir ^ "/" ^ d)) (read_dir (dir ^ "/" ^ d))) subdirs);
-    val prfx = explode ("isatest-makeall-" ^ compiler ^ "-");
-    val sfx = explode ".gz";
-    val k = length prfx;
-    val fs'' = List.mapPartial (fn (d, f) =>
-      let val xs = explode f
-      in
-        if is_prefix op = prfx xs andalso is_suffix op = sfx xs then
-          let
-            val (_, xs1) = chop k xs;
-            val (year', xs2) = chop 4 xs1;
-            val (_ :: month, xs3) = chop 3 xs2;
-            val (_ :: day, _) = chop 3 xs3
-          in
-            if year = implode year' then SOME (d, f,
-              (int_of_string (implode year'),
-               (int_of_string (implode month),
-                int_of_string (implode day))))
-            else NONE
-          end
-        else NONE
-      end) (map (pair dir) fs @ fs')
-  in sort (prod_ord int_ord (prod_ord int_ord int_ord) o pairself #3) fs'' end;
-
-fun get_times f =
-  let
-    val s = execute ("zcat " ^ f ^ " | grep Finished | grep \"elapsed time\"");
-    val xs = filter_out (equal "") (space_explode "\n" s);
-    fun get_time s =
-      let
-        val xs = explode s;
-        val (_, _ :: xs1) = take_prefix (not o equal " ") xs;
-        val (logic, _ :: _ :: h :: _ :: m1 :: m2 :: _ :: s1 :: s2 :: xs2) =
-          take_prefix (not o equal " ") xs1;
-        val cpu = case take_prefix (not o equal ",") xs2 of
-            (_, _ :: _ :: h' :: _ :: m1' :: m2' :: _ :: s1' :: s2' :: _) =>
-              SOME (int_of_string h',
-                int_of_string (m1' ^ m2'), int_of_string (s1' ^ s2'))
-          | _ => NONE
-      in (implode logic,
-        ((int_of_string h, int_of_string (m1 ^ m2), int_of_string (s1 ^ s2)),
-         cpu))
-      end
-  in
-    map get_time xs
-  end;
-
-fun mk_table tab logic =
-  let
-    fun mk_entry (times, (y, (M, D))) = (case AList.lookup op = times logic of
-        SOME (t, t') =>
-          let
-            val (h, m, s) = the_default t t';
-            val date = (100 * ((M - 1) * 31 + D - 1)) div 31;
-            val time = (100 * (h * 3600 + 60 * m + s)) div 60
-          in
-            SOME (Int.toString (date div 100) ^ "." ^ Int.toString (date mod 100) ^ " " ^
-              Int.toString (time div 100) ^ "." ^ Int.toString (time mod 100))
-          end
-      | NONE => (warning ("No session " ^ quote logic ^ " in logfile for " ^
-          Int.toString y ^ "-" ^ Int.toString M ^ "-" ^ Int.toString D); NONE));
-  in
-    space_implode "\n" (List.mapPartial mk_entry tab) ^ "\n"
-  end;
-
-fun mk_tables dir targetdir year compiler =
-  let
-    val files = get_files dir year compiler;
-    val tab = map (fn (d, f, date) => (get_times (d ^ "/" ^ f), date)) files;
-    val logics = map fst (fst (hd tab))
-  in
-    Library.seq (fn logic =>
-      File.write (Path.append (Path.unpack targetdir) (Path.unpack (logic ^ ".dat")))
-        (mk_table tab logic)) logics
-  end;
-
-end
-
-
-(**** Example *****
-
-In ML:
-
-Statistics.mk_tables "/home/isatest/log" "/tmp" "2006" "at-poly";
-
-In Gnuplot:
-
-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"
-
-*******************)
\ No newline at end of file