4 # |
4 # |
5 # DESCRIPTION: Standard statistics. |
5 # DESCRIPTION: Standard statistics. |
6 |
6 |
7 THIS=$(cd "$(dirname "$0")"; pwd -P) |
7 THIS=$(cd "$(dirname "$0")"; pwd -P) |
8 |
8 |
9 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" |
9 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" |
10 |
10 |
11 ISABELLE_SESSIONS="\ |
11 ISABELLE_SESSIONS="\ |
12 HOL-Plain \ |
12 HOL-Plain \ |
13 HOL-Main \ |
13 HOL-Main \ |
14 HOL \ |
14 HOL \ |
15 HOL-Proofs \ |
15 HOL-Proofs \ |
|
16 HOL-Library \ |
16 HOL-Algebra \ |
17 HOL-Algebra \ |
17 HOL-Auth \ |
18 HOL-Auth \ |
18 HOL-Bali \ |
19 HOL-Bali \ |
19 HOL-Decision_Procs \ |
20 HOL-Decision_Procs \ |
20 HOL-Hoare \ |
21 HOL-Hoare \ |
21 HOL-Hoare_Parallel \ |
22 HOL-Hoare_Parallel \ |
22 HOL-Library \ |
23 HOL-Imperative_HOL \ |
23 HOL-Metis_Examples \ |
24 HOL-Metis_Examples \ |
24 HOL-MicroJava \ |
25 HOL-MicroJava \ |
25 HOL-Multivariate_Analysis \ |
26 HOL-Multivariate_Analysis \ |
26 HOL-NSA \ |
27 HOL-NSA \ |
27 HOL-Nominal-Examples \ |
28 HOL-Nominal-Examples \ |
28 HOL-Number_Theory \ |
29 HOL-Number_Theory \ |
29 HOL-Old_Number_Theory \ |
30 HOL-Old_Number_Theory \ |
|
31 HOL-Predicate_Compile_Examples \ |
30 HOL-Proofs-Extraction \ |
32 HOL-Proofs-Extraction \ |
31 HOL-Proofs-Lambda \ |
33 HOL-Proofs-Lambda \ |
32 HOL-SET_Protocol \ |
34 HOL-SET_Protocol \ |
33 HOL-UNITY \ |
35 HOL-UNITY \ |
34 HOL-Word \ |
36 HOL-Word \ |
|
37 HOL-Word-SMT_Examples \ |
35 HOL-ex \ |
38 HOL-ex \ |
36 HOLCF \ |
39 HOLCF \ |
37 IOA \ |
40 IOA \ |
38 ZF \ |
41 ZF \ |
39 ZF-Constructible \ |
42 ZF-Constructible \ |
40 ZF-UNITY" |
43 ZF-UNITY" |
41 |
44 |
42 AFP_SESSIONS="\ |
45 AFP_SESSIONS="\ |
|
46 Coinductive \ |
43 CoreC++ \ |
47 CoreC++ \ |
44 Jinja-Slicing \ |
48 Group-Ring-Module \ |
|
49 Group-Ring-Module-Valuation \ |
45 HOL-BytecodeLogicJmlTypes \ |
50 HOL-BytecodeLogicJmlTypes \ |
|
51 HOL-Collections \ |
46 HOL-DiskPaxos \ |
52 HOL-DiskPaxos \ |
|
53 HOL-FeatherweightJava \ |
47 HOL-Fermat3_4 \ |
54 HOL-Fermat3_4 \ |
48 HOL-Flyspeck-Tame \ |
55 HOL-Flyspeck-Tame \ |
49 HOL-Group-Ring-Module \ |
56 HOL-Free-Groups \ |
50 HOL-Jinja \ |
57 HOL-GraphMarkingIBP \ |
51 HOL-JinjaThreads \ |
|
52 HOL-JiveDataStoreModel \ |
58 HOL-JiveDataStoreModel \ |
|
59 HOL-Locally-Nameless-Sigma \ |
|
60 HOL-Ordinals_and_Cardinals \ |
53 HOL-POPLmark-deBruijn \ |
61 HOL-POPLmark-deBruijn \ |
|
62 HOL-Presburger-Automata \ |
54 HOL-Program-Conflict-Analysis \ |
63 HOL-Program-Conflict-Analysis \ |
55 HOL-RSAPSS \ |
64 HOL-RSAPSS \ |
56 HOL-Recursion-Theory-I \ |
65 HOL-Recursion-Theory-I \ |
57 HOL-SATSolverVerification \ |
66 HOL-SATSolverVerification \ |
58 HOL-SIFPL \ |
67 HOL-SIFPL \ |
59 HOL-SenSocialChoice \ |
68 HOL-SenSocialChoice \ |
60 HOL-SumSquares \ |
69 HOL-SumSquares \ |
61 HOL-Topology \ |
70 HOL-Topology \ |
62 HOL-Valuation \ |
71 HOL-Tree-Automata \ |
|
72 HOL-Word-JinjaThreads \ |
|
73 HOLCF-WorkerWrapper \ |
|
74 HRB-Slicing \ |
|
75 Jinja \ |
|
76 Jinja-Slicing \ |
63 LinearQuantifierElim \ |
77 LinearQuantifierElim \ |
64 Simpl \ |
78 Simpl \ |
65 Simpl-BDD" |
79 Simpl-BDD \ |
|
80 Slicing \ |
|
81 Slicing-InformationFlowSlicing" |
66 |
82 |
67 for PLATFORM in $PLATFORMS |
83 for PLATFORM in $PLATFORMS |
68 do |
84 do |
69 if [ "$PLATFORM" = afp ]; then |
85 if [ "$PLATFORM" = afp ]; then |
70 SESSIONS="$AFP_SESSIONS" |
86 SESSIONS="$AFP_SESSIONS" |