equal
deleted
inserted
replaced
450 |
450 |
451 hollight_home = paths[0] |
451 hollight_home = paths[0] |
452 os.chdir(os.path.join(hollight_home, 'Proofrecording', 'hol_light')) |
452 os.chdir(os.path.join(hollight_home, 'Proofrecording', 'hol_light')) |
453 |
453 |
454 subprocess.check_call(['make']) |
454 subprocess.check_call(['make']) |
455 (return_code, _) = run_process.run_process( |
455 (return_code, _) = util.run_process.run_process( |
456 '''echo -e '#use "hol.ml";;\n export_saved_proofs None;;' | ocaml''', |
456 '''echo -e '#use "hol.ml";;\n export_saved_proofs None;;' | ocaml''', |
457 environment={'HOLPROOFEXPORTDIR': './proofs_extended', 'HOLPROOFOBJECTS': 'EXTENDED'}, |
457 environment={'HOLPROOFEXPORTDIR': './proofs_extended', 'HOLPROOFOBJECTS': 'EXTENDED'}, |
458 shell=True) |
458 shell=True) |
459 subprocess.check_call('tar -czf proofs_extended.tar.gz proofs_extended'.split(' ')) |
459 subprocess.check_call('tar -czf proofs_extended.tar.gz proofs_extended'.split(' ')) |
460 subprocess.check_call(['mv', 'proofs_extended.tar.gz', playground]) |
460 subprocess.check_call(['mv', 'proofs_extended.tar.gz', playground]) |