--- a/Admin/isatest/isatest-stats Thu Oct 13 23:35:15 2011 +0200
+++ b/Admin/isatest/isatest-stats Fri Oct 14 11:34:30 2011 +0200
@@ -9,76 +9,162 @@
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"
ISABELLE_SESSIONS="\
- HOL-Plain \
- HOL-Main \
- HOL \
- HOL-Proofs \
- HOL-Library \
- HOL-Algebra \
HOL-Auth \
HOL-Bali \
+ HOL-Boogie-Examples \
HOL-Decision_Procs \
+ HOL-Hahn_Banach \
HOL-Hoare \
HOL-Hoare_Parallel \
+ HOL-IMPP \
+ HOL-IOA \
HOL-Imperative_HOL \
+ HOL-Import \
+ HOL-Induct \
+ HOL-Isar_Examples \
+ HOL-Lattice \
+ HOL-Library-Codegenerator_Test \
+ HOL-Matrix \
HOL-Metis_Examples \
HOL-MicroJava \
- HOL-Multivariate_Analysis \
- HOL-NSA \
- HOL-Nominal-Examples \
+ HOL-Mirabelle \
+ HOL-Mutabelle \
+ HOL-NanoJava \
+ HOL-Nitpick_Examples \
+ HOL-Nominal-Examples
HOL-Number_Theory \
HOL-Old_Number_Theory \
HOL-Predicate_Compile_Examples \
+ HOL-Probability
+ HOL-Prolog \
HOL-Proofs-Extraction \
HOL-Proofs-Lambda \
+ HOL-Proofs-ex \
+ HOL-Quotient_Examples \
HOL-SET_Protocol \
+ HOL-SPARK-Examples \
+ HOL-SPARK-Manual \
+ HOL-Statespace \
+ HOL-TPTP \
HOL-UNITY \
- HOL-Word \
+ HOL-Unix \
+ HOL-Word-Examples \
HOL-Word-SMT_Examples \
+ HOL-ZF
HOL-ex \
- HOLCF \
- IOA \
- ZF \
- ZF-Constructible \
- ZF-UNITY"
+ HOLCF-FOCUS \
+ HOLCF-IMP \
+ HOLCF-Library \
+ HOLCF-Tutorial \
+ HOLCF-ex \
+ IOA-ABP \
+ IOA-NTP \
+ IOA-Storage \
+ IOA-ex \
+ TLA-Buffer \
+ TLA-Inc \
+ TLA-Memory"
AFP_SESSIONS="\
+ ArrowImpossibilityGS \
Coinductive \
CoreC++ \
- Group-Ring-Module \
- Group-Ring-Module-Valuation \
+ HOL-AVL-Trees \
+ HOL-Abstract-Hoare-Logics \
+ HOL-Abstract-Rewriting \
+ HOL-BinarySearchTree \
+ HOL-Binomial-Heaps \
+ HOL-Binomial-Queues \
HOL-BytecodeLogicJmlTypes \
+ HOL-Category \
+ HOL-Category2 \
+ HOL-Cauchy \
+ HOL-ClockSynchInst \
+ HOL-CofGroups \
HOL-Collections \
+ HOL-Compiling-Exceptions-Correctly \
+ HOL-Completeness \
+ HOL-DPT-SAT-Solver \
+ HOL-DataRefinementIBP \
+ HOL-Depth-First-Search \
HOL-DiskPaxos \
+ HOL-Example-Submission \
+ HOL-FFT \
+ HOL-FOL-Fitting \
HOL-FeatherweightJava \
- HOL-Fermat3_4 \
+ HOL-FileRefinement \
+ HOL-FinFun \
+ HOL-Finger-Trees \
HOL-Flyspeck-Tame \
+ HOL-Free-Boolean-Algebra \
HOL-Free-Groups \
+ HOL-FunWithFunctions \
+ HOL-FunWithTilings \
+ HOL-Functional-Automata \
+ HOL-Gauss-Jordan-Elim-Fun \
+ HOL-GenClock \
+ HOL-General-Triangle \
HOL-GraphMarkingIBP \
+ HOL-HotelKeyCards \
+ HOL-Huffman \
+ HOL-Integration \
HOL-JiveDataStoreModel \
+ HOL-KBPs \
+ HOL-Lazy-Lists-II \
+ HOL-LightweightJava \
+ HOL-List-Index \
HOL-Locally-Nameless-Sigma \
+ HOL-Marriage \
+ HOL-Matrix \
+ HOL-Max-Card-Matching \
+ HOL-MiniML \
+ HOL-MuchAdoAboutTwo \
+ HOL-Multivariate_Analysis \
+ HOL-Myhill-Nerode \
+ HOL-Nominal \
+ HOL-Nominal-Lam-ml-Normalization \
+ HOL-Nominal-SequentInvertibility \
+ HOL-Ordinal \
HOL-Ordinals_and_Cardinals \
HOL-POPLmark-deBruijn \
+ HOL-Perfect-Number-Thm \
+ HOL-Polynomials \
HOL-Presburger-Automata \
HOL-Program-Conflict-Analysis \
- HOL-RSAPSS \
+ HOL-Ramsey-Infinite \
HOL-Recursion-Theory-I \
+ HOL-Regular-Sets \
+ HOL-Robbins-Conjecture \
HOL-SATSolverVerification \
HOL-SIFPL \
HOL-SenSocialChoice \
- HOL-SumSquares \
+ HOL-Statecharts \
HOL-Topology \
+ HOL-Transitive-Closure \
HOL-Tree-Automata \
- HOL-Word-JinjaThreads \
+ HOL-Verified-Prover \
+ HOL-Word \
+ HOL-Word-RIPEMD-160-SPARK \
+ HOLCF \
+ HOLCF-Shivers-CFA \
+ HOLCF-Stream-Fusion \
HOLCF-WorkerWrapper \
HRB-Slicing \
+ HRB-Slicing-InformationFlowSlicing \
Jinja \
- Jinja-Slicing \
- LinearQuantifierElim \
+ Jinja \
+ LatticeProperties \
+ LatticeProperties-MonoBoolTranAlgebra \
+ LatticeProperties-PseudoHoops \
+ Lower_Semicontinuous \
+ NormByEval \
Simpl \
Simpl-BDD \
Slicing \
- Slicing-InformationFlowSlicing"
+ Slicing \
+ Slicing-InformationFlowSlicing \
+ VolpanoSmith"
+
for PLATFORM in $PLATFORMS
do