more precise stats;
authorwenzelm
Tue Jul 27 12:59:22 2010 +0200 (2010-07-27)
changeset 37976ce2ea240895c
parent 37975 a79abb22ca9c
child 37977 3ceccd415145
more precise stats;
Admin/isatest/isatest-statistics
Admin/isatest/isatest-stats
     1.1 --- a/Admin/isatest/isatest-statistics	Mon Jul 26 18:25:19 2010 +0200
     1.2 +++ b/Admin/isatest/isatest-statistics	Tue Jul 27 12:59:22 2010 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4  SESSIONS="$@"
     1.5  
     1.6  case "$PLATFORM" in
     1.7 -  *para* | *-M*)
     1.8 +  *para* | *-M* | afp)
     1.9      PARALLEL=true
    1.10      ;;
    1.11    *)
     2.1 --- a/Admin/isatest/isatest-stats	Mon Jul 26 18:25:19 2010 +0200
     2.2 +++ b/Admin/isatest/isatest-stats	Tue Jul 27 12:59:22 2010 +0200
     2.3 @@ -6,20 +6,21 @@
     2.4  
     2.5  THIS=$(cd "$(dirname "$0")"; pwd -P)
     2.6  
     2.7 -PLATFORMS="at-poly at-poly-test at64-poly cygwin-poly mac-poly-M4 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para afp at-sml-dev"
     2.8 +PLATFORMS="at-poly at-poly-test afp at64-poly cygwin-poly mac-poly-M4 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para at-sml-dev"
     2.9  
    2.10  ISABELLE_SESSIONS="\
    2.11    HOL-Plain \
    2.12    HOL-Main \
    2.13    HOL \
    2.14    HOL-Proofs \
    2.15 +  HOL-Library \
    2.16    HOL-Algebra \
    2.17    HOL-Auth \
    2.18    HOL-Bali \
    2.19    HOL-Decision_Procs \
    2.20    HOL-Hoare \
    2.21    HOL-Hoare_Parallel \
    2.22 -  HOL-Library \
    2.23 +  HOL-Imperative_HOL \
    2.24    HOL-Metis_Examples \
    2.25    HOL-MicroJava \
    2.26    HOL-Multivariate_Analysis \
    2.27 @@ -27,11 +28,13 @@
    2.28    HOL-Nominal-Examples \
    2.29    HOL-Number_Theory \
    2.30    HOL-Old_Number_Theory \
    2.31 +  HOL-Predicate_Compile_Examples \
    2.32    HOL-Proofs-Extraction \
    2.33    HOL-Proofs-Lambda \
    2.34    HOL-SET_Protocol \
    2.35    HOL-UNITY \
    2.36    HOL-Word \
    2.37 +  HOL-Word-SMT_Examples \
    2.38    HOL-ex \
    2.39    HOLCF \
    2.40    IOA \
    2.41 @@ -40,17 +43,23 @@
    2.42    ZF-UNITY"
    2.43  
    2.44  AFP_SESSIONS="\
    2.45 +  Coinductive \
    2.46    CoreC++ \
    2.47 -  Jinja-Slicing \
    2.48 +  Group-Ring-Module \
    2.49 +  Group-Ring-Module-Valuation \
    2.50    HOL-BytecodeLogicJmlTypes \
    2.51 +  HOL-Collections \
    2.52    HOL-DiskPaxos \
    2.53 +  HOL-FeatherweightJava \
    2.54    HOL-Fermat3_4 \
    2.55    HOL-Flyspeck-Tame \
    2.56 -  HOL-Group-Ring-Module \
    2.57 -  HOL-Jinja \
    2.58 -  HOL-JinjaThreads \
    2.59 +  HOL-Free-Groups \
    2.60 +  HOL-GraphMarkingIBP \
    2.61    HOL-JiveDataStoreModel \
    2.62 +  HOL-Locally-Nameless-Sigma \
    2.63 +  HOL-Ordinals_and_Cardinals \
    2.64    HOL-POPLmark-deBruijn \
    2.65 +  HOL-Presburger-Automata \
    2.66    HOL-Program-Conflict-Analysis \
    2.67    HOL-RSAPSS \
    2.68    HOL-Recursion-Theory-I \
    2.69 @@ -59,10 +68,17 @@
    2.70    HOL-SenSocialChoice \
    2.71    HOL-SumSquares \
    2.72    HOL-Topology \
    2.73 -  HOL-Valuation \
    2.74 +  HOL-Tree-Automata \
    2.75 +  HOL-Word-JinjaThreads \
    2.76 +  HOLCF-WorkerWrapper \
    2.77 +  HRB-Slicing \
    2.78 +  Jinja \
    2.79 +  Jinja-Slicing \
    2.80    LinearQuantifierElim \
    2.81    Simpl \
    2.82 -  Simpl-BDD"
    2.83 +  Simpl-BDD \
    2.84 +  Slicing \
    2.85 +  Slicing-InformationFlowSlicing"
    2.86  
    2.87  for PLATFORM in $PLATFORMS
    2.88  do