505 @configuration(repos = [Isabelle], deps = []) |
505 @configuration(repos = [Isabelle], deps = []) |
506 def SML_makeall(*args): |
506 def SML_makeall(*args): |
507 """Makeall built with SML/NJ""" |
507 """Makeall built with SML/NJ""" |
508 return isabelle_makeall(*args, more_settings=smlnj_settings, target='smlnj', make_options=('-j', '3')) |
508 return isabelle_makeall(*args, more_settings=smlnj_settings, target='smlnj', make_options=('-j', '3')) |
509 |
509 |
510 |
|
511 |
|
512 # Importer |
|
513 |
|
514 @configuration(repos = ['Hollight'], deps = []) |
|
515 def Hollight_proof_objects(env, case, paths, dep_paths, playground): |
|
516 """Build proof object bundle from HOL Light""" |
|
517 |
|
518 hollight_home = paths[0] |
|
519 os.chdir(os.path.join(hollight_home, 'Proofrecording', 'hol_light')) |
|
520 |
|
521 subprocess.check_call(['make']) |
|
522 (return_code, _) = util.run_process.run_process( |
|
523 '''echo -e '#use "hol.ml";;\n export_saved_proofs None;;' | ocaml''', |
|
524 environment={'HOLPROOFEXPORTDIR': './proofs_extended', 'HOLPROOFOBJECTS': 'EXTENDED'}, |
|
525 shell=True) |
|
526 subprocess.check_call('tar -czf proofs_extended.tar.gz proofs_extended'.split(' ')) |
|
527 subprocess.check_call(['mv', 'proofs_extended.tar.gz', playground]) |
|
528 |
|
529 return (return_code == 0, '', {}, {}, playground) |
|
530 |
|
531 |
|
532 @configuration(repos = [Isabelle, 'Hollight'], deps = [(Hollight_proof_objects, [1])]) |
|
533 def HOL_Generate_HOLLight(env, case, paths, dep_paths, playground): |
|
534 """Generated theories by HOL Light import""" |
|
535 |
|
536 os.chdir(playground) |
|
537 subprocess.check_call(['tar', '-xzf', path.join(dep_paths[0], 'proofs_extended.tar.gz')]) |
|
538 proofs_dir = path.join(playground, 'proofs_extended') |
|
539 |
|
540 return isabelle_make('src/HOL', env, case, paths, dep_paths, playground, |
|
541 more_settings=('HOL4_PROOFS="%s"' % proofs_dir), target='HOL-Generate-HOLLight') |
|