205 |
205 |
206 return (return_code == 0, extract_isabelle_run_summary(log), |
206 return (return_code == 0, extract_isabelle_run_summary(log), |
207 {'timing': extract_isabelle_run_timing(log)}, {'log': log}, None) |
207 {'timing': extract_isabelle_run_timing(log)}, {'log': log}, None) |
208 |
208 |
209 |
209 |
210 # Isabelle configurations |
210 def make_pure(env, case, paths, dep_paths, playground, more_settings=''): |
211 |
|
212 @configuration(repos = [Isabelle], deps = []) |
|
213 def Pure(env, case, paths, dep_paths, playground): |
|
214 """Pure image""" |
|
215 |
211 |
216 isabelle_home = paths[0] |
212 isabelle_home = paths[0] |
217 prepare_isabelle_repository(isabelle_home, env.settings.contrib, '') |
213 prepare_isabelle_repository(isabelle_home, env.settings.contrib, '', |
|
214 more_settings=more_settings) |
218 os.chdir(path.join(isabelle_home, 'src', 'Pure')) |
215 os.chdir(path.join(isabelle_home, 'src', 'Pure')) |
219 |
216 |
220 (return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'make', 'Pure') |
217 (return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'make', 'Pure') |
221 |
218 |
222 result = path.join(isabelle_home, 'heaps') |
219 result = path.join(isabelle_home, 'heaps') |
223 return (return_code == 0, extract_isabelle_run_summary(log), |
220 return (return_code == 0, extract_isabelle_run_summary(log), |
224 {'timing': extract_isabelle_run_timing(log)}, {'log': log}, result) |
221 {'timing': extract_isabelle_run_timing(log)}, {'log': log}, result) |
|
222 |
|
223 |
|
224 # Isabelle configurations |
|
225 |
|
226 @configuration(repos = [Isabelle], deps = []) |
|
227 def Pure(*args): |
|
228 """Pure image""" |
|
229 return make_pure(*args) |
|
230 |
|
231 @configuration(repos = [Isabelle], deps = []) |
|
232 def Pure_64(*args): |
|
233 """Pure image (64 bit)""" |
|
234 return make_pure(*args, more_settings='ML_PLATFORM=x86_64-linux') |
225 |
235 |
226 @configuration(repos = [Isabelle], deps = [(Pure, [0])]) |
236 @configuration(repos = [Isabelle], deps = [(Pure, [0])]) |
227 def HOL(*args): |
237 def HOL(*args): |
228 """HOL image""" |
238 """HOL image""" |
229 return build_isabelle_image('HOL', 'Pure', 'HOL', *args) |
239 return build_isabelle_image('HOL', 'Pure', 'HOL', *args) |
230 |
240 |
231 @configuration(repos = [Isabelle], deps = [(HOL, [0])]) |
241 @configuration(repos = [Isabelle], deps = [(Pure_64, [0])]) |
232 def HOL_HOLCF(*args): |
242 def HOL_64(*args): |
233 """HOL-HOLCF image""" |
243 """HOL image (64 bit)""" |
234 return build_isabelle_image('HOL/HOLCF', 'HOL', 'HOLCF', *args) |
244 return build_isabelle_image('HOL', 'Pure', 'HOL', *args, more_settings='ML_PLATFORM=x86_64-linux') |
235 |
245 |
236 @configuration(repos = [Isabelle], deps = [(HOL, [0])]) |
246 @configuration(repos = [Isabelle], deps = [(HOL_64, [0])]) |
237 def HOL_Nominal(*args): |
247 def HOL_HOLCF_64(*args): |
238 """HOL-Nominal image""" |
248 """HOL-HOLCF image (64 bit)""" |
239 return build_isabelle_image('HOL/Nominal', 'HOL', 'HOL-Nominal', *args) |
249 return build_isabelle_image('HOL/HOLCF', 'HOL', 'HOLCF', *args, more_settings='ML_PLATFORM=x86_64-linux') |
240 |
250 |
241 @configuration(repos = [Isabelle], deps = [(HOL, [0])]) |
251 @configuration(repos = [Isabelle], deps = [(HOL_64, [0])]) |
242 def HOL_Word(*args): |
252 def HOL_Nominal_64(*args): |
243 """HOL-Word image""" |
253 """HOL-Nominal image (64 bit)""" |
244 return build_isabelle_image('HOL/Word', 'HOL', 'HOL-Word', *args) |
254 return build_isabelle_image('HOL/Nominal', 'HOL', 'HOL-Nominal', *args, more_settings='ML_PLATFORM=x86_64-linux') |
|
255 |
|
256 @configuration(repos = [Isabelle], deps = [(HOL_64, [0])]) |
|
257 def HOL_Word_64(*args): |
|
258 """HOL-Word image (64 bit)""" |
|
259 return build_isabelle_image('HOL/Word', 'HOL', 'HOL-Word', *args, more_settings='ML_PLATFORM=x86_64-linux') |
245 |
260 |
246 @configuration(repos = [Isabelle], deps = [ |
261 @configuration(repos = [Isabelle], deps = [ |
247 (HOL, [0]), |
262 (HOL_64, [0]), |
248 (HOL_HOLCF, [0]), |
263 (HOL_HOLCF_64, [0]), |
249 (HOL_Nominal, [0]), |
264 (HOL_Nominal_64, [0]), |
250 (HOL_Word, [0]) |
265 (HOL_Word_64, [0]) |
251 ]) |
266 ]) |
252 def AFP_images(*args): |
267 def AFP_images(*args): |
253 """Isabelle images needed for the AFP""" |
268 """Isabelle images needed for the AFP (64 bit)""" |
254 return isabelle_dependency_only(*args) |
269 return isabelle_dependency_only(*args) |
255 |
270 |
256 @configuration(repos = [Isabelle], deps = []) |
271 @configuration(repos = [Isabelle], deps = []) |
257 def Isabelle_makeall(*args): |
272 def Isabelle_makeall(*args): |
258 """Isabelle makeall""" |
273 """Isabelle makeall""" |