Admin/isatest/isatest-stats
author wenzelm
Wed Dec 05 20:16:36 2007 +0100 (2007-12-05)
changeset 25547 ffa6e91b7add
parent 24831 887d1b32a1a5
child 26172 fa302c5bc2f2
permissions -rwxr-xr-x
removed -e flag from most sessions;
     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 at64-poly at64-poly-5.1-para at-mac-poly-5.1-para afp"
    11 
    12 ISABELLE_SESSIONS="\
    13   HOL \
    14   HOL-Algebra \
    15   HOL-Auth \
    16   HOL-Bali \
    17   HOL-Complex \
    18   HOL-Complex-ex \
    19   HOL-Extraction \
    20   HOL-Hoare \
    21   HOL-HoareParallel \
    22   HOL-Lambda \
    23   HOL-MetisExamples \
    24   HOL-MicroJava \
    25   HOL-Nominal-Examples \
    26   HOL-NumberTheory \
    27   HOL-SET-Protocol \
    28   HOL-UNITY \
    29   HOL-ex \
    30   ZF \
    31   ZF-Constructible\
    32   ZF-UNITY"
    33 
    34 AFP_SESSIONS="\
    35   CoreC++\
    36   HOL-DiskPaxos\
    37   HOL-Fermat3_4\
    38   HOL-Flyspeck-Tame\
    39   HOL-Group-Ring-Module\
    40   HOL-Jinja\
    41   HOL-JiveDataStoreModel\
    42   HOL-POPLmark-deBruijn\
    43   HOL-RSAPSS\
    44   HOL-SumSquares\
    45   HOL-Valuation"
    46 
    47 for PLATFORM in $PLATFORMS
    48 do
    49   if [ "$PLATFORM" = afp ]; then
    50     SESSIONS="$AFP_SESSIONS"
    51   else
    52     SESSIONS="$ISABELLE_SESSIONS"
    53   fi
    54 
    55   "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" ${1:-100} $SESSIONS
    56   cat > "stats/$PLATFORM.html" <<EOF
    57 <!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
    58 <html>
    59 <head><title>Development Snapshot -- Performance Statistics</title></head>
    60 
    61 <body>
    62 <h1>$PLATFORM</h1>
    63 EOF
    64 
    65 for SESSION in $SESSIONS
    66 do
    67   echo "<br><img src="$PLATFORM/$SESSION.png"><br>" >> "stats/$PLATFORM.html"
    68 done
    69 
    70 echo "</body>" >> "stats/$PLATFORM.html"
    71 echo "</html>" >> "stats/$PLATFORM.html"
    72 
    73 done