more precise stats;
authorwenzelm
Tue, 27 Jul 2010 12:59:22 +0200
changeset 37976 ce2ea240895c
parent 37975 a79abb22ca9c
child 37977 3ceccd415145
more precise stats;
Admin/isatest/isatest-statistics
Admin/isatest/isatest-stats
--- a/Admin/isatest/isatest-statistics	Mon Jul 26 18:25:19 2010 +0200
+++ b/Admin/isatest/isatest-statistics	Tue Jul 27 12:59:22 2010 +0200
@@ -51,7 +51,7 @@
 SESSIONS="$@"
 
 case "$PLATFORM" in
-  *para* | *-M*)
+  *para* | *-M* | afp)
     PARALLEL=true
     ;;
   *)
--- a/Admin/isatest/isatest-stats	Mon Jul 26 18:25:19 2010 +0200
+++ b/Admin/isatest/isatest-stats	Tue Jul 27 12:59:22 2010 +0200
@@ -6,20 +6,21 @@
 
 THIS=$(cd "$(dirname "$0")"; pwd -P)
 
-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"
+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"
 
 ISABELLE_SESSIONS="\
   HOL-Plain \
   HOL-Main \
   HOL \
   HOL-Proofs \
+  HOL-Library \
   HOL-Algebra \
   HOL-Auth \
   HOL-Bali \
   HOL-Decision_Procs \
   HOL-Hoare \
   HOL-Hoare_Parallel \
-  HOL-Library \
+  HOL-Imperative_HOL \
   HOL-Metis_Examples \
   HOL-MicroJava \
   HOL-Multivariate_Analysis \
@@ -27,11 +28,13 @@
   HOL-Nominal-Examples \
   HOL-Number_Theory \
   HOL-Old_Number_Theory \
+  HOL-Predicate_Compile_Examples \
   HOL-Proofs-Extraction \
   HOL-Proofs-Lambda \
   HOL-SET_Protocol \
   HOL-UNITY \
   HOL-Word \
+  HOL-Word-SMT_Examples \
   HOL-ex \
   HOLCF \
   IOA \
@@ -40,17 +43,23 @@
   ZF-UNITY"
 
 AFP_SESSIONS="\
+  Coinductive \
   CoreC++ \
-  Jinja-Slicing \
+  Group-Ring-Module \
+  Group-Ring-Module-Valuation \
   HOL-BytecodeLogicJmlTypes \
+  HOL-Collections \
   HOL-DiskPaxos \
+  HOL-FeatherweightJava \
   HOL-Fermat3_4 \
   HOL-Flyspeck-Tame \
-  HOL-Group-Ring-Module \
-  HOL-Jinja \
-  HOL-JinjaThreads \
+  HOL-Free-Groups \
+  HOL-GraphMarkingIBP \
   HOL-JiveDataStoreModel \
+  HOL-Locally-Nameless-Sigma \
+  HOL-Ordinals_and_Cardinals \
   HOL-POPLmark-deBruijn \
+  HOL-Presburger-Automata \
   HOL-Program-Conflict-Analysis \
   HOL-RSAPSS \
   HOL-Recursion-Theory-I \
@@ -59,10 +68,17 @@
   HOL-SenSocialChoice \
   HOL-SumSquares \
   HOL-Topology \
-  HOL-Valuation \
+  HOL-Tree-Automata \
+  HOL-Word-JinjaThreads \
+  HOLCF-WorkerWrapper \
+  HRB-Slicing \
+  Jinja \
+  Jinja-Slicing \
   LinearQuantifierElim \
   Simpl \
-  Simpl-BDD"
+  Simpl-BDD \
+  Slicing \
+  Slicing-InformationFlowSlicing"
 
 for PLATFORM in $PLATFORMS
 do