Admin/isatest/isatest-statistics
author blanchet
Mon, 19 May 2014 23:43:53 +0200
changeset 57005 33f3d2ea803d
parent 49937 463cdbfba8c7
permissions -rwxr-xr-x
store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     1
#!/usr/bin/env bash
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     2
#
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     3
# Author: Makarius
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     4
#
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     5
# DESCRIPTION: Produce statistics from isatest session logs.
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     6
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     7
## platform settings
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     8
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     9
case $(uname) in
24831
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 22410
diff changeset
    10
  SunOS)	
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 22410
diff changeset
    11
    ZGREP=xgrep 
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 22410
diff changeset
    12
    TE="png color"
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 22410
diff changeset
    13
    ;;
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 22410
diff changeset
    14
  *)	
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 22410
diff changeset
    15
    ZGREP=zgrep
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 22410
diff changeset
    16
    TE="png"
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 22410
diff changeset
    17
    ;;
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    18
esac
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    19
24831
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 22410
diff changeset
    20
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    21
## diagnostics
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    22
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    23
PRG="$(basename "$0")"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    24
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    25
function usage()
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    26
{
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    27
  echo
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    28
  echo "Usage: $PRG DIR PLATFORM TIMESPAN SESSIONS..."
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    29
  echo
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    30
  echo "  Produce statistics from isatest session logs, looking TIMESPAN"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    31
  echo "  days into the past.  Outputs .png files into DIR."
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    32
  echo
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    33
  exit 1
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    34
}
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    35
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    36
function fail()
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    37
{
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    38
  echo "$1" >&2
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    39
  exit 2
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    40
}
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    41
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    42
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    43
## arguments
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    44
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    45
[ "$1" = "-?" ] && usage
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    46
[ "$#" -lt "4" ] && usage
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    47
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    48
DIR="$1"; shift
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    49
PLATFORM="$1"; shift
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    50
TIMESPAN="$1"; shift
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    51
SESSIONS="$@"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    52
25453
80557dafd2a0 include elapsed time for parallel sessions;
wenzelm
parents: 24831
diff changeset
    53
case "$PLATFORM" in
37976
ce2ea240895c more precise stats;
wenzelm
parents: 37160
diff changeset
    54
  *para* | *-M* | afp)
25453
80557dafd2a0 include elapsed time for parallel sessions;
wenzelm
parents: 24831
diff changeset
    55
    PARALLEL=true
80557dafd2a0 include elapsed time for parallel sessions;
wenzelm
parents: 24831
diff changeset
    56
    ;;
80557dafd2a0 include elapsed time for parallel sessions;
wenzelm
parents: 24831
diff changeset
    57
  *)
80557dafd2a0 include elapsed time for parallel sessions;
wenzelm
parents: 24831
diff changeset
    58
    PARALLEL=false
80557dafd2a0 include elapsed time for parallel sessions;
wenzelm
parents: 24831
diff changeset
    59
    ;;
80557dafd2a0 include elapsed time for parallel sessions;
wenzelm
parents: 24831
diff changeset
    60
esac
80557dafd2a0 include elapsed time for parallel sessions;
wenzelm
parents: 24831
diff changeset
    61
24831
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 22410
diff changeset
    62
if [ "$PLATFORM" = afp ]; then
44178
04b3d8327c12 point isatest-statistics to the right afp log files
kleing
parents: 37976
diff changeset
    63
  LOG_DIR=~isatest/afp/log
24831
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 22410
diff changeset
    64
  LOG_NAME="afp-test-devel*"
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 22410
diff changeset
    65
else
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 22410
diff changeset
    66
  LOG_DIR=~isatest/log
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 22410
diff changeset
    67
  LOG_NAME="isatest-makeall-${PLATFORM}*"
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 22410
diff changeset
    68
fi
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform;
wenzelm
parents: 22410
diff changeset
    69
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    70
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    71
## main
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    72
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    73
ALL_DATA="/tmp/isatest-all$$.dat"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    74
SESSION_DATA="/tmp/isatest$$.dat"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    75
mkdir -p "$DIR" || fail "Bad directory: $DIR"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    76
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    77
$ZGREP "^Finished .*elapsed" \
49937
463cdbfba8c7 proper find -mtime (file data) instead of -ctime (meta data);
wenzelm
parents: 44178
diff changeset
    78
  $(find "$LOG_DIR" -name "$LOG_NAME" -mtime "-${TIMESPAN}") | \
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    79
perl -e '
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    80
  while (<>) {
28467
c8336c42668e include factor in timing report;
wenzelm
parents: 25480
diff changeset
    81
    if (m/(\d\d\d\d)-(\d\d)-(\d\d).*:Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time/) {
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    82
        my $year = $1;
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    83
        my $month = $2;
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    84
        my $day = $3;
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    85
        my $name = $4;
25453
80557dafd2a0 include elapsed time for parallel sessions;
wenzelm
parents: 24831
diff changeset
    86
        my $elapsed_time = ($5 * 3600 + $6 * 60 + $7) / 60;
80557dafd2a0 include elapsed time for parallel sessions;
wenzelm
parents: 24831
diff changeset
    87
        my $cpu_time = ($8 * 3600 + $9 * 60 + $10) / 60;
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    88
25453
80557dafd2a0 include elapsed time for parallel sessions;
wenzelm
parents: 24831
diff changeset
    89
        printf "$name $year-$month-$day %.2f %.2f\n", $cpu_time, $elapsed_time;
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    90
    }
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    91
  }' > "$ALL_DATA"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    92
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    93
for SESSION in $SESSIONS
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    94
do
29426
0a1d32bc5ee5 slightly more robust matching of session name;
wenzelm
parents: 28467
diff changeset
    95
  grep "^${SESSION} " "$ALL_DATA" > "$SESSION_DATA"
25480
1bada8ff8122 tuned titles;
wenzelm
parents: 25479
diff changeset
    96
  PLOT="plot [] [0:] \"$SESSION_DATA\" using 2:3 smooth sbezier title \"interpolated cpu time\", \"$SESSION_DATA\" using 2:3 smooth csplines title \"cpu time\""
25453
80557dafd2a0 include elapsed time for parallel sessions;
wenzelm
parents: 24831
diff changeset
    97
  if [ "$PARALLEL" = true ]; then
25480
1bada8ff8122 tuned titles;
wenzelm
parents: 25479
diff changeset
    98
    PLOT="${PLOT}, \"$SESSION_DATA\" using 2:4 smooth sbezier title \"interpolated elapsed time\", \"$SESSION_DATA\" using 2:4 smooth csplines title \"elapsed time\""
25453
80557dafd2a0 include elapsed time for parallel sessions;
wenzelm
parents: 24831
diff changeset
    99
  fi
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   100
  gnuplot <<EOF
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   101
set terminal $TE
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   102
set output "$DIR/${SESSION}.png"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   103
set xdata time
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   104
set timefmt "%Y-%m-%d"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   105
set format x "%d-%b"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   106
set xlabel "$SESSION"
25479
139b8843873b moved titles;
wenzelm
parents: 25478
diff changeset
   107
set key left top
25453
80557dafd2a0 include elapsed time for parallel sessions;
wenzelm
parents: 24831
diff changeset
   108
$PLOT
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   109
EOF
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   110
done
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   111
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   112
rm -f "$ALL_DATA" "$SESSION_DATA"