mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

ML API: build system changes

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-01-08 20:56:49 +00:00
parent 4a606dbe60
commit 49dd2e4a07
2 changed files with 38 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

48
scripts/mk_util.py
View file

@ -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: ')

2
src/api/ml/README
View file

@ -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.