--- a/Admin/mira.py Sun Aug 05 15:11:09 2012 +0200
+++ b/Admin/mira.py Sun Aug 05 22:00:59 2012 +0200
@@ -139,64 +139,27 @@
env.report_db.put(case, (success == 'successful'), content)
-
-def isabelle_usedir(env, isa_path, isabelle_usedir_opts, base_image, dir_name):
-
- return env.run_process('%s/bin/isabelle' % isa_path, 'usedir',
- isabelle_usedir_opts, base_image, dir_name)
-
-
-def isabelle_dependency_only(env, case, paths, dep_paths, playground):
+def isabelle_build(env, case, paths, dep_paths, playground, *cmdargs, **kwargs):
- isabelle_home = paths[0]
- result = path.join(isabelle_home, 'heaps')
- os.makedirs(result)
- for dep_path in dep_paths:
- subprocess.check_call(['cp', '-R'] + glob(dep_path + '/*') + [result])
-
- return (True, 'ok', {}, {}, result)
-
-
-def build_isabelle_image(subdir, base, img, env, case, paths, dep_paths, playground,
- usedir_options=default_usedir_options, more_settings=''):
+ more_settings=kwargs.get('more_settings', '')
isabelle_home = paths[0]
- dep_path = dep_paths[0]
- prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path,
- usedir_options=usedir_options, more_settings=more_settings)
- os.chdir(path.join(isabelle_home, 'src', subdir))
- (return_code, log) = isabelle_usedir(env, isabelle_home, '-b', base, img)
-
- result = path.join(isabelle_home, 'heaps')
-
- return (return_code == 0, extract_isabelle_run_summary(log),
- extract_report_data(isabelle_home, log), {'log': log}, result)
-
-
-def isabelle_make(subdir, env, case, paths, dep_paths, playground, usedir_options=default_usedir_options,
- more_settings='', target='all', keep_results=False):
+ # copy over build results from dependencies
+ heap_dir = path.join(isabelle_home, 'heaps')
+ classes_dir = path.join(heap_dir, 'classes')
+ os.makedirs(classes_dir)
- isabelle_home = paths[0]
- dep_path = dep_paths[0] if dep_paths else None
- prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path,
- usedir_options=usedir_options, more_settings=more_settings)
- os.chdir(path.join(isabelle_home, subdir))
-
- (return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'make', '-k', target)
-
- result = path.join(isabelle_home, 'heaps') if keep_results else None
+ for dep_path in dep_paths:
+ subprocess.check_call(['cp', '-a'] + glob(dep_path + '/*') + [heap_dir])
- return (return_code == 0, extract_isabelle_run_summary(log),
- extract_report_data(isabelle_home, log), {'log': log}, result)
-
+ subprocess.check_call(['ln', '-s', classes_dir, path.join(isabelle_home, 'lib', 'classes')])
+ jars = glob(path.join(classes_dir, 'ext', '*.jar'))
+ if jars:
+ subprocess.check_call(['touch'] + jars)
-def isabelle_makeall(env, case, paths, dep_paths, playground, usedir_options=default_usedir_options,
- more_settings='', target='all', make_options=()):
-
- if 'lxbroy10' in misc.hostnames():
- make_options += ('-j', '8')
- usedir_options += " -M 4 -q 2 -i false -d false"
+ # misc preparations
+ if 'lxbroy10' in misc.hostnames(): # special settings for lxbroy10
more_settings += '''
ML_PLATFORM="x86_64-linux"
ML_HOME="/home/polyml/polyml-5.4.1/x86_64-linux"
@@ -206,58 +169,46 @@
ISABELLE_GHC="/usr/bin/ghc"
'''
- isabelle_home = paths[0]
- dep_path = dep_paths[0] if dep_paths else None
- prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path,
- usedir_options=usedir_options, more_settings=more_settings)
+ prepare_isabelle_repository(isabelle_home, env.settings.contrib, None,
+ usedir_options="", more_settings=more_settings)
os.chdir(isabelle_home)
- (return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'makeall', '-k', *(make_options + (target,)))
-
- return (return_code == 0, extract_isabelle_run_summary(log),
- extract_report_data(isabelle_home, log), {'log': log}, None)
-
-
-def make_pure(env, case, paths, dep_paths, playground, more_settings=''):
+ # invoke build tool
+ (return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'build', '-s', '-v', *cmdargs)
- isabelle_home = paths[0]
- prepare_isabelle_repository(isabelle_home, env.settings.contrib, '',
- more_settings=more_settings)
- os.chdir(path.join(isabelle_home, 'src', 'Pure'))
+ # collect report
+ return (return_code == 0, extract_isabelle_run_summary(log),
+ extract_report_data(isabelle_home, log), {'log': log}, heap_dir)
- (return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'make', 'Pure')
-
- result = path.join(isabelle_home, 'heaps')
- return (return_code == 0, extract_isabelle_run_summary(log),
- {'timing': extract_isabelle_run_timing(log)}, {'log': log}, result)
# Isabelle configurations
@configuration(repos = [Isabelle], deps = [])
def Pure(*args):
- """Pure image"""
- return make_pure(*args)
+ """Pure Image"""
+ return isabelle_build(*(args + ("-b", "Pure")))
@configuration(repos = [Isabelle], deps = [(Pure, [0])])
def HOL(*args):
- """HOL image"""
- return build_isabelle_image('HOL', 'Pure', 'HOL', *args)
+ """HOL Image"""
+ return isabelle_build(*(args + ("-b", "HOL")))
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
def HOL_Library(*args):
- """HOL-Library image"""
- return build_isabelle_image('HOL', 'HOL', 'HOL-Library', *args)
+ """HOL Library"""
+ return isabelle_build(*(args + ("-b", "HOL-Library")))
+
+@configuration(repos = [Isabelle], deps = [(HOL, [0])])
+def HOL_HOLCF(*args):
+ """HOLCF"""
+ return isabelle_build(*(args + ("-b", "HOL-HOLCF")))
@configuration(repos = [Isabelle], deps = [(Pure, [0])])
def ZF(*args):
- """ZF image"""
- return build_isabelle_image('ZF', 'Pure', 'ZF', *args)
+ """HOLCF"""
+ return isabelle_build(*(args + ("-b", "ZF")))
-@configuration(repos = [Isabelle], deps = [(HOL, [0])])
-def HOL_HOLCF(*args):
- """HOLCF image"""
- return build_isabelle_image('HOL/HOLCF', 'HOL', 'HOLCF', *args)
settings64='''
ML_PLATFORM=x86_64-linux
@@ -267,77 +218,33 @@
@configuration(repos = [Isabelle], deps = [])
def Pure_64(*args):
- """Pure image (64 bit)"""
- return make_pure(*args, more_settings=settings64)
+ """Pure Image (64 bit)"""
+ return isabelle_build(*(args + ("-b", "Pure")), more_settings=settings64)
-@configuration(repos = [Isabelle], deps = [(Pure_64, [0])])
+@configuration(repos = [Isabelle], deps = [(Pure, [0])])
def HOL_64(*args):
- """HOL image (64 bit)"""
- return build_isabelle_image('HOL', 'Pure', 'HOL', *args, more_settings=settings64)
-
-@configuration(repos = [Isabelle], deps = [(HOL_64, [0])])
-def HOL_HOLCF_64(*args):
- """HOL-HOLCF image (64 bit)"""
- return build_isabelle_image('HOL/HOLCF', 'HOL', 'HOLCF', *args, more_settings=settings64)
+ """HOL Image (64 bit)"""
+ return isabelle_build(*(args + ("-b", "HOL")), more_settings=settings64)
-@configuration(repos = [Isabelle], deps = [(HOL_64, [0])])
-def HOL_Nominal_64(*args):
- """HOL-Nominal image (64 bit)"""
- return build_isabelle_image('HOL/Nominal', 'HOL', 'HOL-Nominal', *args, more_settings=settings64)
+@configuration(repos = [Isabelle], deps = [(HOL, [0])])
+def HOL_HOLCF_64(*args):
+ """HOLCF Image"""
+ return isabelle_build(*(args + ("-b", "HOL-HOLCF")), more_settings=settings64)
-@configuration(repos = [Isabelle], deps = [(HOL_64, [0])])
+@configuration(repos = [Isabelle], deps = [(HOL, [0])])
def HOL_Word_64(*args):
- """HOL-Word image (64 bit)"""
- return build_isabelle_image('HOL/Word', 'HOL', 'HOL-Word', *args, more_settings=settings64)
+ """HOL-Word Image"""
+ return isabelle_build(*(args + ("-b", "HOL-Word")), more_settings=settings64)
-@configuration(repos = [Isabelle], deps = [
- (HOL_64, [0]),
- (HOL_HOLCF_64, [0]),
- (HOL_Nominal_64, [0]),
- (HOL_Word_64, [0])
- ])
+@configuration(repos = [Isabelle], deps = [])
def AFP_images(*args):
"""Isabelle images needed for the AFP (64 bit)"""
- return isabelle_dependency_only(*args)
+ return isabelle_build(*(args + ("-b", "-j", "2", "Pure", "HOL", "HOL-HOLCF", "HOL-Word")), more_settings=settings64)
@configuration(repos = [Isabelle], deps = [])
def Isabelle_makeall(*args):
- """Isabelle makeall"""
- return isabelle_makeall(*args)
-
-
-# distribution and documentation Build
-
-@configuration(repos = [Isabelle], deps = [])
-def Distribution(env, case, paths, dep_paths, playground):
- """Build of distribution"""
- ## FIXME This is rudimentary; study Admin/CHECKLIST to complete this configuration accordingly
- isabelle_home = paths[0]
- (return_code, log) = env.run_process(path.join(isabelle_home, 'Admin', 'Release', 'makedist'),
- REPOS = repositories.get(Isabelle).local_path, DISTPREFIX = os.getcwd())
- return (return_code == 0, '', ## FIXME might add summary here
- {}, {'log': log}, None) ## FIXME might add proper result here
-
-@configuration(repos = [Isabelle], deps = [
- (HOL, [0]),
- (HOL_HOLCF, [0]),
- (ZF, [0]),
- (HOL_Library, [0])
- ])
-def Documentation_images(*args):
- """Isabelle images needed to build the documentation"""
- return isabelle_dependency_only(*args)
-
-@configuration(repos = [Isabelle], deps = [(Documentation_images, [0])])
-def Documentation(env, case, paths, dep_paths, playground):
- """Build of documentation"""
- isabelle_home = paths[0]
- dep_path = dep_paths[0]
- prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path,
- usedir_options = default_usedir_options)
- (return_code, log) = env.run_process(path.join(isabelle_home, 'Admin', 'build', 'doc-src'))
- return (return_code == 0, extract_isabelle_run_summary(log),
- extract_report_data(isabelle_home, log), {'log': log}, None)
+ """Build all sessions"""
+ return isabelle_build(*(args + ("-j", "6", "-o", "threads=4", "-a")), more_settings=settings64)
# Mutabelle configurations
@@ -497,13 +404,62 @@
ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
'''
-@configuration(repos = [Isabelle], deps = [])
+@configuration(repos = [Isabelle], deps = [(Pure, [0])])
def SML_HOL(*args):
"""HOL image built with SML/NJ"""
- return isabelle_make('src/HOL', *args, more_settings=smlnj_settings, target='HOL', keep_results=True)
+ return isabelle_build(*(args + ("-b", "HOL")), more_settings=smlnj_settings)
@configuration(repos = [Isabelle], deps = [])
def SML_makeall(*args):
- """Makeall built with SML/NJ"""
- return isabelle_makeall(*args, more_settings=smlnj_settings, target='smlnj', make_options=('-j', '3'))
+ """SML/NJ build of all possible sessions"""
+ return isabelle_build(*(args + ("-j", "3", "-a")), more_settings=smlnj_settings)
+
+
+# Legacy Isabelle configurations
+
+# distribution and documentation Build
+
+@configuration(repos = [Isabelle], deps = [])
+def Distribution(env, case, paths, dep_paths, playground):
+ """Build of distribution"""
+ ## FIXME This is rudimentary; study Admin/CHECKLIST to complete this configuration accordingly
+ isabelle_home = paths[0]
+ (return_code, log) = env.run_process(path.join(isabelle_home, 'Admin', 'Release', 'makedist'),
+ REPOS = repositories.get(Isabelle).local_path, DISTPREFIX = os.getcwd())
+ return (return_code == 0, '', ## FIXME might add summary here
+ {}, {'log': log}, None) ## FIXME might add proper result here
+
+
+def isabelle_dependency_only(env, case, paths, dep_paths, playground):
+ isabelle_home = paths[0]
+ result = path.join(isabelle_home, 'heaps')
+ os.makedirs(result)
+ for dep_path in dep_paths:
+ subprocess.check_call(['cp', '-R'] + glob(dep_path + '/*') + [result])
+
+ return (True, 'ok', {}, {}, result)
+
+
+@configuration(repos = [Isabelle], deps = [
+ (HOL, [0]),
+ (HOL_HOLCF, [0]),
+ (ZF, [0]),
+ (HOL_Library, [0])
+ ])
+def Documentation_images(*args):
+ """Isabelle images needed to build the documentation"""
+ return isabelle_dependency_only(*args)
+
+@configuration(repos = [Isabelle], deps = [(Documentation_images, [0])])
+def Documentation(env, case, paths, dep_paths, playground):
+ """Build of documentation"""
+ isabelle_home = paths[0]
+ dep_path = dep_paths[0]
+ prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path,
+ usedir_options = default_usedir_options)
+ (return_code, log) = env.run_process(path.join(isabelle_home, 'Admin', 'build', 'doc-src'))
+ return (return_code == 0, extract_isabelle_run_summary(log),
+ extract_report_data(isabelle_home, log), {'log': log}, None)
+
+