# HG changeset patch # User wenzelm # Date 1280228362 -7200 # Node ID ce2ea240895c328a9cc717ad5b9ce955b066a8f0 # Parent a79abb22ca9c46a4e7e9d7a8977233255b5b0096 more precise stats; diff -r a79abb22ca9c -r ce2ea240895c Admin/isatest/isatest-statistics --- 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 ;; *) diff -r a79abb22ca9c -r ce2ea240895c Admin/isatest/isatest-stats --- 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