more complete stats, including small sessions which provide some clues on main HOL baseline performance;
authorwenzelm
Fri Oct 14 11:34:30 2011 +0200 (2011-10-14)
changeset 4514297e81a8aa277
parent 45141 b2eb87bd541b
child 45143 aed8f14bf562
child 45145 d5086da3c32d
more complete stats, including small sessions which provide some clues on main HOL baseline performance;
Admin/isatest/isatest-stats
     1.1 --- a/Admin/isatest/isatest-stats	Thu Oct 13 23:35:15 2011 +0200
     1.2 +++ b/Admin/isatest/isatest-stats	Fri Oct 14 11:34:30 2011 +0200
     1.3 @@ -9,76 +9,162 @@
     1.4  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"
     1.5  
     1.6  ISABELLE_SESSIONS="\
     1.7 -  HOL-Plain \
     1.8 -  HOL-Main \
     1.9 -  HOL \
    1.10 -  HOL-Proofs \
    1.11 -  HOL-Library \
    1.12 -  HOL-Algebra \
    1.13    HOL-Auth \
    1.14    HOL-Bali \
    1.15 +  HOL-Boogie-Examples \
    1.16    HOL-Decision_Procs \
    1.17 +  HOL-Hahn_Banach \
    1.18    HOL-Hoare \
    1.19    HOL-Hoare_Parallel \
    1.20 +  HOL-IMPP \
    1.21 +  HOL-IOA \
    1.22    HOL-Imperative_HOL \
    1.23 +  HOL-Import \
    1.24 +  HOL-Induct \
    1.25 +  HOL-Isar_Examples \
    1.26 +  HOL-Lattice \
    1.27 +  HOL-Library-Codegenerator_Test \
    1.28 +  HOL-Matrix \
    1.29    HOL-Metis_Examples \
    1.30    HOL-MicroJava \
    1.31 -  HOL-Multivariate_Analysis \
    1.32 -  HOL-NSA \
    1.33 -  HOL-Nominal-Examples \
    1.34 +  HOL-Mirabelle \
    1.35 +  HOL-Mutabelle \
    1.36 +  HOL-NanoJava \
    1.37 +  HOL-Nitpick_Examples \
    1.38 +  HOL-Nominal-Examples
    1.39    HOL-Number_Theory \
    1.40    HOL-Old_Number_Theory \
    1.41    HOL-Predicate_Compile_Examples \
    1.42 +  HOL-Probability
    1.43 +  HOL-Prolog \
    1.44    HOL-Proofs-Extraction \
    1.45    HOL-Proofs-Lambda \
    1.46 +  HOL-Proofs-ex \
    1.47 +  HOL-Quotient_Examples \
    1.48    HOL-SET_Protocol \
    1.49 +  HOL-SPARK-Examples \
    1.50 +  HOL-SPARK-Manual \
    1.51 +  HOL-Statespace \
    1.52 +  HOL-TPTP \
    1.53    HOL-UNITY \
    1.54 -  HOL-Word \
    1.55 +  HOL-Unix \
    1.56 +  HOL-Word-Examples \
    1.57    HOL-Word-SMT_Examples \
    1.58 +  HOL-ZF
    1.59    HOL-ex \
    1.60 -  HOLCF \
    1.61 -  IOA \
    1.62 -  ZF \
    1.63 -  ZF-Constructible \
    1.64 -  ZF-UNITY"
    1.65 +  HOLCF-FOCUS \
    1.66 +  HOLCF-IMP \
    1.67 +  HOLCF-Library \
    1.68 +  HOLCF-Tutorial \
    1.69 +  HOLCF-ex \
    1.70 +  IOA-ABP \
    1.71 +  IOA-NTP \
    1.72 +  IOA-Storage \
    1.73 +  IOA-ex \
    1.74 +  TLA-Buffer \
    1.75 +  TLA-Inc \
    1.76 +  TLA-Memory"
    1.77  
    1.78  AFP_SESSIONS="\
    1.79 +  ArrowImpossibilityGS \
    1.80    Coinductive \
    1.81    CoreC++ \
    1.82 -  Group-Ring-Module \
    1.83 -  Group-Ring-Module-Valuation \
    1.84 +  HOL-AVL-Trees \
    1.85 +  HOL-Abstract-Hoare-Logics \
    1.86 +  HOL-Abstract-Rewriting \
    1.87 +  HOL-BinarySearchTree \
    1.88 +  HOL-Binomial-Heaps \
    1.89 +  HOL-Binomial-Queues \
    1.90    HOL-BytecodeLogicJmlTypes \
    1.91 +  HOL-Category \
    1.92 +  HOL-Category2 \
    1.93 +  HOL-Cauchy \
    1.94 +  HOL-ClockSynchInst \
    1.95 +  HOL-CofGroups \
    1.96    HOL-Collections \
    1.97 +  HOL-Compiling-Exceptions-Correctly \
    1.98 +  HOL-Completeness \
    1.99 +  HOL-DPT-SAT-Solver \
   1.100 +  HOL-DataRefinementIBP \
   1.101 +  HOL-Depth-First-Search \
   1.102    HOL-DiskPaxos \
   1.103 +  HOL-Example-Submission \
   1.104 +  HOL-FFT \
   1.105 +  HOL-FOL-Fitting \
   1.106    HOL-FeatherweightJava \
   1.107 -  HOL-Fermat3_4 \
   1.108 +  HOL-FileRefinement \
   1.109 +  HOL-FinFun \
   1.110 +  HOL-Finger-Trees \
   1.111    HOL-Flyspeck-Tame \
   1.112 +  HOL-Free-Boolean-Algebra \
   1.113    HOL-Free-Groups \
   1.114 +  HOL-FunWithFunctions \
   1.115 +  HOL-FunWithTilings \
   1.116 +  HOL-Functional-Automata \
   1.117 +  HOL-Gauss-Jordan-Elim-Fun \
   1.118 +  HOL-GenClock \
   1.119 +  HOL-General-Triangle \
   1.120    HOL-GraphMarkingIBP \
   1.121 +  HOL-HotelKeyCards \
   1.122 +  HOL-Huffman \
   1.123 +  HOL-Integration \
   1.124    HOL-JiveDataStoreModel \
   1.125 +  HOL-KBPs \
   1.126 +  HOL-Lazy-Lists-II \
   1.127 +  HOL-LightweightJava \
   1.128 +  HOL-List-Index \
   1.129    HOL-Locally-Nameless-Sigma \
   1.130 +  HOL-Marriage \
   1.131 +  HOL-Matrix \
   1.132 +  HOL-Max-Card-Matching \
   1.133 +  HOL-MiniML \
   1.134 +  HOL-MuchAdoAboutTwo \
   1.135 +  HOL-Multivariate_Analysis \
   1.136 +  HOL-Myhill-Nerode \
   1.137 +  HOL-Nominal \
   1.138 +  HOL-Nominal-Lam-ml-Normalization \
   1.139 +  HOL-Nominal-SequentInvertibility \
   1.140 +  HOL-Ordinal \
   1.141    HOL-Ordinals_and_Cardinals \
   1.142    HOL-POPLmark-deBruijn \
   1.143 +  HOL-Perfect-Number-Thm \
   1.144 +  HOL-Polynomials \
   1.145    HOL-Presburger-Automata \
   1.146    HOL-Program-Conflict-Analysis \
   1.147 -  HOL-RSAPSS \
   1.148 +  HOL-Ramsey-Infinite \
   1.149    HOL-Recursion-Theory-I \
   1.150 +  HOL-Regular-Sets \
   1.151 +  HOL-Robbins-Conjecture \
   1.152    HOL-SATSolverVerification \
   1.153    HOL-SIFPL \
   1.154    HOL-SenSocialChoice \
   1.155 -  HOL-SumSquares \
   1.156 +  HOL-Statecharts \
   1.157    HOL-Topology \
   1.158 +  HOL-Transitive-Closure \
   1.159    HOL-Tree-Automata \
   1.160 -  HOL-Word-JinjaThreads \
   1.161 +  HOL-Verified-Prover \
   1.162 +  HOL-Word \
   1.163 +  HOL-Word-RIPEMD-160-SPARK \
   1.164 +  HOLCF \
   1.165 +  HOLCF-Shivers-CFA \
   1.166 +  HOLCF-Stream-Fusion \
   1.167    HOLCF-WorkerWrapper \
   1.168    HRB-Slicing \
   1.169 +  HRB-Slicing-InformationFlowSlicing \
   1.170    Jinja \
   1.171 -  Jinja-Slicing \
   1.172 -  LinearQuantifierElim \
   1.173 +  Jinja \
   1.174 +  LatticeProperties \
   1.175 +  LatticeProperties-MonoBoolTranAlgebra \
   1.176 +  LatticeProperties-PseudoHoops \
   1.177 +  Lower_Semicontinuous \
   1.178 +  NormByEval \
   1.179    Simpl \
   1.180    Simpl-BDD \
   1.181    Slicing \
   1.182 -  Slicing-InformationFlowSlicing"
   1.183 +  Slicing \
   1.184 +  Slicing-InformationFlowSlicing \
   1.185 +  VolpanoSmith"
   1.186 +
   1.187  
   1.188  for PLATFORM in $PLATFORMS
   1.189  do