diff --git a/scripts/mk_util.py b/scripts/mk_util.py index d644b269c..fd8962bda 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -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(): diff --git a/scripts/update_api.py b/scripts/update_api.py index 3a3b2c40a..e531a103c 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -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__':