# HG changeset patch
# User bulwahn
# Date 1301069361 -3600
# Node ID a51761c262d1a1f40c9848bf515ca05eea714e5b
# Parent  306713ec55c3ca0b0344f92b1ff10f6827016f43# Parent  b9ae421fbcc7295a19941cd1016262ba87ec8824
merged

diff -r 306713ec55c3 -r a51761c262d1 Admin/mira.py
--- a/Admin/mira.py	Fri Mar 25 16:03:49 2011 +0100
+++ b/Admin/mira.py	Fri Mar 25 17:09:21 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)
@@ -96,8 +97,8 @@
 
 def isabelle_dependency_only(env, case, paths, dep_paths, playground):
 
-    p = paths[0]
-    result = path.join(p, 'heaps')
+    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])
@@ -105,28 +106,41 @@
     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]
+    isabelle_home = paths[0]
     dep_path = dep_paths[0]
-    prepare_isabelle_repository(p, env.settings.contrib, dep_path)
-    os.chdir(path.join(p, 'src', subdir))
+    prepare_isabelle_repository(p, env.settings.contrib, dep_path, more_settings=more_settings)
+    os.chdir(path.join(isabelle_home, 'src', subdir))
 
-    (return_code, log) = isabelle_usedir(env, p, '-b', base, img)
+    (return_code, log) = isabelle_usedir(env, isabelle_home, '-b', base, img)
 
-    result = path.join(p, 'heaps')
+    result = path.join(isabelle_home, 'heaps')
     return (return_code == 0, extract_isabelle_run_summary(log),
       {'timing': extract_isabelle_run_timing(log)}, {'log': log}, result)
 
 
-def isabelle_makeall(env, case, paths, dep_paths, playground):
+def isabelle_make(subdir, env, case, paths, dep_paths, playground, more_settings='', target='all'):
+
+    isabelle_home = paths[0]
+    dep_path = dep_paths[0] if dep_paths else None
+    prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path, 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)
 
-    p = paths[0]
-    dep_path = dep_paths[0]
-    prepare_isabelle_repository(p, env.settings.contrib, dep_path)
-    os.chdir(p)
+    return (return_code == 0, extract_isabelle_run_summary(log),
+      {'timing': extract_isabelle_run_timing(log)}, {'log': log}, None)
+
+
+def isabelle_makeall(env, case, paths, dep_paths, playground, more_settings='', target='all'):
 
-    (return_code, log) = env.run_process('%s/bin/isabelle' % p, 'makeall', '-k', 'all')
+    isabelle_home = paths[0]
+    dep_path = dep_paths[0] if dep_paths else None
+    prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path, more_settings=more_settings)
+    os.chdir(isabelle_home)
+
+    (return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'makeall', '-k', target)
 
     return (return_code == 0, extract_isabelle_run_summary(log),
       {'timing': extract_isabelle_run_timing(log)}, {'log': log}, None)
@@ -138,13 +152,13 @@
 def Pure(env, case, paths, dep_paths, playground):
     """Pure image"""
 
-    p = paths[0]
-    prepare_isabelle_repository(p, env.settings.contrib, '')
-    os.chdir(path.join(p, 'src', 'Pure'))
+    isabelle_home = paths[0]
+    prepare_isabelle_repository(isabelle_home, env.settings.contrib, '')
+    os.chdir(path.join(isabelle_home, 'src', 'Pure'))
 
-    (return_code, log) = env.run_process('%s/bin/isabelle' % p, 'make', 'Pure')
+    (return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'make', 'Pure')
 
-    result = path.join(p, 'heaps')
+    result = path.join(isabelle_home, 'heaps')
     return (return_code == 0, extract_isabelle_run_summary(log),
       {'timing': extract_isabelle_run_timing(log)}, {'log': log}, result)
 
@@ -315,3 +329,22 @@
     """Judgement Day regression suite SN"""
     return judgement_day('Isabelle/src/HOL/Proofs/Lambda', 'StrongNorm', 'prover_timeout=10', *args)
 
+
+# SML/NJ
+
+smlnj_settings = '''
+ML_SYSTEM=smlnj
+ML_HOME="/home/smlnj/110.72/bin"
+ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=256"
+ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
+'''
+
+@configuration(repos = [Isabelle], deps = [])
+def SML_HOL(*args):
+    """HOL image built with SML/NJ"""
+    return isabelle_make('src/HOL', *args, more_settings=smlnj_settings, target='HOL')
+
+@configuration(repos = [Isabelle], deps = [])
+def SML_makeall(*args):
+    """Makeall built with SML/NJ"""
+    return isabelle_makeall(*args, more_settings=smlnj_settings)