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

#!/usr/bin/env bash
#
# Author: Makarius
#
# DESCRIPTION: Produce statistics from isatest session logs.

## platform settings

case $(uname) in
  SunOS)	
    ZGREP=xgrep 
    TE="png color"
    ;;
  *)	
    ZGREP=zgrep
    TE="png"
    ;;
esac


## diagnostics

PRG="$(basename "$0")"

function usage()
{
  echo
  echo "Usage: $PRG DIR PLATFORM TIMESPAN SESSIONS..."
  echo
  echo "  Produce statistics from isatest session logs, looking TIMESPAN"
  echo "  days into the past.  Outputs .png files into DIR."
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}


## arguments

[ "$1" = "-?" ] && usage
[ "$#" -lt "4" ] && usage

DIR="$1"; shift
PLATFORM="$1"; shift
TIMESPAN="$1"; shift
SESSIONS="$@"

case "$PLATFORM" in
  *para* | *-M* | afp)
    PARALLEL=true
    ;;
  *)
    PARALLEL=false
    ;;
esac

if [ "$PLATFORM" = afp ]; then
  LOG_DIR=~isatest/afp/log
  LOG_NAME="afp-test-devel*"
else
  LOG_DIR=~isatest/log
  LOG_NAME="isatest-makeall-${PLATFORM}*"
fi


## main

ALL_DATA="/tmp/isatest-all$$.dat"
SESSION_DATA="/tmp/isatest$$.dat"
mkdir -p "$DIR" || fail "Bad directory: $DIR"

$ZGREP "^Finished .*elapsed" \
  $(find "$LOG_DIR" -name "$LOG_NAME" -mtime "-${TIMESPAN}") | \
perl -e '
  while (<>) {
    if (m/(\d\d\d\d)-(\d\d)-(\d\d).*:Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time/) {
        my $year = $1;
        my $month = $2;
        my $day = $3;
        my $name = $4;
        my $elapsed_time = ($5 * 3600 + $6 * 60 + $7) / 60;
        my $cpu_time = ($8 * 3600 + $9 * 60 + $10) / 60;

        printf "$name $year-$month-$day %.2f %.2f\n", $cpu_time, $elapsed_time;
    }
  }' > "$ALL_DATA"

for SESSION in $SESSIONS
do
  grep "^${SESSION} " "$ALL_DATA" > "$SESSION_DATA"
  PLOT="plot [] [0:] \"$SESSION_DATA\" using 2:3 smooth sbezier title \"interpolated cpu time\", \"$SESSION_DATA\" using 2:3 smooth csplines title \"cpu time\""
  if [ "$PARALLEL" = true ]; then
    PLOT="${PLOT}, \"$SESSION_DATA\" using 2:4 smooth sbezier title \"interpolated elapsed time\", \"$SESSION_DATA\" using 2:4 smooth csplines title \"elapsed time\""
  fi
  gnuplot <<EOF
set terminal $TE
set output "$DIR/${SESSION}.png"
set xdata time
set timefmt "%Y-%m-%d"
set format x "%d-%b"
set xlabel "$SESSION"
set key left top
$PLOT
EOF
done

rm -f "$ALL_DATA" "$SESSION_DATA"