Admin/isatest/isatest-stats
author wenzelm
Thu Aug 19 18:44:26 2010 +0200 (2010-08-19)
changeset 38561 d2a8087effc6
parent 37976 ce2ea240895c
child 41646 167a045fade4
permissions -rwxr-xr-x
updated some isatest settings;
     1 #!/usr/bin/env bash
     2 #
     3 # Author: Makarius
     4 #
     5 # DESCRIPTION: Standard statistics.
     6 
     7 THIS=$(cd "$(dirname "$0")"; pwd -P)
     8 
     9 PLATFORMS="at-poly at-poly-test afp at64-poly cygwin-poly mac-poly-M4 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at64-poly-5.1-para at-mac-poly-5.1-para at-sml-dev"
    10 
    11 ISABELLE_SESSIONS="\
    12   HOL-Plain \
    13   HOL-Main \
    14   HOL \
    15   HOL-Proofs \
    16   HOL-Library \
    17   HOL-Algebra \
    18   HOL-Auth \
    19   HOL-Bali \
    20   HOL-Decision_Procs \
    21   HOL-Hoare \
    22   HOL-Hoare_Parallel \
    23   HOL-Imperative_HOL \
    24   HOL-Metis_Examples \
    25   HOL-MicroJava \
    26   HOL-Multivariate_Analysis \
    27   HOL-NSA \
    28   HOL-Nominal-Examples \
    29   HOL-Number_Theory \
    30   HOL-Old_Number_Theory \
    31   HOL-Predicate_Compile_Examples \
    32   HOL-Proofs-Extraction \
    33   HOL-Proofs-Lambda \
    34   HOL-SET_Protocol \
    35   HOL-UNITY \
    36   HOL-Word \
    37   HOL-Word-SMT_Examples \
    38   HOL-ex \
    39   HOLCF \
    40   IOA \
    41   ZF \
    42   ZF-Constructible \
    43   ZF-UNITY"
    44 
    45 AFP_SESSIONS="\
    46   Coinductive \
    47   CoreC++ \
    48   Group-Ring-Module \
    49   Group-Ring-Module-Valuation \
    50   HOL-BytecodeLogicJmlTypes \
    51   HOL-Collections \
    52   HOL-DiskPaxos \
    53   HOL-FeatherweightJava \
    54   HOL-Fermat3_4 \
    55   HOL-Flyspeck-Tame \
    56   HOL-Free-Groups \
    57   HOL-GraphMarkingIBP \
    58   HOL-JiveDataStoreModel \
    59   HOL-Locally-Nameless-Sigma \
    60   HOL-Ordinals_and_Cardinals \
    61   HOL-POPLmark-deBruijn \
    62   HOL-Presburger-Automata \
    63   HOL-Program-Conflict-Analysis \
    64   HOL-RSAPSS \
    65   HOL-Recursion-Theory-I \
    66   HOL-SATSolverVerification \
    67   HOL-SIFPL \
    68   HOL-SenSocialChoice \
    69   HOL-SumSquares \
    70   HOL-Topology \
    71   HOL-Tree-Automata \
    72   HOL-Word-JinjaThreads \
    73   HOLCF-WorkerWrapper \
    74   HRB-Slicing \
    75   Jinja \
    76   Jinja-Slicing \
    77   LinearQuantifierElim \
    78   Simpl \
    79   Simpl-BDD \
    80   Slicing \
    81   Slicing-InformationFlowSlicing"
    82 
    83 for PLATFORM in $PLATFORMS
    84 do
    85   if [ "$PLATFORM" = afp ]; then
    86     SESSIONS="$AFP_SESSIONS"
    87   else
    88     SESSIONS="$ISABELLE_SESSIONS"
    89   fi
    90 
    91   "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" ${1:-100} $SESSIONS
    92   cat > "stats/$PLATFORM.html" <<EOF
    93 <!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
    94 <html>
    95 <head><title>Development Snapshot -- Performance Statistics</title></head>
    96 
    97 <body>
    98 <h1>$PLATFORM</h1>
    99 EOF
   100 
   101 for SESSION in $SESSIONS
   102 do
   103   echo "<br><img src="$PLATFORM/$SESSION.png"><br>" >> "stats/$PLATFORM.html"
   104 done
   105 
   106 echo "</body>" >> "stats/$PLATFORM.html"
   107 echo "</html>" >> "stats/$PLATFORM.html"
   108 
   109 done