Admin/isatest/isatest-stats
author wenzelm
Fri Oct 14 11:34:30 2011 +0200 (2011-10-14)
changeset 45142 97e81a8aa277
parent 44993 9a2d100dd3eb
child 45194 d825a8f1d088
permissions -rwxr-xr-x
more complete stats, including small sessions which provide some clues on main HOL baseline performance;
     1 #!/usr/bin/env bash
     2 #
     3 # Author: Makarius
     4 #
     5 # DESCRIPTION: Standard statistics.
     6 
     7 THIS="$(cd "$(dirname "$0")"; pwd)"
     8 
     9 PLATFORMS="at-poly at-poly-test afp at64-poly cygwin-poly-e mac-poly-M2 mac-poly-M4 mac-poly64-M2 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-Auth \
    13   HOL-Bali \
    14   HOL-Boogie-Examples \
    15   HOL-Decision_Procs \
    16   HOL-Hahn_Banach \
    17   HOL-Hoare \
    18   HOL-Hoare_Parallel \
    19   HOL-IMPP \
    20   HOL-IOA \
    21   HOL-Imperative_HOL \
    22   HOL-Import \
    23   HOL-Induct \
    24   HOL-Isar_Examples \
    25   HOL-Lattice \
    26   HOL-Library-Codegenerator_Test \
    27   HOL-Matrix \
    28   HOL-Metis_Examples \
    29   HOL-MicroJava \
    30   HOL-Mirabelle \
    31   HOL-Mutabelle \
    32   HOL-NanoJava \
    33   HOL-Nitpick_Examples \
    34   HOL-Nominal-Examples
    35   HOL-Number_Theory \
    36   HOL-Old_Number_Theory \
    37   HOL-Predicate_Compile_Examples \
    38   HOL-Probability
    39   HOL-Prolog \
    40   HOL-Proofs-Extraction \
    41   HOL-Proofs-Lambda \
    42   HOL-Proofs-ex \
    43   HOL-Quotient_Examples \
    44   HOL-SET_Protocol \
    45   HOL-SPARK-Examples \
    46   HOL-SPARK-Manual \
    47   HOL-Statespace \
    48   HOL-TPTP \
    49   HOL-UNITY \
    50   HOL-Unix \
    51   HOL-Word-Examples \
    52   HOL-Word-SMT_Examples \
    53   HOL-ZF
    54   HOL-ex \
    55   HOLCF-FOCUS \
    56   HOLCF-IMP \
    57   HOLCF-Library \
    58   HOLCF-Tutorial \
    59   HOLCF-ex \
    60   IOA-ABP \
    61   IOA-NTP \
    62   IOA-Storage \
    63   IOA-ex \
    64   TLA-Buffer \
    65   TLA-Inc \
    66   TLA-Memory"
    67 
    68 AFP_SESSIONS="\
    69   ArrowImpossibilityGS \
    70   Coinductive \
    71   CoreC++ \
    72   HOL-AVL-Trees \
    73   HOL-Abstract-Hoare-Logics \
    74   HOL-Abstract-Rewriting \
    75   HOL-BinarySearchTree \
    76   HOL-Binomial-Heaps \
    77   HOL-Binomial-Queues \
    78   HOL-BytecodeLogicJmlTypes \
    79   HOL-Category \
    80   HOL-Category2 \
    81   HOL-Cauchy \
    82   HOL-ClockSynchInst \
    83   HOL-CofGroups \
    84   HOL-Collections \
    85   HOL-Compiling-Exceptions-Correctly \
    86   HOL-Completeness \
    87   HOL-DPT-SAT-Solver \
    88   HOL-DataRefinementIBP \
    89   HOL-Depth-First-Search \
    90   HOL-DiskPaxos \
    91   HOL-Example-Submission \
    92   HOL-FFT \
    93   HOL-FOL-Fitting \
    94   HOL-FeatherweightJava \
    95   HOL-FileRefinement \
    96   HOL-FinFun \
    97   HOL-Finger-Trees \
    98   HOL-Flyspeck-Tame \
    99   HOL-Free-Boolean-Algebra \
   100   HOL-Free-Groups \
   101   HOL-FunWithFunctions \
   102   HOL-FunWithTilings \
   103   HOL-Functional-Automata \
   104   HOL-Gauss-Jordan-Elim-Fun \
   105   HOL-GenClock \
   106   HOL-General-Triangle \
   107   HOL-GraphMarkingIBP \
   108   HOL-HotelKeyCards \
   109   HOL-Huffman \
   110   HOL-Integration \
   111   HOL-JiveDataStoreModel \
   112   HOL-KBPs \
   113   HOL-Lazy-Lists-II \
   114   HOL-LightweightJava \
   115   HOL-List-Index \
   116   HOL-Locally-Nameless-Sigma \
   117   HOL-Marriage \
   118   HOL-Matrix \
   119   HOL-Max-Card-Matching \
   120   HOL-MiniML \
   121   HOL-MuchAdoAboutTwo \
   122   HOL-Multivariate_Analysis \
   123   HOL-Myhill-Nerode \
   124   HOL-Nominal \
   125   HOL-Nominal-Lam-ml-Normalization \
   126   HOL-Nominal-SequentInvertibility \
   127   HOL-Ordinal \
   128   HOL-Ordinals_and_Cardinals \
   129   HOL-POPLmark-deBruijn \
   130   HOL-Perfect-Number-Thm \
   131   HOL-Polynomials \
   132   HOL-Presburger-Automata \
   133   HOL-Program-Conflict-Analysis \
   134   HOL-Ramsey-Infinite \
   135   HOL-Recursion-Theory-I \
   136   HOL-Regular-Sets \
   137   HOL-Robbins-Conjecture \
   138   HOL-SATSolverVerification \
   139   HOL-SIFPL \
   140   HOL-SenSocialChoice \
   141   HOL-Statecharts \
   142   HOL-Topology \
   143   HOL-Transitive-Closure \
   144   HOL-Tree-Automata \
   145   HOL-Verified-Prover \
   146   HOL-Word \
   147   HOL-Word-RIPEMD-160-SPARK \
   148   HOLCF \
   149   HOLCF-Shivers-CFA \
   150   HOLCF-Stream-Fusion \
   151   HOLCF-WorkerWrapper \
   152   HRB-Slicing \
   153   HRB-Slicing-InformationFlowSlicing \
   154   Jinja \
   155   Jinja \
   156   LatticeProperties \
   157   LatticeProperties-MonoBoolTranAlgebra \
   158   LatticeProperties-PseudoHoops \
   159   Lower_Semicontinuous \
   160   NormByEval \
   161   Simpl \
   162   Simpl-BDD \
   163   Slicing \
   164   Slicing \
   165   Slicing-InformationFlowSlicing \
   166   VolpanoSmith"
   167 
   168 
   169 for PLATFORM in $PLATFORMS
   170 do
   171   if [ "$PLATFORM" = afp ]; then
   172     SESSIONS="$AFP_SESSIONS"
   173   else
   174     SESSIONS="$ISABELLE_SESSIONS"
   175   fi
   176 
   177   "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" ${1:-100} $SESSIONS
   178   cat > "stats/$PLATFORM.html" <<EOF
   179 <!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
   180 <html>
   181 <head><title>Development Snapshot -- Performance Statistics</title></head>
   182 
   183 <body>
   184 <h1>$PLATFORM</h1>
   185 EOF
   186 
   187 for SESSION in $SESSIONS
   188 do
   189   echo "<br><img src="$PLATFORM/$SESSION.png"><br>" >> "stats/$PLATFORM.html"
   190 done
   191 
   192 echo "</body>" >> "stats/$PLATFORM.html"
   193 echo "</html>" >> "stats/$PLATFORM.html"
   194 
   195 done