1.1 --- a/Admin/mira.py Wed Jul 06 17:56:58 2011 +0200
1.2 +++ b/Admin/mira.py Wed Jul 06 17:58:03 2011 +0200
1.3 @@ -207,14 +207,11 @@
1.4 {'timing': extract_isabelle_run_timing(log)}, {'log': log}, None)
1.5
1.6
1.7 -# Isabelle configurations
1.8 -
1.9 -@configuration(repos = [Isabelle], deps = [])
1.10 -def Pure(env, case, paths, dep_paths, playground):
1.11 - """Pure image"""
1.12 +def make_pure(env, case, paths, dep_paths, playground, more_settings=''):
1.13
1.14 isabelle_home = paths[0]
1.15 - prepare_isabelle_repository(isabelle_home, env.settings.contrib, '')
1.16 + prepare_isabelle_repository(isabelle_home, env.settings.contrib, '',
1.17 + more_settings=more_settings)
1.18 os.chdir(path.join(isabelle_home, 'src', 'Pure'))
1.19
1.20 (return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'make', 'Pure')
1.21 @@ -223,34 +220,52 @@
1.22 return (return_code == 0, extract_isabelle_run_summary(log),
1.23 {'timing': extract_isabelle_run_timing(log)}, {'log': log}, result)
1.24
1.25 +
1.26 +# Isabelle configurations
1.27 +
1.28 +@configuration(repos = [Isabelle], deps = [])
1.29 +def Pure(*args):
1.30 + """Pure image"""
1.31 + return make_pure(*args)
1.32 +
1.33 +@configuration(repos = [Isabelle], deps = [])
1.34 +def Pure_64(*args):
1.35 + """Pure image (64 bit)"""
1.36 + return make_pure(*args, more_settings='ML_PLATFORM=x86_64-linux')
1.37 +
1.38 @configuration(repos = [Isabelle], deps = [(Pure, [0])])
1.39 def HOL(*args):
1.40 """HOL image"""
1.41 return build_isabelle_image('HOL', 'Pure', 'HOL', *args)
1.42
1.43 -@configuration(repos = [Isabelle], deps = [(HOL, [0])])
1.44 -def HOL_HOLCF(*args):
1.45 - """HOL-HOLCF image"""
1.46 - return build_isabelle_image('HOL/HOLCF', 'HOL', 'HOLCF', *args)
1.47 +@configuration(repos = [Isabelle], deps = [(Pure_64, [0])])
1.48 +def HOL_64(*args):
1.49 + """HOL image (64 bit)"""
1.50 + return build_isabelle_image('HOL', 'Pure', 'HOL', *args, more_settings='ML_PLATFORM=x86_64-linux')
1.51
1.52 -@configuration(repos = [Isabelle], deps = [(HOL, [0])])
1.53 -def HOL_Nominal(*args):
1.54 - """HOL-Nominal image"""
1.55 - return build_isabelle_image('HOL/Nominal', 'HOL', 'HOL-Nominal', *args)
1.56 +@configuration(repos = [Isabelle], deps = [(HOL_64, [0])])
1.57 +def HOL_HOLCF_64(*args):
1.58 + """HOL-HOLCF image (64 bit)"""
1.59 + return build_isabelle_image('HOL/HOLCF', 'HOL', 'HOLCF', *args, more_settings='ML_PLATFORM=x86_64-linux')
1.60
1.61 -@configuration(repos = [Isabelle], deps = [(HOL, [0])])
1.62 -def HOL_Word(*args):
1.63 - """HOL-Word image"""
1.64 - return build_isabelle_image('HOL/Word', 'HOL', 'HOL-Word', *args)
1.65 +@configuration(repos = [Isabelle], deps = [(HOL_64, [0])])
1.66 +def HOL_Nominal_64(*args):
1.67 + """HOL-Nominal image (64 bit)"""
1.68 + return build_isabelle_image('HOL/Nominal', 'HOL', 'HOL-Nominal', *args, more_settings='ML_PLATFORM=x86_64-linux')
1.69 +
1.70 +@configuration(repos = [Isabelle], deps = [(HOL_64, [0])])
1.71 +def HOL_Word_64(*args):
1.72 + """HOL-Word image (64 bit)"""
1.73 + return build_isabelle_image('HOL/Word', 'HOL', 'HOL-Word', *args, more_settings='ML_PLATFORM=x86_64-linux')
1.74
1.75 @configuration(repos = [Isabelle], deps = [
1.76 - (HOL, [0]),
1.77 - (HOL_HOLCF, [0]),
1.78 - (HOL_Nominal, [0]),
1.79 - (HOL_Word, [0])
1.80 + (HOL_64, [0]),
1.81 + (HOL_HOLCF_64, [0]),
1.82 + (HOL_Nominal_64, [0]),
1.83 + (HOL_Word_64, [0])
1.84 ])
1.85 def AFP_images(*args):
1.86 - """Isabelle images needed for the AFP"""
1.87 + """Isabelle images needed for the AFP (64 bit)"""
1.88 return isabelle_dependency_only(*args)
1.89
1.90 @configuration(repos = [Isabelle], deps = [])