diff --git a/makefile b/makefile index 5c3360d18..5b0b58a49 100644 --- a/makefile +++ b/makefile @@ -17,6 +17,7 @@ # find_library(ocaml) # include(FindOCaml) # Todo: use DEPFILE in https://cmake.org/cmake/help/latest/command/add_custom_command.html +# for rpath, see https://discourse.cmake.org/t/how-to-get-an-lc-rpath-and-rpath-prefix-on-a-dylib-on-macos/5540 # Generate ``z3native.ml`` and ``z3native_stubs.c`` @@ -127,6 +128,9 @@ # "${z3ml_bin}/z3enums.cmi" +ML_LIB=/home/ex/.opam/5.2.0/lib +ML_LIB=/Users/ex/.opam/5.2.0/lib +ROOT=$$(pwd) ml0: mkdir -p build @@ -176,11 +180,12 @@ ml: -DCMAKE_VERBOSE_MAKEFILE=TRUE \ -DZ3_BUILD_LIBZ3_SHARED=TRUE \ -DZ3_BUILD_OCAML_BINDINGS=TRUE \ - -DZ3_BUILD_OCAML_EXTERNAL_LIBZ3=/home/ex/my_z3 \ - -DZ3_USE_LIB_GMP=TRUE \ --debug-trycompile \ ../ +# -DZ3_BUILD_OCAML_EXTERNAL_LIBZ3=/home/ex/my_z3 \ +# -DZ3_USE_LIB_GMP=TRUE \ + # LD_LIBRARY_PATH=build ./build/src/api/ml/ml_example build-all: @@ -210,10 +215,10 @@ MKLIB_FLAGS = \ -package zarith \ -lz3 -lstdc++ -lpthread\ -lgmp \ - -L/home/ex/code/ocaml-build-examples/vendor/z3/build \ - -dllpath /home/ex/code/ocaml-build-examples/vendor/z3/build \ - -L/home/ex/.opam/5.1.1/lib/stublibs \ - -dllpath /home/ex/.opam/5.1.1/lib/stublibs \ + -L$(ROOT)/build \ + -dllpath $(ROOT)/build \ + -L$(ML_LIB)/stublibs \ + -dllpath $(ML_LIB)/stublibs \ -I build/src/api/ml \ -o build/src/api/ml/z3ml @@ -232,74 +237,74 @@ om: # why? # DEPENDS "${z3ml_bin}/z3enums.cmo" +# -I +threads \ or1: ocamlfind ocamlc -verbose \ -o ml_example.byte \ -package zarith \ - -I +threads \ - -I /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml \ - -dllpath /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml \ - -I /home/ex/.opam/5.1.1/lib/stublibs \ - -dllpath /home/ex/.opam/5.1.1/lib/stublibs \ - /home/ex/.opam/5.1.1/lib/zarith/zarith.cma \ - /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml/z3ml.cma \ - /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml/ml_example.ml \ + -I $(ROOT)/build/src/api/ml \ + -dllpath $(ROOT)/build/src/api/ml \ + -I $(ML_LIB)/stublibs \ + -dllpath $(ML_LIB)/stublibs \ + $(ML_LIB)/zarith/zarith.cma \ + $(ROOT)/build/src/api/ml/z3ml.cma \ + $(ROOT)/build/src/api/ml/ml_example.ml \ # -linkpkg \ or2: ocamlrun ml_example.byte -# -I /home/ex/.opam/5.1.1/lib/stublibs \ +# -I $(ML_LIB)/stublibs \ # "-cclib" "-L${PROJECT_BINARY_DIR}" # "-cclib" [[-L. -lpthread -lstdc++ -lz3]] # "-linkpkg" # "-cclib" "-L${PROJECT_BINARY_DIR}" # "-cclib" [[-L. -lpthread -lstdc++ -lz3]] +# -I +threads \ oc1: ocamlfind ocamlopt \ - -I +threads \ -o ml_example \ -package zarith \ -linkpkg \ - -I /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml \ + -I $(ROOT)/build/src/api/ml \ z3ml.cmxa \ - /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml/ml_example.ml + $(ROOT)/build/src/api/ml/ml_example.ml oc2: ./ml_example # must have -# /home/ex/.opam/5.1.1/lib/zarith/zarith.cma -# -I /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml +# $(ML_LIB)/zarith/zarith.cma +# -I $(ROOT)/build/src/api/ml # can be removed # -cclib "-lstdc++ -lz3" -# -cclib "-L. -L/home/ex/.opam/5.1.1/lib/stublibs -L/home/ex/.opam/5.1.1/lib/zarith " -# -L/home/ex/code/ocaml-build-examples/vendor/z3/build +# -cclib "-L. -L$(ML_LIB)/stublibs -L$(ML_LIB)/zarith " +# -L$(ROOT)/build # -package zarith # -linkpkg # -lpthread # -package z3 -# -I /home/ex/.opam/5.1.1/lib/zarith +# -I $(ML_LIB)/zarith # must not have # -custom -# -o /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml/ml_example.byte +# -o $(ROOT)/build/src/api/ml/ml_example.byte -# CAML_LD_LIBRARY_PATH=/home/ex/.opam/5.1.1/lib/stublibs:/home/ex/code/ocaml-build-examples/vendor/z3/build:/home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml:/home/ex/.opam/5.1.1/lib/zarith +# CAML_LD_LIBRARY_PATH=$(ML_LIB)/stublibs:$(ROOT)/build:$(ROOT)/build/src/api/ml:$(ML_LIB)/zarith or3: - ocamlrun -I /home/ex/.opam/5.1.1/lib/zarith -I /home/ex/.opam/5.1.1/lib/stublibs -I /home/ex/.opam/5.1.1/lib/zarith ml_example.byte + ocamlrun -I $(ML_LIB)/zarith -I $(ML_LIB)/stublibs -I $(ML_LIB)/zarith ml_example.byte -# -I /home/ex/.opam/5.1.1/lib/zarith -# -I /home/ex/.opam/5.1.1/lib/stublibs -# -I /home/ex/code/ocaml-build-examples/vendor/z3/build -# -I /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml +# -I $(ML_LIB)/zarith +# -I $(ML_LIB)/stublibs +# -I $(ROOT)/build +# -I $(ROOT)/build/src/api/ml # -t -b diff --git a/src/api/ml/CMakeLists.txt b/src/api/ml/CMakeLists.txt index 5cd31d444..18ea6f15d 100644 --- a/src/api/ml/CMakeLists.txt +++ b/src/api/ml/CMakeLists.txt @@ -153,19 +153,36 @@ execute_process( set(ocaml_stublibs_path "${ocaml_destdir_path}/stublibs") +set(c_lib_deps "-lz3" "-lstdc++" "-lpthread") +if (Z3_USE_LIB_GMP) + list(APPEND c_lib_deps "-lgmp") +endif() + +if( APPLE ) + set(ocaml_rpath "@executable_path/../libz3${so_ext}") +elseif( UNIX ) + set(ocaml_rpath "\\$ORIGIN/../libz3${so_ext}") +endif() +list(APPEND c_lib_deps "-dllpath" ${ocaml_rpath}) + +# We may not directly use CMake's BUILD_RPATH or INSTALL_RPATH since they don't set +# the ocaml stub libraries as a normal library target. + set(ocamlmklib_flags "-o" "z3ml" "-ocamlcflags" "-bin-annot" "-package" "zarith" - "-lz3" "-lstdc++" "-lpthread" - $<$:-lgmp> + ${c_lib_deps} "-L${libz3_path}" "-dllpath" "${libz3_path}" "-L${ocaml_stublibs_path}" "-dllpath" "${ocaml_stublibs_path}" + "-dllpath" "@rpath/dllz3ml.so" "-I" "${z3ml_bin}") +# OCaml's dll stublib hava platform-independent name `dll.so` + add_custom_command( - OUTPUT ${z3ml_bin}/dllz3ml${so_ext} + OUTPUT ${z3ml_bin}/dllz3ml.so ${z3ml_bin}/libz3ml.a ${z3ml_bin}/z3ml.cma ${z3ml_bin}/z3ml.cmxa @@ -184,7 +201,7 @@ add_custom_command( "-o" "${z3ml_bin}/z3ml.cmxs" "-I" "${z3ml_bin}" "${z3ml_bin}/z3ml.cmxa" - DEPENDS + DEPENDS libz3_z3ml ${z3ml_bin}/z3native_stubs.o ${z3ml_bin}/z3enums.cmo @@ -193,7 +210,7 @@ add_custom_command( ${z3ml_bin}/z3enums.cmx ${z3ml_bin}/z3native.cmx ${z3ml_bin}/z3.cmx - COMMENT "Building z3ml.{cma,cmxa,cmxs}, dllz3ml${so_ext}, and libz3ml.a" + COMMENT "Building z3ml.{cma,cmxa,cmxs}, dllz3ml.so, and libz3ml.a" VERBATIM) ############################################################################### @@ -212,13 +229,14 @@ execute_process( OUTPUT_VARIABLE ocaml_pkg_zarith_path OUTPUT_STRIP_TRAILING_WHITESPACE) +# "-I" "+threads" + add_custom_command( OUTPUT ${z3ml_bin}/ml_example${bc_ext} ${z3ml_bin}/ml_example.bc.log COMMAND "${OCAMLFIND}" "ocamlc" "-o" "${z3ml_bin}/ml_example${bc_ext}" "-package" "zarith" - "-I" "+threads" "-I" "${z3ml_bin}" "-dllpath" "${z3ml_bin}" "-I" ${ocaml_stublibs_path} @@ -231,17 +249,18 @@ add_custom_command( ">" "${z3ml_bin}/ml_example.bc.log" DEPENDS ${z3ml_bin}/z3ml.cma - ${z3ml_bin}/dllz3ml${so_ext} + ${z3ml_bin}/dllz3ml.so ${z3ml_bin}/ml_example.ml COMMENT "Testing build and run ml_example bytecode" VERBATIM) +# "-I" "+threads" + add_custom_command( OUTPUT ${z3ml_bin}/ml_example${exe_ext} ${z3ml_bin}/ml_example.log COMMAND "${OCAMLFIND}" "ocamlopt" "-o" "${z3ml_bin}/ml_example${exe_ext}" - "-I" "+threads" "-package" "zarith" "-linkpkg" "-I" "${z3ml_bin}" @@ -251,7 +270,7 @@ add_custom_command( ">" "${z3ml_bin}/ml_example.log" DEPENDS ${z3ml_bin}/z3ml.cmxa - ${z3ml_bin}/dllz3ml${so_ext} + ${z3ml_bin}/dllz3ml.so ${z3ml_bin}/ml_example.ml COMMENT "Testing build and run ml_example natively" VERBATIM) @@ -269,7 +288,7 @@ add_custom_target(build_z3_ocaml_bindings ${z3ml_bin}/z3ml.cma ${z3ml_bin}/z3ml.cmxa ${z3ml_bin}/z3ml.cmxs - ${z3ml_bin}/dllz3ml${so_ext} + ${z3ml_bin}/dllz3ml.so ${z3ml_bin}/libz3ml.a build_ocaml_example ) @@ -282,20 +301,20 @@ add_custom_target(build_z3_ocaml_bindings # I don't know how to use conditional `COMMAND` nor specify a file dependency for itself # Renaming it and back seems a simple solution. -# COMMAND mv "${z3ml_bin}/dllz3ml${so_ext}" "${z3ml_bin}/dllz3ml.pre${so_ext}" +# COMMAND mv "${z3ml_bin}/dllz3ml.so" "${z3ml_bin}/dllz3ml.pre.so" # if (NOT APPLE) # add_custom_command( -# OUTPUT "${z3ml_bin}/dllz3ml${so_ext}" -# COMMAND mv "${z3ml_bin}/dllz3ml.pre${so_ext}" "${z3ml_bin}/dllz3ml${so_ext}" -# DEPENDS "${z3ml_bin}/dllz3ml.pre${so_ext}" +# OUTPUT "${z3ml_bin}/dllz3ml.so" +# COMMAND mv "${z3ml_bin}/dllz3ml.pre.so" "${z3ml_bin}/dllz3ml.so}" +# DEPENDS "${z3ml_bin}/dllz3ml.pre.so" # ) # else() # # if IS_OSX: # # install_name_tool -id ${stubs_install_path}/libz3.dylib libz3.dylib # # install_name_tool -change libz3.dylib ${stubs_install_path}/libz3.dylib api/ml/dllz3ml.so # add_custom_command( -# OUTPUT "${z3ml_bin}/dllz3ml${so_ext}" -# COMMAND mv "${z3ml_bin}/dllz3ml.pre${so_ext}" "${z3ml_bin}/dllz3ml${so_ext}" -# DEPENDS "${z3ml_bin}/dllz3ml.pre${so_ext}" +# OUTPUT "${z3ml_bin}/dllz3ml.so" +# COMMAND mv "${z3ml_bin}/dllz3ml.pre.so" "${z3ml_bin}/dllz3ml.so" +# DEPENDS "${z3ml_bin}/dllz3ml.so" # ) # endif() \ No newline at end of file