From 49dd2e4a07a48ce106c86cb0b6fefee804bc47ee Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 8 Jan 2013 20:56:49 +0000 Subject: [PATCH] ML API: build system changes Signed-off-by: Christoph M. Wintersteiger --- scripts/mk_util.py | 48 +++++++++++++++++++++++++++++++++++----------- src/api/ml/README | 2 +- 2 files changed, 38 insertions(+), 12 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 9dcf43813..4c39ff13b 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1342,6 +1342,7 @@ class MLComponent(Component): def mk_makefile(self, out): if is_ml_enabled(): +<<<<<<< HEAD CP_CMD = "cp" if IS_WINDOWS: CP_CMD = "copy" @@ -1436,18 +1437,31 @@ class MLComponent(Component): mk_dir(bld_dir) libfile = '%s$(SO_EXT)' % self.lib_name out.write('%s: libz3$(SO_EXT) %s' % (libfile, os.path.join(self.to_src_dir, 'z3native.c'))) +======= + src_dir = self.to_src_dir + sub_dir = os.path.join('api', 'ml') + mk_dir(os.path.join(BUILD_DIR, sub_dir)) + for f in filter(lambda f: f.endswith('.ml'), os.listdir(self.src_dir)): + shutil.copyfile(os.path.join(self.src_dir, f), os.path.join(BUILD_DIR, sub_dir, f)) + for f in filter(lambda f: f.endswith('.c'), os.listdir(self.src_dir)): + shutil.copyfile(os.path.join(self.src_dir, f), os.path.join(BUILD_DIR, sub_dir, f)) + out.write('z3.cmxa:') + for mlfile in get_ml_files(self.src_dir): + out.write(' %s' % os.path.join(src_dir, mlfile)) + out.write('\n') + out.write('\tpushd %s && %s ' % (sub_dir, OCAMLOPT)) + if DEBUG_MODE: + out.write('-g ') + out.write('-ccopt "-I../../%s" -cclib "-L../.. -lz3" z3native.c z3enums.ml z3native.ml z3.ml -a -o ../../z3.cmxa -linkall && popd\n' % get_component(API_COMPONENT).to_src_dir) + out.write('z3.cma:') +>>>>>>> ML API: build system changes for mlfile in get_ml_files(self.src_dir): out.write(' %s' % os.path.join(self.to_src_dir, mlfile)) out.write('\n') - out.write('\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)api/ml/z3native$(OBJ_EXT) -I"%s" -I%s %s/z3native.c\n' % (get_component(API_COMPONENT).to_src_dir, OCAML_LIB, self.to_src_dir)) - if IS_WINDOWS: - out.write('\t$(SLINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(LIB_EXT)\n' % (libfile, os.path.join('api', 'ml', 'z3native'))) - else: - out.write('\t$(SLINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' % (libfile, os.path.join('api', 'ml', 'z3native'))) - out.write('z3.cmxa: %s\n' % libfile) - out.write('\tcd %s && ocamlbuild -cflags \'-g\' -lflags -cclib,-L../..,-cclib,-lz3,-cclib,-lz3ml,-linkall -build-dir ../../../%s/api/ml z3.cmxa z3native$(OBJ_EXT) && cd -\n' % (self.to_src_dir,BUILD_DIR)) - out.write('z3.cma: %s\n' % libfile) - out.write('\tcd %s && ocamlbuild -cflags \'-g\' -lflags -custom,-cclib,-L../..,-cclib,-lz3,-cclib,-lz3ml,-linkall -build-dir ../../../%s/api/ml z3native$(OBJ_EXT) z3.cma && cd -\n' % (self.to_src_dir,BUILD_DIR)) + out.write('\tpushd %s && %s ' % (sub_dir, OCAMLC)) + if DEBUG_MODE: + out.write('-g ') + out.write('-custom -ccopt "-I../../%s" -cclib "-L../.. -lz3" z3native.c z3enums.ml z3native.ml z3.ml -a -o ../../z3.cma -linkall && popd\n' % get_component(API_COMPONENT).to_src_dir) out.write('ml: z3.cmxa z3.cma\n') out.write('\n') @@ -1576,7 +1590,10 @@ class MLExampleComponent(ExampleComponent): for mlfile in get_ml_files(self.ex_dir): out.write(' %s' % os.path.join(self.to_ex_dir, mlfile)) out.write('\n') - out.write('\tocamlc -g -o ml_example.byte -I . z3.cma -I api/ml') + out.write('\t%s ' % OCAMLC) + if DEBUG_MODE: + out.write('-g ') + out.write('-custom -o ml_example.byte -I . z3.cma -I api/ml') for mlfile in get_ml_files(self.ex_dir): out.write(' %s/%s' % (self.to_ex_dir, mlfile)) out.write('\n') @@ -1584,7 +1601,10 @@ class MLExampleComponent(ExampleComponent): for mlfile in get_ml_files(self.ex_dir): out.write(' %s' % os.path.join(self.to_ex_dir, mlfile)) out.write('\n') - out.write('\tocamlopt -g -o ml_example -I . z3.cmxa -I api/ml') + out.write('\t%s ' % OCAMLOPT) + if DEBUG_MODE: + out.write('-g ') + out.write('-o ml_example($EXE_EXT) -I . z3.cmxa -I api/ml') for mlfile in get_ml_files(self.ex_dir): out.write(' %s/%s' % (self.to_ex_dir, mlfile)) out.write('\n') @@ -1862,9 +1882,15 @@ def mk_config(): print('JNI Bindings: %s' % JNI_HOME) print('Java Compiler: %s' % JAVAC) if is_ml_enabled(): +<<<<<<< HEAD print('Ocaml Compiler: %s' % OCAMLC) print('Ocaml Native: %s' % OCAMLOPT) print('Ocaml Library: %s' % OCAML_LIB) +======= + print('OCaml Compiler: %s' % OCAMLC) + print('OCaml Native: %s' % OCAMLOPT) + print('OCaml Library: %s' % OCAML_LIB) +>>>>>>> ML API: build system changes def mk_install(out): out.write('install: ') diff --git a/src/api/ml/README b/src/api/ml/README index 36f903925..beee7d864 100644 --- a/src/api/ml/README +++ b/src/api/ml/README @@ -5,4 +5,4 @@ We are currently working on a brand new ML API. On Windows, there are no less than four different ports of OCaml. The Z3 build system assumes that either the win32 or the win64 port is installed. This means that OCaml will use `cl' as the underlying C compiler and not the cygwin or -mingw compilers. +mingw compilers. \ No newline at end of file