diff -r 9cb122742f5c -r 3c71630041c7 Admin/mira.py --- a/Admin/mira.py Fri Mar 25 15:22:09 2011 +0100 +++ b/Admin/mira.py Thu Mar 24 23:14:49 2011 +0100 @@ -13,7 +13,7 @@ # build and evaluation tools -def prepare_isabelle_repository(loc_isabelle, loc_contrib, loc_dependency_heaps, parallelism = True): +def prepare_isabelle_repository(loc_isabelle, loc_contrib, loc_dependency_heaps, parallelism = True, more_settings=''): loc_contrib = path.expanduser(loc_contrib) if not path.exists(loc_contrib): @@ -50,7 +50,8 @@ ISABELLE_USEDIR_OPTIONS="$ISABELLE_USEDIR_OPTIONS %s -t true -v true -d pdf -g true -i true" Z3_NON_COMMERCIAL="yes" -''' % (isabelle_path, parallelism_options) +%s +''' % (isabelle_path, parallelism_options, more_settings) writer = open(path.join(loc_isabelle, 'etc', 'settings'), 'a') writer.write(extra_settings) @@ -105,11 +106,11 @@ return (True, 'ok', {}, {}, result) -def build_isabelle_image(subdir, base, img, env, case, paths, dep_paths, playground): +def build_isabelle_image(subdir, base, img, env, case, paths, dep_paths, playground, more_settings=''): p = paths[0] dep_path = dep_paths[0] - prepare_isabelle_repository(p, env.settings.contrib, dep_path) + prepare_isabelle_repository(p, env.settings.contrib, dep_path, more_settings=more_settings) os.chdir(path.join(p, 'src', subdir)) (return_code, log) = isabelle_usedir(env, p, '-b', base, img) @@ -119,14 +120,14 @@ {'timing': extract_isabelle_run_timing(log)}, {'log': log}, result) -def isabelle_makeall(env, case, paths, dep_paths, playground): +def isabelle_makeall(env, case, paths, dep_paths, playground, more_settings='', target='all'): p = paths[0] dep_path = dep_paths[0] - prepare_isabelle_repository(p, env.settings.contrib, dep_path) + prepare_isabelle_repository(p, env.settings.contrib, dep_path, more_settings=more_settings) os.chdir(p) - (return_code, log) = env.run_process('%s/bin/isabelle' % p, 'makeall', '-k', 'all') + (return_code, log) = env.run_process('%s/bin/isabelle' % p, 'makeall', '-k', target) return (return_code == 0, extract_isabelle_run_summary(log), {'timing': extract_isabelle_run_timing(log)}, {'log': log}, None)