437 |
437 |
438 @configuration(repos = [Isabelle], deps = []) |
438 @configuration(repos = [Isabelle], deps = []) |
439 def SML_makeall(*args): |
439 def SML_makeall(*args): |
440 """Makeall built with SML/NJ""" |
440 """Makeall built with SML/NJ""" |
441 return isabelle_makeall(*args, more_settings=smlnj_settings, target='smlnj', make_options=('-j', '3')) |
441 return isabelle_makeall(*args, more_settings=smlnj_settings, target='smlnj', make_options=('-j', '3')) |
|
442 |
|
443 |
|
444 |
|
445 # Importer |
|
446 |
|
447 @configuration(repos = ['Hollight'], deps = []) |
|
448 def Hollight_proof_objects(env, case, paths, dep_paths, playground): |
|
449 """Build proof object bundle from HOL Light""" |
|
450 |
|
451 hollight_home = paths[0] |
|
452 os.chdir(os.path.join(hollight_home, 'Proofrecording', 'hol_light')) |
|
453 |
|
454 subprocess.check_call(['make']) |
|
455 (return_code, _) = run_process.run_process( |
|
456 '''echo -e '#use "hol.ml";;\n export_saved_proofs None;;' | ocaml''', |
|
457 environment={'HOLPROOFEXPORTDIR': './proofs_extended', 'HOLPROOFOBJECTS': 'EXTENDED'}, |
|
458 shell=True) |
|
459 subprocess.check_call('tar -czf proofs_extended.tar.gz proofs_extended'.split(' ')) |
|
460 subprocess.check_call(['mv', 'proofs_extended.tar.gz', playground]) |
|
461 |
|
462 return (return_code == 0, '', {}, {}, playground) |
|
463 |
|
464 |
|
465 @configuration(repos = [Isabelle, 'Hollight'], deps = [(Hollight_proof_objects, [1])]) |
|
466 def HOL_Generate_HOLLight(env, case, paths, dep_paths, playground): |
|
467 """Generated theories by HOL Light import""" |
|
468 |
|
469 os.chdir(playground) |
|
470 subprocess.check_call(['tar', '-xzf', path.join(dep_paths[0], 'proofs_extended.tar.gz')]) |
|
471 proofs_dir = path.join(playground, 'proofs_extended') |
|
472 |
|
473 return isabelle_make('src/HOL', env, case, paths, dep_paths, playground, |
|
474 more_settings=('HOL4PROOFS="%s"' % proofs_dir), target='HOL-Generate-HOLLight') |