Admin/isatest/isatest-stats
author wenzelm
Thu Jul 03 19:17:52 2008 +0200 (2008-07-03)
changeset 27478 ac3b0f881d89
parent 27448 28914fe628c8
child 28530 843b35caa8c4
permissions -rwxr-xr-x
more 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 at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para afp"
    11 
    12 ISABELLE_SESSIONS="\
    13   HOL-Plain \
    14   HOL \
    15   HOL-Algebra \
    16   HOL-Auth \
    17   HOL-Bali \
    18   HOL-Complex \
    19   HOL-Complex-ex \
    20   HOL-Extraction \
    21   HOL-Hoare \
    22   HOL-HoareParallel \
    23   HOL-Lambda \
    24   HOL-Library \
    25   HOL-MetisExamples \
    26   HOL-MicroJava \
    27   HOL-NSA \
    28   HOL-Nominal-Examples \
    29   HOL-NumberTheory \
    30   HOL-SET-Protocol \
    31   HOL-UNITY \
    32   HOL-Word \
    33   HOL-ex \
    34   ZF \
    35   ZF-Constructible\
    36   ZF-UNITY"
    37 
    38 AFP_SESSIONS="\
    39   CoreC++\
    40   LinearQuantifierElim\
    41   HOL-DiskPaxos\
    42   HOL-Fermat3_4\
    43   HOL-Flyspeck-Tame\
    44   HOL-Group-Ring-Module\
    45   HOL-JinjaThreads\
    46   HOL-Jinja\
    47   HOL-JiveDataStoreModel\
    48   HOL-POPLmark-deBruijn\
    49   HOL-Program-Conflict-Analysis\
    50   HOL-RSAPSS\
    51   HOL-Recursion-Theory-I\
    52   HOL-SumSquares\
    53   HOL-Topology\
    54   HOL-Valuation\
    55   Simpl-BDD\
    56   Simpl"
    57 
    58 for PLATFORM in $PLATFORMS
    59 do
    60   if [ "$PLATFORM" = afp ]; then
    61     SESSIONS="$AFP_SESSIONS"
    62   else
    63     SESSIONS="$ISABELLE_SESSIONS"
    64   fi
    65 
    66   "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" ${1:-100} $SESSIONS
    67   cat > "stats/$PLATFORM.html" <<EOF
    68 <!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
    69 <html>
    70 <head><title>Development Snapshot -- Performance Statistics</title></head>
    71 
    72 <body>
    73 <h1>$PLATFORM</h1>
    74 EOF
    75 
    76 for SESSION in $SESSIONS
    77 do
    78   echo "<br><img src="$PLATFORM/$SESSION.png"><br>" >> "stats/$PLATFORM.html"
    79 done
    80 
    81 echo "</body>" >> "stats/$PLATFORM.html"
    82 echo "</html>" >> "stats/$PLATFORM.html"
    83 
    84 done