1.1 --- a/Admin/mira.py Sun Aug 05 15:11:09 2012 +0200
1.2 +++ b/Admin/mira.py Sun Aug 05 22:00:59 2012 +0200
1.3 @@ -139,64 +139,27 @@
1.4 env.report_db.put(case, (success == 'successful'), content)
1.5
1.6
1.7 +def isabelle_build(env, case, paths, dep_paths, playground, *cmdargs, **kwargs):
1.8
1.9 -def isabelle_usedir(env, isa_path, isabelle_usedir_opts, base_image, dir_name):
1.10 -
1.11 - return env.run_process('%s/bin/isabelle' % isa_path, 'usedir',
1.12 - isabelle_usedir_opts, base_image, dir_name)
1.13 -
1.14 -
1.15 -def isabelle_dependency_only(env, case, paths, dep_paths, playground):
1.16 + more_settings=kwargs.get('more_settings', '')
1.17
1.18 isabelle_home = paths[0]
1.19 - result = path.join(isabelle_home, 'heaps')
1.20 - os.makedirs(result)
1.21 +
1.22 + # copy over build results from dependencies
1.23 + heap_dir = path.join(isabelle_home, 'heaps')
1.24 + classes_dir = path.join(heap_dir, 'classes')
1.25 + os.makedirs(classes_dir)
1.26 +
1.27 for dep_path in dep_paths:
1.28 - subprocess.check_call(['cp', '-R'] + glob(dep_path + '/*') + [result])
1.29 + subprocess.check_call(['cp', '-a'] + glob(dep_path + '/*') + [heap_dir])
1.30
1.31 - return (True, 'ok', {}, {}, result)
1.32 + subprocess.check_call(['ln', '-s', classes_dir, path.join(isabelle_home, 'lib', 'classes')])
1.33 + jars = glob(path.join(classes_dir, 'ext', '*.jar'))
1.34 + if jars:
1.35 + subprocess.check_call(['touch'] + jars)
1.36
1.37 -
1.38 -def build_isabelle_image(subdir, base, img, env, case, paths, dep_paths, playground,
1.39 - usedir_options=default_usedir_options, more_settings=''):
1.40 -
1.41 - isabelle_home = paths[0]
1.42 - dep_path = dep_paths[0]
1.43 - prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path,
1.44 - usedir_options=usedir_options, more_settings=more_settings)
1.45 - os.chdir(path.join(isabelle_home, 'src', subdir))
1.46 -
1.47 - (return_code, log) = isabelle_usedir(env, isabelle_home, '-b', base, img)
1.48 -
1.49 - result = path.join(isabelle_home, 'heaps')
1.50 -
1.51 - return (return_code == 0, extract_isabelle_run_summary(log),
1.52 - extract_report_data(isabelle_home, log), {'log': log}, result)
1.53 -
1.54 -
1.55 -def isabelle_make(subdir, env, case, paths, dep_paths, playground, usedir_options=default_usedir_options,
1.56 - more_settings='', target='all', keep_results=False):
1.57 -
1.58 - isabelle_home = paths[0]
1.59 - dep_path = dep_paths[0] if dep_paths else None
1.60 - prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path,
1.61 - usedir_options=usedir_options, more_settings=more_settings)
1.62 - os.chdir(path.join(isabelle_home, subdir))
1.63 -
1.64 - (return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'make', '-k', target)
1.65 -
1.66 - result = path.join(isabelle_home, 'heaps') if keep_results else None
1.67 -
1.68 - return (return_code == 0, extract_isabelle_run_summary(log),
1.69 - extract_report_data(isabelle_home, log), {'log': log}, result)
1.70 -
1.71 -
1.72 -def isabelle_makeall(env, case, paths, dep_paths, playground, usedir_options=default_usedir_options,
1.73 - more_settings='', target='all', make_options=()):
1.74 -
1.75 - if 'lxbroy10' in misc.hostnames():
1.76 - make_options += ('-j', '8')
1.77 - usedir_options += " -M 4 -q 2 -i false -d false"
1.78 + # misc preparations
1.79 + if 'lxbroy10' in misc.hostnames(): # special settings for lxbroy10
1.80 more_settings += '''
1.81 ML_PLATFORM="x86_64-linux"
1.82 ML_HOME="/home/polyml/polyml-5.4.1/x86_64-linux"
1.83 @@ -206,58 +169,46 @@
1.84 ISABELLE_GHC="/usr/bin/ghc"
1.85 '''
1.86
1.87 - isabelle_home = paths[0]
1.88 - dep_path = dep_paths[0] if dep_paths else None
1.89 - prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path,
1.90 - usedir_options=usedir_options, more_settings=more_settings)
1.91 + prepare_isabelle_repository(isabelle_home, env.settings.contrib, None,
1.92 + usedir_options="", more_settings=more_settings)
1.93 os.chdir(isabelle_home)
1.94
1.95 - (return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'makeall', '-k', *(make_options + (target,)))
1.96 + # invoke build tool
1.97 + (return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'build', '-s', '-v', *cmdargs)
1.98
1.99 + # collect report
1.100 return (return_code == 0, extract_isabelle_run_summary(log),
1.101 - extract_report_data(isabelle_home, log), {'log': log}, None)
1.102 + extract_report_data(isabelle_home, log), {'log': log}, heap_dir)
1.103
1.104
1.105 -def make_pure(env, case, paths, dep_paths, playground, more_settings=''):
1.106 -
1.107 - isabelle_home = paths[0]
1.108 - prepare_isabelle_repository(isabelle_home, env.settings.contrib, '',
1.109 - more_settings=more_settings)
1.110 - os.chdir(path.join(isabelle_home, 'src', 'Pure'))
1.111 -
1.112 - (return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'make', 'Pure')
1.113 -
1.114 - result = path.join(isabelle_home, 'heaps')
1.115 - return (return_code == 0, extract_isabelle_run_summary(log),
1.116 - {'timing': extract_isabelle_run_timing(log)}, {'log': log}, result)
1.117 -
1.118
1.119 # Isabelle configurations
1.120
1.121 @configuration(repos = [Isabelle], deps = [])
1.122 def Pure(*args):
1.123 - """Pure image"""
1.124 - return make_pure(*args)
1.125 + """Pure Image"""
1.126 + return isabelle_build(*(args + ("-b", "Pure")))
1.127
1.128 @configuration(repos = [Isabelle], deps = [(Pure, [0])])
1.129 def HOL(*args):
1.130 - """HOL image"""
1.131 - return build_isabelle_image('HOL', 'Pure', 'HOL', *args)
1.132 + """HOL Image"""
1.133 + return isabelle_build(*(args + ("-b", "HOL")))
1.134
1.135 @configuration(repos = [Isabelle], deps = [(HOL, [0])])
1.136 def HOL_Library(*args):
1.137 - """HOL-Library image"""
1.138 - return build_isabelle_image('HOL', 'HOL', 'HOL-Library', *args)
1.139 + """HOL Library"""
1.140 + return isabelle_build(*(args + ("-b", "HOL-Library")))
1.141 +
1.142 +@configuration(repos = [Isabelle], deps = [(HOL, [0])])
1.143 +def HOL_HOLCF(*args):
1.144 + """HOLCF"""
1.145 + return isabelle_build(*(args + ("-b", "HOL-HOLCF")))
1.146
1.147 @configuration(repos = [Isabelle], deps = [(Pure, [0])])
1.148 def ZF(*args):
1.149 - """ZF image"""
1.150 - return build_isabelle_image('ZF', 'Pure', 'ZF', *args)
1.151 + """HOLCF"""
1.152 + return isabelle_build(*(args + ("-b", "ZF")))
1.153
1.154 -@configuration(repos = [Isabelle], deps = [(HOL, [0])])
1.155 -def HOL_HOLCF(*args):
1.156 - """HOLCF image"""
1.157 - return build_isabelle_image('HOL/HOLCF', 'HOL', 'HOLCF', *args)
1.158
1.159 settings64='''
1.160 ML_PLATFORM=x86_64-linux
1.161 @@ -267,77 +218,33 @@
1.162
1.163 @configuration(repos = [Isabelle], deps = [])
1.164 def Pure_64(*args):
1.165 - """Pure image (64 bit)"""
1.166 - return make_pure(*args, more_settings=settings64)
1.167 + """Pure Image (64 bit)"""
1.168 + return isabelle_build(*(args + ("-b", "Pure")), more_settings=settings64)
1.169
1.170 -@configuration(repos = [Isabelle], deps = [(Pure_64, [0])])
1.171 +@configuration(repos = [Isabelle], deps = [(Pure, [0])])
1.172 def HOL_64(*args):
1.173 - """HOL image (64 bit)"""
1.174 - return build_isabelle_image('HOL', 'Pure', 'HOL', *args, more_settings=settings64)
1.175 + """HOL Image (64 bit)"""
1.176 + return isabelle_build(*(args + ("-b", "HOL")), more_settings=settings64)
1.177
1.178 -@configuration(repos = [Isabelle], deps = [(HOL_64, [0])])
1.179 +@configuration(repos = [Isabelle], deps = [(HOL, [0])])
1.180 def HOL_HOLCF_64(*args):
1.181 - """HOL-HOLCF image (64 bit)"""
1.182 - return build_isabelle_image('HOL/HOLCF', 'HOL', 'HOLCF', *args, more_settings=settings64)
1.183 + """HOLCF Image"""
1.184 + return isabelle_build(*(args + ("-b", "HOL-HOLCF")), more_settings=settings64)
1.185
1.186 -@configuration(repos = [Isabelle], deps = [(HOL_64, [0])])
1.187 -def HOL_Nominal_64(*args):
1.188 - """HOL-Nominal image (64 bit)"""
1.189 - return build_isabelle_image('HOL/Nominal', 'HOL', 'HOL-Nominal', *args, more_settings=settings64)
1.190 +@configuration(repos = [Isabelle], deps = [(HOL, [0])])
1.191 +def HOL_Word_64(*args):
1.192 + """HOL-Word Image"""
1.193 + return isabelle_build(*(args + ("-b", "HOL-Word")), more_settings=settings64)
1.194
1.195 -@configuration(repos = [Isabelle], deps = [(HOL_64, [0])])
1.196 -def HOL_Word_64(*args):
1.197 - """HOL-Word image (64 bit)"""
1.198 - return build_isabelle_image('HOL/Word', 'HOL', 'HOL-Word', *args, more_settings=settings64)
1.199 -
1.200 -@configuration(repos = [Isabelle], deps = [
1.201 - (HOL_64, [0]),
1.202 - (HOL_HOLCF_64, [0]),
1.203 - (HOL_Nominal_64, [0]),
1.204 - (HOL_Word_64, [0])
1.205 - ])
1.206 +@configuration(repos = [Isabelle], deps = [])
1.207 def AFP_images(*args):
1.208 """Isabelle images needed for the AFP (64 bit)"""
1.209 - return isabelle_dependency_only(*args)
1.210 + return isabelle_build(*(args + ("-b", "-j", "2", "Pure", "HOL", "HOL-HOLCF", "HOL-Word")), more_settings=settings64)
1.211
1.212 @configuration(repos = [Isabelle], deps = [])
1.213 def Isabelle_makeall(*args):
1.214 - """Isabelle makeall"""
1.215 - return isabelle_makeall(*args)
1.216 -
1.217 -
1.218 -# distribution and documentation Build
1.219 -
1.220 -@configuration(repos = [Isabelle], deps = [])
1.221 -def Distribution(env, case, paths, dep_paths, playground):
1.222 - """Build of distribution"""
1.223 - ## FIXME This is rudimentary; study Admin/CHECKLIST to complete this configuration accordingly
1.224 - isabelle_home = paths[0]
1.225 - (return_code, log) = env.run_process(path.join(isabelle_home, 'Admin', 'Release', 'makedist'),
1.226 - REPOS = repositories.get(Isabelle).local_path, DISTPREFIX = os.getcwd())
1.227 - return (return_code == 0, '', ## FIXME might add summary here
1.228 - {}, {'log': log}, None) ## FIXME might add proper result here
1.229 -
1.230 -@configuration(repos = [Isabelle], deps = [
1.231 - (HOL, [0]),
1.232 - (HOL_HOLCF, [0]),
1.233 - (ZF, [0]),
1.234 - (HOL_Library, [0])
1.235 - ])
1.236 -def Documentation_images(*args):
1.237 - """Isabelle images needed to build the documentation"""
1.238 - return isabelle_dependency_only(*args)
1.239 -
1.240 -@configuration(repos = [Isabelle], deps = [(Documentation_images, [0])])
1.241 -def Documentation(env, case, paths, dep_paths, playground):
1.242 - """Build of documentation"""
1.243 - isabelle_home = paths[0]
1.244 - dep_path = dep_paths[0]
1.245 - prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path,
1.246 - usedir_options = default_usedir_options)
1.247 - (return_code, log) = env.run_process(path.join(isabelle_home, 'Admin', 'build', 'doc-src'))
1.248 - return (return_code == 0, extract_isabelle_run_summary(log),
1.249 - extract_report_data(isabelle_home, log), {'log': log}, None)
1.250 + """Build all sessions"""
1.251 + return isabelle_build(*(args + ("-j", "6", "-o", "threads=4", "-a")), more_settings=settings64)
1.252
1.253
1.254 # Mutabelle configurations
1.255 @@ -497,13 +404,62 @@
1.256 ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
1.257 '''
1.258
1.259 -@configuration(repos = [Isabelle], deps = [])
1.260 +@configuration(repos = [Isabelle], deps = [(Pure, [0])])
1.261 def SML_HOL(*args):
1.262 """HOL image built with SML/NJ"""
1.263 - return isabelle_make('src/HOL', *args, more_settings=smlnj_settings, target='HOL', keep_results=True)
1.264 + return isabelle_build(*(args + ("-b", "HOL")), more_settings=smlnj_settings)
1.265
1.266 @configuration(repos = [Isabelle], deps = [])
1.267 def SML_makeall(*args):
1.268 - """Makeall built with SML/NJ"""
1.269 - return isabelle_makeall(*args, more_settings=smlnj_settings, target='smlnj', make_options=('-j', '3'))
1.270 + """SML/NJ build of all possible sessions"""
1.271 + return isabelle_build(*(args + ("-j", "3", "-a")), more_settings=smlnj_settings)
1.272
1.273 +
1.274 +# Legacy Isabelle configurations
1.275 +
1.276 +# distribution and documentation Build
1.277 +
1.278 +@configuration(repos = [Isabelle], deps = [])
1.279 +def Distribution(env, case, paths, dep_paths, playground):
1.280 + """Build of distribution"""
1.281 + ## FIXME This is rudimentary; study Admin/CHECKLIST to complete this configuration accordingly
1.282 + isabelle_home = paths[0]
1.283 + (return_code, log) = env.run_process(path.join(isabelle_home, 'Admin', 'Release', 'makedist'),
1.284 + REPOS = repositories.get(Isabelle).local_path, DISTPREFIX = os.getcwd())
1.285 + return (return_code == 0, '', ## FIXME might add summary here
1.286 + {}, {'log': log}, None) ## FIXME might add proper result here
1.287 +
1.288 +
1.289 +def isabelle_dependency_only(env, case, paths, dep_paths, playground):
1.290 +
1.291 + isabelle_home = paths[0]
1.292 + result = path.join(isabelle_home, 'heaps')
1.293 + os.makedirs(result)
1.294 + for dep_path in dep_paths:
1.295 + subprocess.check_call(['cp', '-R'] + glob(dep_path + '/*') + [result])
1.296 +
1.297 + return (True, 'ok', {}, {}, result)
1.298 +
1.299 +
1.300 +@configuration(repos = [Isabelle], deps = [
1.301 + (HOL, [0]),
1.302 + (HOL_HOLCF, [0]),
1.303 + (ZF, [0]),
1.304 + (HOL_Library, [0])
1.305 + ])
1.306 +def Documentation_images(*args):
1.307 + """Isabelle images needed to build the documentation"""
1.308 + return isabelle_dependency_only(*args)
1.309 +
1.310 +@configuration(repos = [Isabelle], deps = [(Documentation_images, [0])])
1.311 +def Documentation(env, case, paths, dep_paths, playground):
1.312 + """Build of documentation"""
1.313 + isabelle_home = paths[0]
1.314 + dep_path = dep_paths[0]
1.315 + prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path,
1.316 + usedir_options = default_usedir_options)
1.317 + (return_code, log) = env.run_process(path.join(isabelle_home, 'Admin', 'build', 'doc-src'))
1.318 + return (return_code == 0, extract_isabelle_run_summary(log),
1.319 + extract_report_data(isabelle_home, log), {'log': log}, None)
1.320 +
1.321 +