mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

Refactor update_api.mk_ml() so that the source and output directories

Browse source 
can be different. This feature will be needed by the CMake build system
to build the OCaml bindings.
This commit is contained in:
Dan Liew 2016-11-21 01:04:55 +00:00
parent 76bbecf4fe
commit 2e74a2c54e
2 changed files with 24 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
scripts/mk_util.py
View file

@ -2870,7 +2870,8 @@ def mk_bindings(api_files):
dotnet_output_dir=dotnet_output_dir,
java_output_dir=java_output_dir,
java_package_name=java_package_name,
ml_output_dir=ml_output_dir
ml_output_dir=ml_output_dir,
ml_src_dir=ml_output_dir
)
cp_z3py_to_build()
if is_ml_enabled():

32
scripts/update_api.py
View file

@ -1195,13 +1195,13 @@ def ml_alloc_and_store(t, lhs, rhs):
alloc_str = '%s = caml_alloc_custom(&%s, sizeof(%s), 0, 1); ' % (lhs, pops, pts)
return alloc_str + ml_set_wrap(t, lhs, rhs)
def mk_ml(ml_dir):
def mk_ml(ml_src_dir, ml_output_dir):
global Type2Str
ml_nativef = os.path.join(ml_dir, 'z3native.ml')
ml_nativef = os.path.join(ml_output_dir, 'z3native.ml')
ml_native = open(ml_nativef, 'w')
ml_native.write('(* Automatically generated file *)\n\n')
ml_pref = open(os.path.join(ml_dir, 'z3native.ml.pre'), 'r')
ml_pref = open(os.path.join(ml_src_dir, 'z3native.ml.pre'), 'r')
for s in ml_pref:
ml_native.write(s);
ml_pref.close()
@ -1250,14 +1250,14 @@ def mk_ml(ml_dir):
if mk_util.is_verbose():
print ('Generated "%s"' % ml_nativef)
mk_z3native_stubs_c(ml_dir)
mk_z3native_stubs_c(ml_src_dir, ml_output_dir)
def mk_z3native_stubs_c(ml_dir): # C interface
ml_wrapperf = os.path.join(ml_dir, 'z3native_stubs.c')
def mk_z3native_stubs_c(ml_src_dir, ml_output_dir): # C interface
ml_wrapperf = os.path.join(ml_output_dir, 'z3native_stubs.c')
ml_wrapper = open(ml_wrapperf, 'w')
ml_wrapper.write('// Automatically generated file\n\n')
ml_pref = open(os.path.join(ml_dir, 'z3native_stubs.c.pre'), 'r')
ml_pref = open(os.path.join(ml_src_dir, 'z3native_stubs.c.pre'), 'r')
for s in ml_pref:
ml_wrapper.write(s);
ml_pref.close()
@ -1666,7 +1666,8 @@ def generate_files(api_files,
dotnet_output_dir=None,
java_output_dir=None,
java_package_name=None,
ml_output_dir=None):
ml_output_dir=None,
ml_src_dir=None):
"""
Scan the api files in ``api_files`` and emit the relevant API files into
the output directories specified. If an output directory is set to ``None``
@ -1741,7 +1742,8 @@ def generate_files(api_files,
mk_java(java_output_dir, java_package_name)
if ml_output_dir:
mk_ml(ml_output_dir)
assert not ml_src_dir is None
mk_ml(ml_src_dir, ml_output_dir)
def main(args):
logging.basicConfig(level=logging.INFO)
@ -1768,6 +1770,10 @@ def main(args):
dest="java_package_name",
default=None,
help="Name to give the Java package (e.g. ``com.microsoft.z3``).")
parser.add_argument("--ml-src-dir",
dest="ml_src_dir",
default=None,
help="Directory containing OCaml source files. If not specified no files are emitted")
parser.add_argument("--ml-output-dir",
dest="ml_output_dir",
default=None,
@ -1779,6 +1785,11 @@ def main(args):
logging.error('--java-package-name must be specified')
return 1
if pargs.ml_output_dir:
if pargs.ml_src_dir is None:
logging.error('--ml-src-dir must be specified')
return 1
for api_file in pargs.api_files:
if not os.path.exists(api_file):
logging.error('"{}" does not exist'.format(api_file))
@ -1790,7 +1801,8 @@ def main(args):
dotnet_output_dir=pargs.dotnet_output_dir,
java_output_dir=pargs.java_output_dir,
java_package_name=pargs.java_package_name,
ml_output_dir=pargs.ml_output_dir)
ml_output_dir=pargs.ml_output_dir,
ml_src_dir=pargs.ml_src_dir)
return 0
if __name__ == '__main__':