Simple ML script for producing Gnuplot files from
isatest log files.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest_statistics.ML Mon Aug 07 17:43:51 2006 +0200
@@ -0,0 +1,116 @@
+(* 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 \"cpu 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 (_, _ :: _ :: h' :: _ :: m1' :: m2' :: _ :: s1' :: s2' :: _) =
+ take_prefix (not o equal ",") xs2
+ in (implode logic,
+ ((int_of_string h, int_of_string (m1 ^ m2), int_of_string (s1 ^ s2)),
+ (int_of_string h', int_of_string (m1' ^ m2'), int_of_string (s1' ^ s2'))))
+ 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 (_, (h, m, s)) =>
+ let
+ 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