cover AFP logs as well, using "afp" pseudo-platform;
authorwenzelm
Thu Oct 04 16:21:31 2007 +0200 (2007-10-04 ago)
changeset 24831887d1b32a1a5
parent 24830 a7b3ab44d993
child 24832 64cd13299d39
cover AFP logs as well, using "afp" pseudo-platform;
Admin/isatest/isatest-statistics
Admin/isatest/isatest-stats
     1.1 --- a/Admin/isatest/isatest-statistics	Thu Oct 04 14:42:47 2007 +0200
     1.2 +++ b/Admin/isatest/isatest-statistics	Thu Oct 04 16:21:31 2007 +0200
     1.3 @@ -5,21 +5,20 @@
     1.4  #
     1.5  # DESCRIPTION: Produce statistics from isatest session logs.
     1.6  
     1.7 -ISATEST_LOG=~isatest/log
     1.8 -
     1.9  ## platform settings
    1.10  
    1.11  case $(uname) in
    1.12 -	SunOS)	
    1.13 -		ZGREP=xgrep 
    1.14 -		TE="png color"
    1.15 -	;;
    1.16 -	*)	
    1.17 -		ZGREP=zgrep
    1.18 -		TE="png"
    1.19 -	;;
    1.20 +  SunOS)	
    1.21 +    ZGREP=xgrep 
    1.22 +    TE="png color"
    1.23 +    ;;
    1.24 +  *)	
    1.25 +    ZGREP=zgrep
    1.26 +    TE="png"
    1.27 +    ;;
    1.28  esac
    1.29  
    1.30 +
    1.31  ## diagnostics
    1.32  
    1.33  PRG="$(basename "$0")"
    1.34 @@ -52,6 +51,14 @@
    1.35  TIMESPAN="$1"; shift
    1.36  SESSIONS="$@"
    1.37  
    1.38 +if [ "$PLATFORM" = afp ]; then
    1.39 +  LOG_DIR=~isatest/afp-log
    1.40 +  LOG_NAME="afp-test-devel*"
    1.41 +else
    1.42 +  LOG_DIR=~isatest/log
    1.43 +  LOG_NAME="isatest-makeall-${PLATFORM}*"
    1.44 +fi
    1.45 +
    1.46  
    1.47  ## main
    1.48  
    1.49 @@ -60,10 +67,10 @@
    1.50  mkdir -p "$DIR" || fail "Bad directory: $DIR"
    1.51  
    1.52  $ZGREP "^Finished .*elapsed" \
    1.53 -  $(find "$ISATEST_LOG" -name "isatest-makeall-${PLATFORM}*" -ctime "-${TIMESPAN}") | \
    1.54 +  $(find "$LOG_DIR" -name "$LOG_NAME" -ctime "-${TIMESPAN}") | \
    1.55  perl -e '
    1.56    while (<>) {
    1.57 -    if (m/isatest-makeall-.*-(\d+)-(\d+)-(\d+)-.*:Finished (\S+) \(.*, (\d+):(\d+):(\d+) cpu time\)/) {
    1.58 +    if (m/(\d\d\d\d)-(\d\d)-(\d\d).*:Finished (\S+) \(.*, (\d+):(\d+):(\d+) cpu time\)/) {
    1.59          my $year = $1;
    1.60          my $month = $2;
    1.61          my $day = $3;
     2.1 --- a/Admin/isatest/isatest-stats	Thu Oct 04 14:42:47 2007 +0200
     2.2 +++ b/Admin/isatest/isatest-stats	Thu Oct 04 16:21:31 2007 +0200
     2.3 @@ -7,8 +7,9 @@
     2.4  
     2.5  THIS=$(cd "$(dirname "$0")"; pwd -P)
     2.6  
     2.7 -PLATFORMS="at-poly at-sml-dev at-mac-poly-e at64-poly-e at-poly-5.1-para-e at64-poly-5.1-para-e at-mac-poly-5.1-para-e"
     2.8 -SESSIONS="\
     2.9 +PLATFORMS="at-poly at-sml-dev at64-poly-e at64-poly-5.1-para-e at-mac-poly-5.1-para-e afp"
    2.10 +
    2.11 +ISABELLE_SESSIONS="\
    2.12    HOL \
    2.13    HOL-Algebra \
    2.14    HOL-Auth \
    2.15 @@ -30,8 +31,27 @@
    2.16    ZF-Constructible\
    2.17    ZF-UNITY"
    2.18  
    2.19 +AFP_SESSIONS="\
    2.20 +  CoreC++\
    2.21 +  HOL-DiskPaxos\
    2.22 +  HOL-Fermat3_4\
    2.23 +  HOL-Flyspeck-Tame\
    2.24 +  HOL-Group-Ring-Module\
    2.25 +  HOL-Jinja\
    2.26 +  HOL-JiveDataStoreModel\
    2.27 +  HOL-POPLmark-deBruijn\
    2.28 +  HOL-RSAPSS\
    2.29 +  HOL-SumSquares\
    2.30 +  HOL-Valuation"
    2.31 +
    2.32  for PLATFORM in $PLATFORMS
    2.33  do
    2.34 +  if [ "$PLATFORM" = afp ]; then
    2.35 +    SESSIONS="$AFP_SESSIONS"
    2.36 +  else
    2.37 +    SESSIONS="$ISABELLE_SESSIONS"
    2.38 +  fi
    2.39 +
    2.40    "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" ${1:-100} $SESSIONS
    2.41    cat > "stats/$PLATFORM.html" <<EOF
    2.42  <!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">