Admin/isatest-statistics
author haftmann
Tue Oct 10 13:59:12 2006 +0200 (2006-10-10)
changeset 20950 981fa0ce23ed
parent 20651 41a63aabea83
permissions -rwxr-xr-x
added IsarAdvanced material
     1 #!/usr/bin/env bash
     2 #
     3 # $Id$
     4 # Author: Makarius
     5 #
     6 # DESCRIPTION: Produce statistics from isatest session logs.
     7 
     8 ISATEST_LOG=~isatest/log
     9 
    10 ## platform settings
    11 
    12 case $(uname) in
    13 	SunOS)	
    14 		ZGREP=xgrep 
    15 		TE="png color"
    16 	;;
    17 	*)	
    18 		ZGREP=zgrep
    19 		TE="png"
    20 	;;
    21 esac
    22 
    23 ## diagnostics
    24 
    25 PRG="$(basename "$0")"
    26 
    27 function usage()
    28 {
    29   echo
    30   echo "Usage: $PRG DIR PLATFORM TIMESPAN SESSIONS..."
    31   echo
    32   echo "  Produce statistics from isatest session logs, looking TIMESPAN"
    33   echo "  days into the past.  Outputs .png files into DIR."
    34   echo
    35   exit 1
    36 }
    37 
    38 function fail()
    39 {
    40   echo "$1" >&2
    41   exit 2
    42 }
    43 
    44 
    45 ## arguments
    46 
    47 [ "$1" = "-?" ] && usage
    48 [ "$#" -lt "4" ] && usage
    49 
    50 DIR="$1"; shift
    51 PLATFORM="$1"; shift
    52 TIMESPAN="$1"; shift
    53 SESSIONS="$@"
    54 
    55 
    56 ## main
    57 
    58 ALL_DATA="/tmp/isatest-all$$.dat"
    59 SESSION_DATA="/tmp/isatest$$.dat"
    60 mkdir -p "$DIR" || fail "Bad directory: $DIR"
    61 
    62 $ZGREP "^Finished .*elapsed" \
    63   $(find "$ISATEST_LOG" -name "isatest-makeall-${PLATFORM}*" -ctime "-${TIMESPAN}") | \
    64 perl -e '
    65   while (<>) {
    66     if (m/isatest-makeall-.*-(\d+)-(\d+)-(\d+)-.*:Finished (\S+) \(.*, (\d+):(\d+):(\d+) cpu time\)/) {
    67         my $year = $1;
    68         my $month = $2;
    69         my $day = $3;
    70         my $name = $4;
    71         my $time = ($5 * 3600 + $6 * 60 + $7) / 60;
    72 
    73         printf "$name $year-$month-$day %.2f\n", $time;
    74     }
    75   }' > "$ALL_DATA"
    76 
    77 for SESSION in $SESSIONS
    78 do
    79   fgrep "$SESSION " "$ALL_DATA" > "$SESSION_DATA"
    80   gnuplot <<EOF
    81 set terminal $TE
    82 set output "$DIR/${SESSION}.png"
    83 set xdata time
    84 set timefmt "%Y-%m-%d"
    85 set format x "%d-%b"
    86 set xlabel "$SESSION"
    87 plot [] [0:] "$SESSION_DATA" using 2:3 smooth sbezier notitle, "$SESSION_DATA" using 2:3 smooth csplines notitle
    88 EOF
    89 done
    90 
    91 rm -f "$ALL_DATA" "$SESSION_DATA"