Admin/mira.py
changeset 43903 1e2aa420c660
parent 43897 b28745c3ddce
child 45157 efc2e2d80218
equal deleted inserted replaced
43902:8064210028b7 43903:1e2aa420c660
   469     os.chdir(playground)
   469     os.chdir(playground)
   470     subprocess.check_call(['tar', '-xzf', path.join(dep_paths[0], 'proofs_extended.tar.gz')])
   470     subprocess.check_call(['tar', '-xzf', path.join(dep_paths[0], 'proofs_extended.tar.gz')])
   471     proofs_dir = path.join(playground, 'proofs_extended')
   471     proofs_dir = path.join(playground, 'proofs_extended')
   472 
   472 
   473     return isabelle_make('src/HOL', env, case, paths, dep_paths, playground,
   473     return isabelle_make('src/HOL', env, case, paths, dep_paths, playground,
   474       more_settings=('HOL4PROOFS="%s"' % proofs_dir), target='HOL-Generate-HOLLight')
   474       more_settings=('HOL4_PROOFS="%s"' % proofs_dir), target='HOL-Generate-HOLLight')