mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 01:25:31 +00:00
f7aec02503
* Update doc for `mk_context`. * Migrating to cmake. * Migrating to cmake. It builds both internal or external libz3. * Start to work on platform-specific problem. * Messy notes. * debug. * Cleanup a bit. * Fixing shared lib extension. * Minor. * Resume working on this PR. * Remove including `AddOCaml`. * Keep `z3.ml` and `z3.mli` in the src but specify the generated file in the bin. * Keep `ml_example.ml` in the src. * Try github action for ocaml. * Add workflow using matrix. * Fix mac linking once more. * Bypass @rpath in building sanity check.
400 lines
10 KiB
Makefile
400 lines
10 KiB
Makefile
# ${PROJECT_SOURCE_DIR}: /vendor/z3
|
|
# ${PROJECT_BINARY_DIR}: /vendor/z3/build
|
|
# ${CMAKE_CURRENT_SOURCE_DIR}: /vendor/z3/src/api/ml
|
|
# ${CMAKE_CURRENT_BINARY_DIR}: /vendor/z3/build/src/api/ml
|
|
|
|
# TODO: add `-bin-annot` to more `ocamlc`
|
|
# Question: who will set `CAMLORIGIN`
|
|
# - -dllpath $$CAMLORIGIN/../.. \
|
|
# Q: is `ocamlmklib -ldopt -Lfoo` the same as `ocamlmklib -Lfoo`
|
|
# it doesn't looks right (item 4)
|
|
# https://www.ocaml.org/manual/5.2/runtime.html#s:ocamlrun-dllpath
|
|
#
|
|
# if external libz3 is given, no files should be build
|
|
#
|
|
# find_program(OCAMLFIND
|
|
# NAMES ocamlfind)
|
|
# 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``
|
|
|
|
# set(z3ml_generated_files
|
|
# "${z3ml_bin}/z3native.ml"
|
|
# "${z3ml_bin}/z3native_stubs.c"
|
|
# "${z3ml_enums_ml}"
|
|
# )
|
|
|
|
# add_custom_target(ocaml_generated DEPENDS
|
|
# ${z3ml_generated_files}
|
|
# )
|
|
|
|
# add_custom_command(
|
|
# OUTPUT "${z3ml_bin}/z3enums.mli"
|
|
# COMMAND "${OCAMLFIND}" "ocamlc"
|
|
# "-package" "zarith"
|
|
# "-i"
|
|
# "-I" "${z3ml_bin}"
|
|
# "-c" "${z3ml_bin}/z3enums.ml"
|
|
# ">" "${z3ml_bin}/z3enums.mli"
|
|
# DEPENDS "${z3ml_enums_ml}"
|
|
# COMMENT "Building z3enums.mli"
|
|
# VERBATIM)
|
|
|
|
# "-ldopt"
|
|
# "-ccopt" "-L\\$CAMLORIGIN/../.."
|
|
# "-ccopt" "-Wl,-rpath,\\$CAMLORIGIN/../.."
|
|
|
|
# add_custom_command(
|
|
# OUTPUT "${z3ml_bin}/z3native.cmx"
|
|
# COMMAND "${OCAMLFIND}" "ocamlopt"
|
|
# "-package" "zarith"
|
|
# "-I" "${z3ml_bin}"
|
|
# "-c" "${z3ml_bin}/z3native.ml"
|
|
# DEPENDS "${z3ml_bin}/z3enums.cmo"
|
|
# "${z3ml_bin}/z3native.mli"
|
|
# "${z3ml_bin}/z3native.cmi"
|
|
# "${z3ml_bin}/z3native.ml"
|
|
# COMMENT "Building z3native.cmx"
|
|
# VERBATIM)
|
|
|
|
# add_custom_command(
|
|
# OUTPUT "${z3ml_bin}/z3enums.cmo"
|
|
# COMMAND "${OCAMLFIND}" "ocamlc"
|
|
# "-package" "zarith"
|
|
# "-I" "${z3ml_bin}"
|
|
# "-c" "${z3ml_bin}/z3enums.ml"
|
|
# DEPENDS "${z3ml_enums_ml}"
|
|
# COMMENT "Building z3enums.cmo"
|
|
# VERBATIM)
|
|
|
|
# add_custom_command(
|
|
# OUTPUT "${z3ml_bin}/z3native.mli"
|
|
# COMMAND "${OCAMLFIND}" "ocamlc"
|
|
# "-package" "zarith"
|
|
# "-i"
|
|
# "-I" "${z3ml_bin}"
|
|
# "-c" "${z3ml_bin}/z3native.ml"
|
|
# ">" "${z3ml_bin}/z3native.mli"
|
|
# DEPENDS "${z3ml_enums_ml}"
|
|
# "${z3ml_bin}/z3enums.cmo"
|
|
# "${z3ml_bin}/z3native.ml"
|
|
# COMMENT "Building z3native.mli"
|
|
# VERBATIM)
|
|
|
|
# add_custom_command(
|
|
# OUTPUT "${z3ml_bin}/z3.cmx"
|
|
# 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"
|
|
# "${z3ml_bin}/z3.cmi"
|
|
# COMMENT "Building z3.cmx"
|
|
# VERBATIM)
|
|
|
|
# add_custom_command(
|
|
# OUTPUT "${z3ml_bin}/z3ml.cmxa"
|
|
# COMMAND "${OCAMLFIND}" "ocamlmklib"
|
|
# "-o" z3ml
|
|
# ${ocamlmklib_flags}
|
|
# "-I" "${z3ml_bin}"
|
|
# "${z3ml_bin}/z3enums.cmx"
|
|
# "${z3ml_bin}/z3native.cmx"
|
|
# "${z3ml_bin}/z3native_stubs.o"
|
|
# "${z3ml_bin}/z3.cmx"
|
|
# DEPENDS
|
|
# libz3
|
|
# "${z3ml_bin}/z3enums.cmx"
|
|
# "${z3ml_bin}/z3native.cmx"
|
|
# "${z3ml_bin}/z3native_stubs.o"
|
|
# "${z3ml_bin}/z3.cmx"
|
|
# COMMENT "Building OCaml library ${name}"
|
|
# VERBATIM)
|
|
# add_custom_command(
|
|
# OUTPUT "${z3ml_bin}/z3ml.cmxs"
|
|
# COMMAND "${OCAMLFIND}" "ocamlopt" "-linkall" "-shared"
|
|
# "-o" "${z3ml_bin}/z3ml.cmxs"
|
|
# "-I" "."
|
|
# "-I" "${z3ml_bin}"
|
|
# "${z3ml_bin}/z3ml.cmxa"
|
|
# DEPENDS
|
|
# "${z3ml_bin}/z3ml.cmxa"
|
|
# COMMENT "Building OCaml library ${name}"
|
|
# VERBATIM)
|
|
|
|
# "${z3ml_bin}/z3enums.cmi"
|
|
|
|
ML_LIB=/home/ex/.opam/5.2.0/lib
|
|
ML_LIB=/Users/ex/.opam/5.2.0/lib
|
|
ROOT=$$(pwd)
|
|
MY_Z3=/home/ex/my_z3
|
|
MY_Z3=/Users/ex/code/tmp/my-z3
|
|
|
|
ml0:
|
|
mkdir -p build
|
|
cd build && cmake -G "Ninja" \
|
|
-DZ3_BUILD_LIBZ3_SHARED=TRUE \
|
|
-DZ3_BUILD_OCAML_BINDINGS=TRUE \
|
|
../
|
|
|
|
# -DGRAPHVIZ_EXECUTABLES=FALSE \
|
|
# -DGRAPHVIZ_INTERFACE_LIBS=FALSE \
|
|
# --graphviz=deps.dot \
|
|
|
|
ml-inner-mk:
|
|
mkdir -p build
|
|
cd build && cmake \
|
|
-DCMAKE_VERBOSE_MAKEFILE=TRUE \
|
|
-DZ3_BUILD_LIBZ3_SHARED=TRUE \
|
|
-DZ3_BUILD_OCAML_BINDINGS=TRUE \
|
|
-DZ3_BUILD_PYTHON_BINDINGS=TRUE \
|
|
--debug-trycompile \
|
|
../
|
|
|
|
ml-mk:
|
|
mkdir -p build
|
|
cd build && cmake \
|
|
-DCMAKE_VERBOSE_MAKEFILE=TRUE \
|
|
-DZ3_BUILD_LIBZ3_SHARED=TRUE \
|
|
-DZ3_BUILD_OCAML_BINDINGS=TRUE \
|
|
-DZ3_BUILD_OCAML_EXTERNAL_LIBZ3=$(MY_Z3) \
|
|
--debug-trycompile \
|
|
../
|
|
|
|
ml-inner:
|
|
mkdir -p build
|
|
cd build && cmake \
|
|
-G "Ninja" \
|
|
-DCMAKE_VERBOSE_MAKEFILE=TRUE \
|
|
-DZ3_BUILD_LIBZ3_SHARED=TRUE \
|
|
-DZ3_BUILD_OCAML_BINDINGS=TRUE \
|
|
--debug-trycompile \
|
|
../
|
|
|
|
ml:
|
|
mkdir -p build
|
|
cd build && cmake \
|
|
-G "Ninja" \
|
|
-DCMAKE_VERBOSE_MAKEFILE=TRUE \
|
|
-DZ3_BUILD_LIBZ3_SHARED=TRUE \
|
|
-DZ3_BUILD_OCAML_BINDINGS=TRUE \
|
|
--debug-trycompile \
|
|
../
|
|
|
|
# -DZ3_BUILD_OCAML_EXTERNAL_LIBZ3=$(MY_Z3) \
|
|
# -DZ3_USE_LIB_GMP=TRUE \
|
|
|
|
# LD_LIBRARY_PATH=build ./build/src/api/ml/ml_example
|
|
|
|
build-all:
|
|
cd build && make -j16
|
|
|
|
build-mk:
|
|
cd build && make -j16 build_z3_ocaml_bindings
|
|
.PHONY:build
|
|
|
|
build-nj:
|
|
cd build && ninja
|
|
.PHONY:build-nj
|
|
|
|
build:
|
|
cd build && ninja build_z3_ocaml_bindings
|
|
.PHONY:build
|
|
|
|
dot:
|
|
cd build && dot -Tpng -o deps.png deps.dot
|
|
|
|
clean:
|
|
rm -rf build
|
|
|
|
MKLIB_FLAGS = \
|
|
ocamlfind ocamlmklib \
|
|
-ocamlcflags -bin-annot \
|
|
-package zarith \
|
|
-lz3 -lstdc++ -lpthread\
|
|
-lgmp \
|
|
-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
|
|
|
|
om:
|
|
$(MKLIB_FLAGS) \
|
|
build/src/api/ml/z3enums.cmo \
|
|
build/src/api/ml/z3native.cmo \
|
|
build/src/api/ml/z3native_stubs.o \
|
|
build/src/api/ml/z3.cmo
|
|
|
|
$(MKLIB_FLAGS) \
|
|
build/src/api/ml/z3enums.cmx \
|
|
build/src/api/ml/z3native.cmx \
|
|
build/src/api/ml/z3native_stubs.o \
|
|
build/src/api/ml/z3.cmx
|
|
|
|
# why?
|
|
# DEPENDS "${z3ml_bin}/z3enums.cmo"
|
|
# -I +threads \
|
|
|
|
or1:
|
|
ocamlfind ocamlc -verbose \
|
|
-o ml_example.byte \
|
|
-package zarith \
|
|
-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 $(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 \
|
|
-o ml_example \
|
|
-package zarith \
|
|
-linkpkg \
|
|
-I $(ROOT)/build/src/api/ml \
|
|
z3ml.cmxa \
|
|
$(ROOT)/build/src/api/ml/ml_example.ml
|
|
|
|
oc2:
|
|
./ml_example
|
|
|
|
# must have
|
|
# $(ML_LIB)/zarith/zarith.cma
|
|
# -I $(ROOT)/build/src/api/ml
|
|
|
|
# can be removed
|
|
# -cclib "-lstdc++ -lz3"
|
|
# -cclib "-L. -L$(ML_LIB)/stublibs -L$(ML_LIB)/zarith "
|
|
# -L$(ROOT)/build
|
|
# -package zarith
|
|
# -linkpkg
|
|
# -lpthread
|
|
# -package z3
|
|
# -I $(ML_LIB)/zarith
|
|
|
|
# must not have
|
|
# -custom
|
|
|
|
# -o $(ROOT)/build/src/api/ml/ml_example.byte
|
|
|
|
# CAML_LD_LIBRARY_PATH=$(ML_LIB)/stublibs:$(ROOT)/build:$(ROOT)/build/src/api/ml:$(ML_LIB)/zarith
|
|
|
|
or3:
|
|
ocamlrun -I $(ML_LIB)/zarith -I $(ML_LIB)/stublibs -I $(ML_LIB)/zarith ml_example.byte
|
|
|
|
# -I $(ML_LIB)/zarith
|
|
# -I $(ML_LIB)/stublibs
|
|
# -I $(ROOT)/build
|
|
# -I $(ROOT)/build/src/api/ml
|
|
# -t -b
|
|
|
|
|
|
# -cclib "-L. -lpthread -lstdc++ -lz3"
|
|
|
|
# set (cc_flags "\"-L. -lpthread -lstdc++ -lz3\"")
|
|
#"LD_LIBRARY_PATH=${PROJECT_BINARY_DIR}"
|
|
|
|
# Link libz3 into the python directory so bindings work out of the box
|
|
# add_custom_command(OUTPUT "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
|
|
# COMMAND "${CMAKE_COMMAND}" "-E" "${LINK_COMMAND}"
|
|
# "${PROJECT_BINARY_DIR}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
|
|
# "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
|
|
# DEPENDS libz3
|
|
# COMMENT "Linking libz3 into python directory"
|
|
# )
|
|
|
|
# add_ocaml_library(z3ml
|
|
# OCAML z3enums z3native z3
|
|
# # OCAMLDEP llvm
|
|
# PKG zarith
|
|
# C z3native_stubs
|
|
# CFLAGS "-I${Z3_C_API_PATH} -I${CMAKE_CURRENT_SOURCE_DIR} -I\$\(ocamlfind ocamlc -where\)"
|
|
# GEN "${OCAML_GENERATED_FILES}"
|
|
# # -I${CMAKE_CURRENT_SOURCE_DIR}/../llvm
|
|
# # LLVM IRReader)
|
|
# )
|
|
|
|
|
|
# set(z3_c_api_path "${PROJECT_SOURCE_DIR}/src/api")
|
|
# target_sources(z3ml PRIVATE
|
|
# z3native_stubs.h
|
|
# ${z3_c_api_path})
|
|
|
|
|
|
# message(heads "--${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}")
|
|
# message(extra deps "--${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}")
|
|
|
|
# add_custom_target(z3natives_stubs.c DEPENDS "${Z3_OCAML_NATIVE_STUB_PRE_FILE}")
|
|
# target_sources(ocaml_z3
|
|
# PRIVATE ${Z3_OCAML_NATIVE_FILE} ${Z3_OCAML_NATIVE_STUB_FILE})
|
|
|
|
# target_include_directories(ocaml_z3
|
|
# PUBLIC ${CMAKE_CURRENT_BINARY_DIR}
|
|
# )
|
|
|
|
# add_custom_target (LibCoreBC DEPENDS libcore.bc)
|
|
|
|
# target_sources(src/api/ml/z3natives_stubs.c
|
|
# PUBLIC Z3_OCAML_NATIVE_STUB_FILE)
|
|
|
|
# add_custom_target(${Z3_OCAML_NATIVE_STUB_FILE} DEPENDS
|
|
# ${Z3_OCAML_NATIVE_STUB_PRE_FILE})
|
|
|
|
# target_precompile_headers(
|
|
# ocaml_z3 PRIVATE
|
|
# z3native_stubs.h
|
|
# )
|
|
|
|
# target_sources(ocaml_z3 PRIVATE
|
|
# "${PROJECT_SOURCE_DIR}/src/api/ml/z3native.ml"
|
|
# "${PROJECT_SOURCE_DIR}/src/api/ml/z3native_stubs.c")
|
|
|
|
# add_dependencies(ocaml_z3
|
|
# "${PROJECT_SOURCE_DIR}/src/api"
|
|
# "${PROJECT_BINARY_DIR}/src/api"
|
|
# )
|
|
|
|
# find_package(OCaml)
|
|
# message("DDDebug ${OCAMLFIND}")
|
|
# message("DDDebug ${pkg}")
|
|
# find_ocamlfind_package(ctypes)
|
|
# # find_ocamlfind_package("nonexist")
|
|
# message(small " ${HAVE_OCAML_ctype}")
|
|
# message(caps " ${HAVE_OCAML_CTYPES}")
|
|
# message(small " ${OCAML_ctype_VERSION}")
|
|
# message(caps " ${OCAML_CTYPES_VERSION}")
|
|
# find_package(ocaml REQUIRED)
|
|
|
|
# add_custom_target(ocaml_post_z3enums DEPENDS
|
|
# "${CMAKE_CURRENT_BINARY_DIR}/z3enums.ml"
|
|
# "${CMAKE_CURRENT_BINARY_DIR}/z3enums.mli"
|
|
# "${CMAKE_CURRENT_BINARY_DIR}/z3enums.cmo"
|
|
# "${CMAKE_CURRENT_BINARY_DIR}/z3enums.cmx"
|
|
# )
|
|
# add_custom_target(z3.ml DEPENDS
|
|
# ocaml_post_z3enums
|
|
# )
|
|
# add_custom_target(z3native.ml DEPENDS
|
|
# ocaml_post_z3enums
|
|
# )
|