Admin/isatest/isatest-stats
author kleing
Mon Mar 05 22:12:20 2007 +0100 (2007-03-05)
changeset 22410 da313b67a04d
child 23443 fd8ffc8a5709
permissions -rwxr-xr-x
moved all isatest/cron job related files to own directory
     1 #!/usr/bin/env bash
     2 #
     3 # $Id$
     4 # Author: Makarius
     5 #
     6 # DESCRIPTION: Standard statistics.
     7 
     8 THIS=$(cd "$(dirname "$0")"; pwd -P)
     9 
    10 PLATFORMS="at-poly at-sml-dev at-mac-poly-e at64-poly-e"
    11 SESSIONS="\
    12   HOL \
    13   HOL-Algebra \
    14   HOL-Auth \
    15   HOL-Bali \
    16   HOL-Complex \
    17   HOL-Complex-ex \
    18   HOL-Extraction \
    19   HOL-Hoare \
    20   HOL-HoareParallel \
    21   HOL-Lambda \
    22   HOL-MicroJava \
    23   HOL-NumberTheory \
    24   HOL-SET-Protocol \
    25   HOL-UNITY \
    26   HOL-ex \
    27   ZF \
    28   ZF-Constructible\
    29   ZF-UNITY"
    30 
    31 for PLATFORM in $PLATFORMS
    32 do
    33   "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" ${1:-100} $SESSIONS
    34   cat > "stats/$PLATFORM.html" <<EOF
    35 <!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
    36 <html>
    37 <head><title>Development Snapshot -- Performance Statistics</title></head>
    38 
    39 <body>
    40 <h1>$PLATFORM</h1>
    41 EOF
    42 
    43 for SESSION in $SESSIONS
    44 do
    45   echo "<br><img src="$PLATFORM/$SESSION.png"><br>" >> "stats/$PLATFORM.html"
    46 done
    47 
    48 echo "</body>" >> "stats/$PLATFORM.html"
    49 echo "</html>" >> "stats/$PLATFORM.html"
    50 
    51 done