# HG changeset patch
# User haftmann
# Date 1311052454 -7200
# Node ID 8064210028b73e7da98f4ab9df2b8635c782efdf
# Parent  b28745c3ddcec0b080313033d046c178c1a73b09# Parent  3ab6c30d256dac49c5fe6769b55cbefc98d9ab2c
merged

diff -r 3ab6c30d256d -r 8064210028b7 Admin/mira.py
--- a/Admin/mira.py	Mon Jul 18 21:52:34 2011 +0200
+++ b/Admin/mira.py	Tue Jul 19 07:14:14 2011 +0200
@@ -439,3 +439,36 @@
 def SML_makeall(*args):
     """Makeall built with SML/NJ"""
     return isabelle_makeall(*args, more_settings=smlnj_settings, target='smlnj', make_options=('-j', '3'))
+
+
+
+# Importer
+
+@configuration(repos = ['Hollight'], deps = [])
+def Hollight_proof_objects(env, case, paths, dep_paths, playground):
+    """Build proof object bundle from HOL Light"""
+
+    hollight_home = paths[0]
+    os.chdir(os.path.join(hollight_home, 'Proofrecording', 'hol_light'))
+
+    subprocess.check_call(['make'])
+    (return_code, _) = util.run_process.run_process(
+       '''echo -e '#use "hol.ml";;\n export_saved_proofs None;;' | ocaml''',
+       environment={'HOLPROOFEXPORTDIR': './proofs_extended', 'HOLPROOFOBJECTS': 'EXTENDED'},
+       shell=True)
+    subprocess.check_call('tar -czf proofs_extended.tar.gz proofs_extended'.split(' '))
+    subprocess.check_call(['mv', 'proofs_extended.tar.gz', playground])
+
+    return (return_code == 0, '', {}, {}, playground)
+
+
+@configuration(repos = [Isabelle, 'Hollight'], deps = [(Hollight_proof_objects, [1])])
+def HOL_Generate_HOLLight(env, case, paths, dep_paths, playground):
+    """Generated theories by HOL Light import"""
+
+    os.chdir(playground)
+    subprocess.check_call(['tar', '-xzf', path.join(dep_paths[0], 'proofs_extended.tar.gz')])
+    proofs_dir = path.join(playground, 'proofs_extended')
+
+    return isabelle_make('src/HOL', env, case, paths, dep_paths, playground,
+      more_settings=('HOL4PROOFS="%s"' % proofs_dir), target='HOL-Generate-HOLLight')
diff -r 3ab6c30d256d -r 8064210028b7 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Mon Jul 18 21:52:34 2011 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Tue Jul 19 07:14:14 2011 +0200
@@ -220,7 +220,7 @@
         fun F n =
             let
                 val str = G n Syntax.string_of_term ctxt tn
-                val _ = warning (PolyML.makestring (n, str))
+                val _ = warning (@{make_string} (n, str))
                 val u = Syntax.parse_term ctxt str
                 val u = if t = t' then u else HOLogic.mk_Trueprop u
                 val u = Syntax.check_term ctxt (Type.constraint T u)
diff -r 3ab6c30d256d -r 8064210028b7 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Jul 18 21:52:34 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Jul 19 07:14:14 2011 +0200
@@ -1570,7 +1570,10 @@
 
 (* values_timeout configuration *)
 
-val values_timeout = Attrib.setup_config_real @{binding values_timeout} (K 20.0)
+val default_values_timeout =
+  if String.isPrefix "smlnj" (getenv "ML_SYSTEM") then 600.0 else 20.0
+
+val values_timeout = Attrib.setup_config_real @{binding values_timeout} (K default_values_timeout)
 
 val setup = PredData.put (Graph.empty) #>
   Attrib.setup @{binding code_pred_intro} (Scan.lift (Scan.option Args.name) >> attrib' add_intro)