7 THIS="$(cd "$(dirname "$0")"; pwd)" |
7 THIS="$(cd "$(dirname "$0")"; pwd)" |
8 |
8 |
9 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" |
9 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" |
10 |
10 |
11 ISABELLE_SESSIONS="\ |
11 ISABELLE_SESSIONS="\ |
12 HOL-Plain \ |
|
13 HOL-Main \ |
|
14 HOL \ |
|
15 HOL-Proofs \ |
|
16 HOL-Library \ |
|
17 HOL-Algebra \ |
|
18 HOL-Auth \ |
12 HOL-Auth \ |
19 HOL-Bali \ |
13 HOL-Bali \ |
|
14 HOL-Boogie-Examples \ |
20 HOL-Decision_Procs \ |
15 HOL-Decision_Procs \ |
|
16 HOL-Hahn_Banach \ |
21 HOL-Hoare \ |
17 HOL-Hoare \ |
22 HOL-Hoare_Parallel \ |
18 HOL-Hoare_Parallel \ |
|
19 HOL-IMPP \ |
|
20 HOL-IOA \ |
23 HOL-Imperative_HOL \ |
21 HOL-Imperative_HOL \ |
|
22 HOL-Import \ |
|
23 HOL-Induct \ |
|
24 HOL-Isar_Examples \ |
|
25 HOL-Lattice \ |
|
26 HOL-Library-Codegenerator_Test \ |
|
27 HOL-Matrix \ |
24 HOL-Metis_Examples \ |
28 HOL-Metis_Examples \ |
25 HOL-MicroJava \ |
29 HOL-MicroJava \ |
26 HOL-Multivariate_Analysis \ |
30 HOL-Mirabelle \ |
27 HOL-NSA \ |
31 HOL-Mutabelle \ |
28 HOL-Nominal-Examples \ |
32 HOL-NanoJava \ |
|
33 HOL-Nitpick_Examples \ |
|
34 HOL-Nominal-Examples |
29 HOL-Number_Theory \ |
35 HOL-Number_Theory \ |
30 HOL-Old_Number_Theory \ |
36 HOL-Old_Number_Theory \ |
31 HOL-Predicate_Compile_Examples \ |
37 HOL-Predicate_Compile_Examples \ |
|
38 HOL-Probability |
|
39 HOL-Prolog \ |
32 HOL-Proofs-Extraction \ |
40 HOL-Proofs-Extraction \ |
33 HOL-Proofs-Lambda \ |
41 HOL-Proofs-Lambda \ |
|
42 HOL-Proofs-ex \ |
|
43 HOL-Quotient_Examples \ |
34 HOL-SET_Protocol \ |
44 HOL-SET_Protocol \ |
|
45 HOL-SPARK-Examples \ |
|
46 HOL-SPARK-Manual \ |
|
47 HOL-Statespace \ |
|
48 HOL-TPTP \ |
35 HOL-UNITY \ |
49 HOL-UNITY \ |
36 HOL-Word \ |
50 HOL-Unix \ |
|
51 HOL-Word-Examples \ |
37 HOL-Word-SMT_Examples \ |
52 HOL-Word-SMT_Examples \ |
|
53 HOL-ZF |
38 HOL-ex \ |
54 HOL-ex \ |
39 HOLCF \ |
55 HOLCF-FOCUS \ |
40 IOA \ |
56 HOLCF-IMP \ |
41 ZF \ |
57 HOLCF-Library \ |
42 ZF-Constructible \ |
58 HOLCF-Tutorial \ |
43 ZF-UNITY" |
59 HOLCF-ex \ |
|
60 IOA-ABP \ |
|
61 IOA-NTP \ |
|
62 IOA-Storage \ |
|
63 IOA-ex \ |
|
64 TLA-Buffer \ |
|
65 TLA-Inc \ |
|
66 TLA-Memory" |
44 |
67 |
45 AFP_SESSIONS="\ |
68 AFP_SESSIONS="\ |
|
69 ArrowImpossibilityGS \ |
46 Coinductive \ |
70 Coinductive \ |
47 CoreC++ \ |
71 CoreC++ \ |
48 Group-Ring-Module \ |
72 HOL-AVL-Trees \ |
49 Group-Ring-Module-Valuation \ |
73 HOL-Abstract-Hoare-Logics \ |
|
74 HOL-Abstract-Rewriting \ |
|
75 HOL-BinarySearchTree \ |
|
76 HOL-Binomial-Heaps \ |
|
77 HOL-Binomial-Queues \ |
50 HOL-BytecodeLogicJmlTypes \ |
78 HOL-BytecodeLogicJmlTypes \ |
|
79 HOL-Category \ |
|
80 HOL-Category2 \ |
|
81 HOL-Cauchy \ |
|
82 HOL-ClockSynchInst \ |
|
83 HOL-CofGroups \ |
51 HOL-Collections \ |
84 HOL-Collections \ |
|
85 HOL-Compiling-Exceptions-Correctly \ |
|
86 HOL-Completeness \ |
|
87 HOL-DPT-SAT-Solver \ |
|
88 HOL-DataRefinementIBP \ |
|
89 HOL-Depth-First-Search \ |
52 HOL-DiskPaxos \ |
90 HOL-DiskPaxos \ |
|
91 HOL-Example-Submission \ |
|
92 HOL-FFT \ |
|
93 HOL-FOL-Fitting \ |
53 HOL-FeatherweightJava \ |
94 HOL-FeatherweightJava \ |
54 HOL-Fermat3_4 \ |
95 HOL-FileRefinement \ |
|
96 HOL-FinFun \ |
|
97 HOL-Finger-Trees \ |
55 HOL-Flyspeck-Tame \ |
98 HOL-Flyspeck-Tame \ |
|
99 HOL-Free-Boolean-Algebra \ |
56 HOL-Free-Groups \ |
100 HOL-Free-Groups \ |
|
101 HOL-FunWithFunctions \ |
|
102 HOL-FunWithTilings \ |
|
103 HOL-Functional-Automata \ |
|
104 HOL-Gauss-Jordan-Elim-Fun \ |
|
105 HOL-GenClock \ |
|
106 HOL-General-Triangle \ |
57 HOL-GraphMarkingIBP \ |
107 HOL-GraphMarkingIBP \ |
|
108 HOL-HotelKeyCards \ |
|
109 HOL-Huffman \ |
|
110 HOL-Integration \ |
58 HOL-JiveDataStoreModel \ |
111 HOL-JiveDataStoreModel \ |
|
112 HOL-KBPs \ |
|
113 HOL-Lazy-Lists-II \ |
|
114 HOL-LightweightJava \ |
|
115 HOL-List-Index \ |
59 HOL-Locally-Nameless-Sigma \ |
116 HOL-Locally-Nameless-Sigma \ |
|
117 HOL-Marriage \ |
|
118 HOL-Matrix \ |
|
119 HOL-Max-Card-Matching \ |
|
120 HOL-MiniML \ |
|
121 HOL-MuchAdoAboutTwo \ |
|
122 HOL-Multivariate_Analysis \ |
|
123 HOL-Myhill-Nerode \ |
|
124 HOL-Nominal \ |
|
125 HOL-Nominal-Lam-ml-Normalization \ |
|
126 HOL-Nominal-SequentInvertibility \ |
|
127 HOL-Ordinal \ |
60 HOL-Ordinals_and_Cardinals \ |
128 HOL-Ordinals_and_Cardinals \ |
61 HOL-POPLmark-deBruijn \ |
129 HOL-POPLmark-deBruijn \ |
|
130 HOL-Perfect-Number-Thm \ |
|
131 HOL-Polynomials \ |
62 HOL-Presburger-Automata \ |
132 HOL-Presburger-Automata \ |
63 HOL-Program-Conflict-Analysis \ |
133 HOL-Program-Conflict-Analysis \ |
64 HOL-RSAPSS \ |
134 HOL-Ramsey-Infinite \ |
65 HOL-Recursion-Theory-I \ |
135 HOL-Recursion-Theory-I \ |
|
136 HOL-Regular-Sets \ |
|
137 HOL-Robbins-Conjecture \ |
66 HOL-SATSolverVerification \ |
138 HOL-SATSolverVerification \ |
67 HOL-SIFPL \ |
139 HOL-SIFPL \ |
68 HOL-SenSocialChoice \ |
140 HOL-SenSocialChoice \ |
69 HOL-SumSquares \ |
141 HOL-Statecharts \ |
70 HOL-Topology \ |
142 HOL-Topology \ |
|
143 HOL-Transitive-Closure \ |
71 HOL-Tree-Automata \ |
144 HOL-Tree-Automata \ |
72 HOL-Word-JinjaThreads \ |
145 HOL-Verified-Prover \ |
|
146 HOL-Word \ |
|
147 HOL-Word-RIPEMD-160-SPARK \ |
|
148 HOLCF \ |
|
149 HOLCF-Shivers-CFA \ |
|
150 HOLCF-Stream-Fusion \ |
73 HOLCF-WorkerWrapper \ |
151 HOLCF-WorkerWrapper \ |
74 HRB-Slicing \ |
152 HRB-Slicing \ |
|
153 HRB-Slicing-InformationFlowSlicing \ |
75 Jinja \ |
154 Jinja \ |
76 Jinja-Slicing \ |
155 Jinja \ |
77 LinearQuantifierElim \ |
156 LatticeProperties \ |
|
157 LatticeProperties-MonoBoolTranAlgebra \ |
|
158 LatticeProperties-PseudoHoops \ |
|
159 Lower_Semicontinuous \ |
|
160 NormByEval \ |
78 Simpl \ |
161 Simpl \ |
79 Simpl-BDD \ |
162 Simpl-BDD \ |
80 Slicing \ |
163 Slicing \ |
81 Slicing-InformationFlowSlicing" |
164 Slicing \ |
|
165 Slicing-InformationFlowSlicing \ |
|
166 VolpanoSmith" |
|
167 |
82 |
168 |
83 for PLATFORM in $PLATFORMS |
169 for PLATFORM in $PLATFORMS |
84 do |
170 do |
85 if [ "$PLATFORM" = afp ]; then |
171 if [ "$PLATFORM" = afp ]; then |
86 SESSIONS="$AFP_SESSIONS" |
172 SESSIONS="$AFP_SESSIONS" |