author  berghofe 
Tue, 08 Aug 2006 12:28:00 +0200  
changeset 20359  517236b1bb1d 
parent 20347  1ffbe17cef38 
permissions  rwrr 
20347  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 ("isatestmakeall" ^ 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 

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  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; 

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  70 
in (implode logic, 
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  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 

20359
517236b1bb1d
Adapted to older logfiles containing no cpu time.
berghofe
parents:
20347
diff
changeset

81 
SOME (t, t') => 
20347  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  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" "atpoly"; 

115 

116 
In Gnuplot: 

117 

118 
plot [0:8] [0:40] '/tmp/HOL.dat' smooth sbezier title "HOL", '/tmp/HOLAuth.dat' smooth sbezier title "HOLAuth", '/tmp/HOLComplex.dat' smooth sbezier title "HOLComplex", '/tmp/HOLUNITY.dat' smooth sbezier title "HOLUNITY", '/tmp/HOLBali.dat' smooth sbezier title "HOLBali", '/tmp/HOLMicroJava.dat' smooth sbezier title "HOLMicroJava" 

119 

120 
*******************) 