Admin/mira.py
changeset 42113 3c71630041c7
parent 42109 f5950b976076
child 42114 1cdf54e845fa
--- 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)