# HG changeset patch
# User krauss
# Date 1344172269 -7200
# Node ID 9f9b289964dc9eed67940a4f8477d95d1032a638
# Parent  9170e10c651e6412437c51c931326eeb205b02cc
removed mira configurations related to old importer

diff -r 9170e10c651e -r 9f9b289964dc Admin/mira.py
--- a/Admin/mira.py	Sun Aug 05 21:57:25 2012 +0200
+++ b/Admin/mira.py	Sun Aug 05 15:11:09 2012 +0200
@@ -507,35 +507,3 @@
     """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=('HOL4_PROOFS="%s"' % proofs_dir), target='HOL-Generate-HOLLight')