Admin/isatest/isatest-stats
author wenzelm
Sat Mar 21 12:35:34 2009 +0100 (2009-03-21)
changeset 30616 ac79f1bb5db3
parent 30111 01a87bc13415
child 30700 dc38bb27df50
permissions -rwxr-xr-x
more stats;
     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-Main \
    15   HOL \
    16   HOL-Algebra \
    17   HOL-Auth \
    18   HOL-Bali \
    19   HOL-Decision_Procs \
    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   HOLCF \
    35   IOA \
    36   ZF \
    37   ZF-Constructible \
    38   ZF-UNITY"
    39 
    40 AFP_SESSIONS="\
    41   CoreC++ \
    42   HOL-BytecodeLogicJmlTypes \
    43   HOL-DiskPaxos \
    44   HOL-Fermat3_4 \
    45   HOL-Flyspeck-Tame \
    46   HOL-Group-Ring-Module \
    47   HOL-Jinja \
    48   HOL-JinjaThreads \
    49   HOL-JiveDataStoreModel \
    50   HOL-POPLmark-deBruijn \
    51   HOL-Program-Conflict-Analysis \
    52   HOL-RSAPSS \
    53   HOL-Recursion-Theory-I \
    54   HOL-SATSolverVerification \
    55   HOL-SIFPL \
    56   HOL-SenSocialChoice \
    57   HOL-Slicing \
    58   HOL-SumSquares \
    59   HOL-Topology \
    60   HOL-Valuation \
    61   LinearQuantifierElim \
    62   Simpl \
    63   Simpl-BDD"
    64 
    65 for PLATFORM in $PLATFORMS
    66 do
    67   if [ "$PLATFORM" = afp ]; then
    68     SESSIONS="$AFP_SESSIONS"
    69   else
    70     SESSIONS="$ISABELLE_SESSIONS"
    71   fi
    72 
    73   "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" ${1:-100} $SESSIONS
    74   cat > "stats/$PLATFORM.html" <<EOF
    75 <!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
    76 <html>
    77 <head><title>Development Snapshot -- Performance Statistics</title></head>
    78 
    79 <body>
    80 <h1>$PLATFORM</h1>
    81 EOF
    82 
    83 for SESSION in $SESSIONS
    84 do
    85   echo "<br><img src="$PLATFORM/$SESSION.png"><br>" >> "stats/$PLATFORM.html"
    86 done
    87 
    88 echo "</body>" >> "stats/$PLATFORM.html"
    89 echo "</html>" >> "stats/$PLATFORM.html"
    90 
    91 done