1.1 --- a/Admin/mira.py	Mon Jul 18 18:52:52 2011 +0200
     1.2 +++ b/Admin/mira.py	Mon Jul 18 23:35:50 2011 +0200
     1.3 @@ -439,3 +439,36 @@
     1.4  def SML_makeall(*args):
     1.5      """Makeall built with SML/NJ"""
     1.6      return isabelle_makeall(*args, more_settings=smlnj_settings, target='smlnj', make_options=('-j', '3'))
     1.7 +
     1.8 +
     1.9 +
    1.10 +# Importer
    1.11 +
    1.12 +@configuration(repos = ['Hollight'], deps = [])
    1.13 +def Hollight_proof_objects(env, case, paths, dep_paths, playground):
    1.14 +    """Build proof object bundle from HOL Light"""
    1.15 +
    1.16 +    hollight_home = paths[0]
    1.17 +    os.chdir(os.path.join(hollight_home, 'Proofrecording', 'hol_light'))
    1.18 +
    1.19 +    subprocess.check_call(['make'])
    1.20 +    (return_code, _) = run_process.run_process(
    1.21 +       '''echo -e '#use "hol.ml";;\n export_saved_proofs None;;' | ocaml''',
    1.22 +       environment={'HOLPROOFEXPORTDIR': './proofs_extended', 'HOLPROOFOBJECTS': 'EXTENDED'},
    1.23 +       shell=True)
    1.24 +    subprocess.check_call('tar -czf proofs_extended.tar.gz proofs_extended'.split(' '))
    1.25 +    subprocess.check_call(['mv', 'proofs_extended.tar.gz', playground])
    1.26 +
    1.27 +    return (return_code == 0, '', {}, {}, playground)
    1.28 +
    1.29 +
    1.30 +@configuration(repos = [Isabelle, 'Hollight'], deps = [(Hollight_proof_objects, [1])])
    1.31 +def HOL_Generate_HOLLight(env, case, paths, dep_paths, playground):
    1.32 +    """Generated theories by HOL Light import"""
    1.33 +
    1.34 +    os.chdir(playground)
    1.35 +    subprocess.check_call(['tar', '-xzf', path.join(dep_paths[0], 'proofs_extended.tar.gz')])
    1.36 +    proofs_dir = path.join(playground, 'proofs_extended')
    1.37 +
    1.38 +    return isabelle_make('src/HOL', env, case, paths, dep_paths, playground,
    1.39 +      more_settings=('HOL4PROOFS="%s"' % proofs_dir), target='HOL-Generate-HOLLight')