64bit versions of some mira configurations
authorkrauss
Wed, 06 Jul 2011 17:58:03 +0200
changeset 44555b8d79bd6029e
parent 44554 08ccba00eb34
child 44556 92f78a4a5628
64bit versions of some mira configurations
Admin/mira.py
     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 = [])