diff --git a/makefile b/makefile index fae646d8c..5c3360d18 100644 --- a/makefile +++ b/makefile @@ -190,10 +190,13 @@ build-mk: cd build && make -j16 build_z3_ocaml_bindings .PHONY:build -# /bin/sh: 1: ocamlfind ocamlc -where: not found +build-nj: + cd build && ninja +.PHONY:build-nj + build: cd build && ninja build_z3_ocaml_bindings -.PHONY:build-nj +.PHONY:build dot: cd build && dot -Tpng -o deps.png deps.dot diff --git a/src/api/ml/CMakeLists.txt b/src/api/ml/CMakeLists.txt index 71902f820..5cd31d444 100644 --- a/src/api/ml/CMakeLists.txt +++ b/src/api/ml/CMakeLists.txt @@ -1,6 +1,3 @@ -############################################################################### -# Install -############################################################################### find_package(OCaml REQUIRED) set(exe_ext ${CMAKE_EXECUTABLE_SUFFIX}) @@ -13,7 +10,7 @@ set(z3ml_bin ${CMAKE_CURRENT_BINARY_DIR}) if (Z3_BUILD_OCAML_EXTERNAL_LIBZ3) add_custom_target(libz3_z3ml ALL - DEPENDS "${Z3_BUILD_OCAML_EXTERNAL_LIBZ3}/libz3${so_ext}" + DEPENDS ${Z3_BUILD_OCAML_EXTERNAL_LIBZ3}/libz3${so_ext} ) set(libz3_path ${Z3_BUILD_OCAML_EXTERNAL_LIBZ3}) else() @@ -24,13 +21,11 @@ else() set(libz3_path ${PROJECT_BINARY_DIR}) endif() -set(Z3ml_native_stubs_c "${z3ml_bin}/z3native_stubs.c") - add_custom_command( OUTPUT - "${z3ml_bin}/z3native.ml" - ${Z3ml_native_stubs_c} - COMMAND "${PYTHON_EXECUTABLE}" + ${z3ml_bin}/z3native.ml + ${z3ml_bin}/z3native_stubs.c + COMMAND "${Python3_EXECUTABLE}" "${PROJECT_SOURCE_DIR}/scripts/update_api.py" ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} "--ml-src-dir" @@ -38,37 +33,36 @@ add_custom_command( "--ml-output-dir" "${CMAKE_CURRENT_BINARY_DIR}" DEPENDS + ${PROJECT_SOURCE_DIR}/scripts/update_api.py ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} - "${PROJECT_SOURCE_DIR}/scripts/update_api.py" ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} - COMMENT "Generatinging ${z3ml_bin}/z3native.ml and ${Z3ml_native_stubs_c}" + COMMENT "Generatinging ${z3ml_bin}/z3native.ml and ${z3ml_bin}/z3native_stubs.c" VERBATIM ) -set(gen_z3enum "${z3ml_bin}/z3enums.ml") add_custom_command( OUTPUT - ${gen_z3enum} - COMMAND "${PYTHON_EXECUTABLE}" + ${z3ml_bin}/z3enums.ml + COMMAND "${Python3_EXECUTABLE}" "${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py" ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} "--ml-output-dir" "${CMAKE_CURRENT_BINARY_DIR}" DEPENDS + ${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} - "${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py" ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} - COMMENT "Generating ${gen_z3enum}" + COMMENT "Generating ${z3ml_bin}/z3enums.ml" VERBATIM ) add_custom_command( - OUTPUT "${z3ml_bin}/z3.ml" - "${z3ml_bin}/z3.mli" + OUTPUT ${z3ml_bin}/z3.ml + ${z3ml_bin}/z3.mli COMMAND "${CMAKE_COMMAND}" "-E" "copy" "${z3ml_src}/z3.ml" "${z3ml_bin}/z3.ml" COMMAND "${CMAKE_COMMAND}" "-E" "copy" "${z3ml_src}/z3.mli" "${z3ml_bin}/z3.mli" - DEPENDS "${z3ml_src}/z3.ml" - "${z3ml_src}/z3.mli" + DEPENDS ${z3ml_src}/z3.ml + ${z3ml_src}/z3.mli COMMENT "Copying z3.ml and z3.mli to build area") set(z3ml_common_flags "-package" "zarith" @@ -88,17 +82,16 @@ add_custom_command( "-I" "${PROJECT_SOURCE_DIR}/src/api" "-I" "${ocaml_stub_lib_path}" "-c" "${z3ml_bin}/z3native_stubs.c" - DEPENDS ${Z3ml_native_stubs_c} + DEPENDS ${z3ml_bin}/z3native_stubs.c COMMENT "Building z3native_stubs.o" VERBATIM) # z3enum.ml depends on nothing - add_custom_command( - OUTPUT "${z3ml_bin}/z3enums.mli" - "${z3ml_bin}/z3enums.cmi" - "${z3ml_bin}/z3enums.cmo" - "${z3ml_bin}/z3enums.cmx" + OUTPUT ${z3ml_bin}/z3enums.mli + ${z3ml_bin}/z3enums.cmi + ${z3ml_bin}/z3enums.cmo + ${z3ml_bin}/z3enums.cmx COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} "-i" "-c" "${z3ml_bin}/z3enums.ml" @@ -109,17 +102,16 @@ add_custom_command( "-c" "${z3ml_bin}/z3enums.ml" COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags} "-c" "${z3ml_bin}/z3enums.ml" - DEPENDS ${gen_z3enum} + DEPENDS ${z3ml_bin}/z3enums.ml COMMENT "Building z3enums.{mli,cmi,cmo,cmx}" VERBATIM) # z3native.ml depends on z3enums - add_custom_command( - OUTPUT "${z3ml_bin}/z3native.mli" - "${z3ml_bin}/z3native.cmi" - "${z3ml_bin}/z3native.cmo" - "${z3ml_bin}/z3native.cmx" + OUTPUT ${z3ml_bin}/z3native.mli + ${z3ml_bin}/z3native.cmi + ${z3ml_bin}/z3native.cmo + ${z3ml_bin}/z3native.cmx COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} "-i" "-c" "${z3ml_bin}/z3native.ml" @@ -130,30 +122,30 @@ add_custom_command( "-c" "${z3ml_bin}/z3native.ml" COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags} "-c" "${z3ml_bin}/z3native.ml" - DEPENDS "${z3ml_bin}/z3enums.cmo" - "${z3ml_bin}/z3native.ml" + DEPENDS ${z3ml_bin}/z3enums.cmo + ${z3ml_bin}/z3native.ml COMMENT "Building z3native.{mli,cmi,cmo,cmx}" VERBATIM) # z3.ml depends on z3enums and z3native - add_custom_command( - OUTPUT "${z3ml_bin}/z3.cmi" - "${z3ml_bin}/z3.cmo" - "${z3ml_bin}/z3.cmx" + OUTPUT ${z3ml_bin}/z3.cmi + ${z3ml_bin}/z3.cmo + ${z3ml_bin}/z3.cmx COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} "-c" "${z3ml_bin}/z3.mli" COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} "-c" "${z3ml_bin}/z3.ml" COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags} "-c" "${z3ml_bin}/z3.ml" - DEPENDS "${z3ml_bin}/z3enums.cmo" - "${z3ml_bin}/z3native.cmo" - "${z3ml_bin}/z3.ml" - "${z3ml_bin}/z3.mli" + DEPENDS ${z3ml_bin}/z3enums.cmo + ${z3ml_bin}/z3native.cmo + ${z3ml_bin}/z3.ml + ${z3ml_bin}/z3.mli COMMENT "Building z3.cmo" VERBATIM) +# making ocaml stublibs execute_process( COMMAND ${OCAMLFIND} printconf destdir OUTPUT_VARIABLE ocaml_destdir_path @@ -173,37 +165,119 @@ set(ocamlmklib_flags "-o" "z3ml" "-I" "${z3ml_bin}") add_custom_command( - OUTPUT "${z3ml_bin}/dllz3ml${so_ext}" - "${z3ml_bin}/libz3ml.a" - "${z3ml_bin}/z3ml.cma" - "${z3ml_bin}/z3ml.cmxa" - "${z3ml_bin}/z3ml.cmxs" + OUTPUT ${z3ml_bin}/dllz3ml${so_ext} + ${z3ml_bin}/libz3ml.a + ${z3ml_bin}/z3ml.cma + ${z3ml_bin}/z3ml.cmxa + ${z3ml_bin}/z3ml.cmxs COMMAND "${OCAMLFIND}" "ocamlmklib" ${ocamlmklib_flags} - "${z3ml_bin}/z3enums.cmo" - "${z3ml_bin}/z3native.cmo" - "${z3ml_bin}/z3native_stubs.o" - "${z3ml_bin}/z3.cmo" + "${z3ml_bin}/z3enums.cmo" + "${z3ml_bin}/z3native.cmo" + "${z3ml_bin}/z3native_stubs.o" + "${z3ml_bin}/z3.cmo" COMMAND "${OCAMLFIND}" "ocamlmklib" ${ocamlmklib_flags} - "${z3ml_bin}/z3enums.cmx" - "${z3ml_bin}/z3native.cmx" - "${z3ml_bin}/z3native_stubs.o" - "${z3ml_bin}/z3.cmx" + "${z3ml_bin}/z3enums.cmx" + "${z3ml_bin}/z3native.cmx" + "${z3ml_bin}/z3native_stubs.o" + "${z3ml_bin}/z3.cmx" COMMAND "${OCAMLFIND}" "ocamlopt" "-linkall" "-shared" - "-o" "${z3ml_bin}/z3ml.cmxs" - "-I" "${z3ml_bin}" - "${z3ml_bin}/z3ml.cmxa" + "-o" "${z3ml_bin}/z3ml.cmxs" + "-I" "${z3ml_bin}" + "${z3ml_bin}/z3ml.cmxa" DEPENDS - libz3_z3ml - ${z3ml_bin}/z3native_stubs.o - "${z3ml_bin}/z3enums.cmo" - "${z3ml_bin}/z3native.cmo" - "${z3ml_bin}/z3.cmo" - "${z3ml_bin}/z3enums.cmx" - "${z3ml_bin}/z3native.cmx" - "${z3ml_bin}/z3.cmx" + libz3_z3ml + ${z3ml_bin}/z3native_stubs.o + ${z3ml_bin}/z3enums.cmo + ${z3ml_bin}/z3native.cmo + ${z3ml_bin}/z3.cmo + ${z3ml_bin}/z3enums.cmx + ${z3ml_bin}/z3native.cmx + ${z3ml_bin}/z3.cmx COMMENT "Building z3ml.{cma,cmxa,cmxs}, dllz3ml${so_ext}, and libz3ml.a" VERBATIM) +############################################################################### +# Example +############################################################################### + +add_custom_command( + OUTPUT ${z3ml_bin}/ml_example.ml + COMMAND "${CMAKE_COMMAND}" "-E" + "copy" "${PROJECT_SOURCE_DIR}/examples/ml/ml_example.ml" "${z3ml_bin}/ml_example.ml" + DEPENDS ${PROJECT_SOURCE_DIR}/examples/ml/ml_example.ml + COMMENT "Copying ml_example.ml to build area") + +execute_process( + COMMAND ${OCAMLFIND} query zarith + OUTPUT_VARIABLE ocaml_pkg_zarith_path + OUTPUT_STRIP_TRAILING_WHITESPACE) + +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} + "-dllpath" ${ocaml_stublibs_path} + "${ocaml_pkg_zarith_path}/zarith.cma" + "${z3ml_bin}/z3ml.cma" + "${z3ml_bin}/ml_example.ml" + COMMAND + "ocamlrun" "${z3ml_bin}/ml_example${bc_ext}" + ">" "${z3ml_bin}/ml_example.bc.log" + DEPENDS + ${z3ml_bin}/z3ml.cma + ${z3ml_bin}/dllz3ml${so_ext} + ${z3ml_bin}/ml_example.ml + COMMENT "Testing build and run ml_example bytecode" + VERBATIM) + +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}" + "${z3ml_bin}/z3ml.cmxa" + "${z3ml_bin}/ml_example.ml" + COMMAND "${z3ml_bin}/ml_example${exe_ext}" + ">" "${z3ml_bin}/ml_example.log" + DEPENDS + ${z3ml_bin}/z3ml.cmxa + ${z3ml_bin}/dllz3ml${so_ext} + ${z3ml_bin}/ml_example.ml + COMMENT "Testing build and run ml_example natively" + VERBATIM) + +add_custom_target(build_ocaml_example + ALL + DEPENDS + ${z3ml_bin}/ml_example${bc_ext} + ${z3ml_bin}/ml_example${exe_ext} +) + +add_custom_target(build_z3_ocaml_bindings + ALL + DEPENDS + ${z3ml_bin}/z3ml.cma + ${z3ml_bin}/z3ml.cmxa + ${z3ml_bin}/z3ml.cmxs + ${z3ml_bin}/dllz3ml${so_ext} + ${z3ml_bin}/libz3ml.a + build_ocaml_example +) + +############################################################################### +# Install +############################################################################### + # Hacky: When the os is APPLE, a fix command will mutate `libz3.dylib` and `dlllibz3.so` inplace. # I don't know how to use conditional `COMMAND` nor specify a file dependency for itself # Renaming it and back seems a simple solution. @@ -224,92 +298,4 @@ add_custom_command( # COMMAND mv "${z3ml_bin}/dllz3ml.pre${so_ext}" "${z3ml_bin}/dllz3ml${so_ext}" # DEPENDS "${z3ml_bin}/dllz3ml.pre${so_ext}" # ) -# endif() - -############################################################################### -# Example -############################################################################### - -add_custom_command( - OUTPUT "${z3ml_bin}/ml_example.ml" - COMMAND "${CMAKE_COMMAND}" "-E" - "copy" "${PROJECT_SOURCE_DIR}/examples/ml/ml_example.ml" "${z3ml_bin}/ml_example.ml" - DEPENDS "${PROJECT_SOURCE_DIR}/examples/ml/ml_example.ml" - COMMENT "Copying ml_example.ml to build area") - -execute_process( - COMMAND ${OCAMLFIND} query zarith - OUTPUT_VARIABLE ocaml_pkg_zarith_path - OUTPUT_STRIP_TRAILING_WHITESPACE) - -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} - "-dllpath" ${ocaml_stublibs_path} - "${ocaml_pkg_zarith_path}/zarith.cma" - "${z3ml_bin}/z3ml.cma" - "${z3ml_bin}/ml_example.ml" - COMMAND - "ocamlrun" "${z3ml_bin}/ml_example${bc_ext}" - ">" "${z3ml_bin}/ml_example.bc.log" - DEPENDS - "${z3ml_bin}/z3ml.cma" - "${z3ml_bin}/dllz3ml${so_ext}" - "${z3ml_bin}/ml_example.ml" - COMMENT "Testing build and run ml_example bytecode" - VERBATIM) - -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}" - "${z3ml_bin}/z3ml.cmxa" - "${z3ml_bin}/ml_example.ml" - COMMAND "${z3ml_bin}/ml_example${exe_ext}" - ">" "${z3ml_bin}/ml_example.log" - DEPENDS - "${z3ml_bin}/z3ml.cmxa" - "${z3ml_bin}/dllz3ml${so_ext}" - "${z3ml_bin}/ml_example.ml" - COMMENT "Testing build and run ml_example natively" - VERBATIM) - -add_custom_target(build_ocaml_example - ALL - DEPENDS - "${z3ml_bin}/ml_example${bc_ext}" - "${z3ml_bin}/ml_example${exe_ext}" -) - -add_custom_target(build_z3_ocaml_bindings - ALL - DEPENDS - ${gen_z3enum} - "${z3ml_bin}/z3enums.mli" - ${Z3ml_native_stubs_c} - "${z3ml_bin}/z3native.ml" - "${z3ml_bin}/z3native.mli" - - "${z3ml_bin}/z3ml.cma" - "${z3ml_bin}/z3ml.cmxa" - "${z3ml_bin}/z3ml.cmxs" - "${z3ml_bin}/dllz3ml${so_ext}" - "${z3ml_bin}/libz3ml.a" - build_ocaml_example -) - -############################################################################### -# Install -############################################################################### +# endif() \ No newline at end of file