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