From c2efd3dc6d3250a33b838481de3853661cc87748 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Shiwei=20Weng=20=E7=BF=81=E5=A3=AB=E4=BC=9F?= Date: Fri, 27 Jun 2025 20:55:58 -0400 Subject: [PATCH] Update on building OCaml binding with CMake (#7698) * fix: add generating META for ocamlfind. * Patch macos. We need to keep the `@rpath` and use environment var to enable the test because we need to leave it to be fixed by package managers. * Trigger CI. * Debug. * Debug. * Debug. * Debug. * Debug. * Debug. * Hacky fix for ocaml building warning. * Fix typo and rename variables. --- .github/workflows/ocaml-all.yaml | 125 ------------------------------- .github/workflows/ocaml.yaml | 77 ++++++++++++------- src/api/ml/CMakeLists.txt | 74 +++++++----------- src/api/ml/META.in | 2 +- src/api/ml/z3.ml | 26 +++++-- src/api/ml/z3.mli | 4 +- 6 files changed, 100 insertions(+), 208 deletions(-) delete mode 100644 .github/workflows/ocaml-all.yaml diff --git a/.github/workflows/ocaml-all.yaml b/.github/workflows/ocaml-all.yaml deleted file mode 100644 index c225666c1..000000000 --- a/.github/workflows/ocaml-all.yaml +++ /dev/null @@ -1,125 +0,0 @@ -name: OCaml Binding CI (Ubuntu + macOS) - -on: - push: - branches: [ "**" ] - pull_request: - branches: [ "**" ] - -jobs: - build-test: - strategy: - matrix: - os: [ ubuntu-latest, macos-latest] - ocaml-version: ["5"] - fail-fast: false - runs-on: ${{ matrix.os }} - - steps: - - name: Checkout code - uses: actions/checkout@v4 - - # Cache ccache (shared across runs) - - name: Cache ccache - uses: actions/cache@v4 - with: - path: ~/.ccache - key: ${{ runner.os }}-ccache-${{ github.sha }} - restore-keys: | - ${{ runner.os }}-ccache- - - # Cache opam (compiler + packages) - - name: Cache opam - uses: actions/cache@v4 - with: - path: ~/.opam - key: ${{ runner.os }}-opam-${{ matrix.ocaml-version }}-${{ github.sha }} - restore-keys: | - ${{ runner.os }}-opam-${{ matrix.ocaml-version }}- - - # Setup OCaml via action - - uses: ocaml/setup-ocaml@v3 - with: - ocaml-compiler: ${{ matrix.ocaml-version }} - opam-disable-sandboxing: true - - # Platform-specific dependencies - - name: Install system dependencies (Ubuntu) - if: matrix.os == 'ubuntu-latest' - run: | - sudo apt-get update - sudo apt-get install -y \ - bubblewrap m4 libgmp-dev pkg-config ninja-build ccache - - - name: Install system dependencies (macOS) - if: matrix.os == 'macos-latest' - run: | - brew install gmp pkg-config ninja ccache - - - name: Install required opam packages - run: opam install -y ocamlfind zarith - - # Configure - - name: Configure with CMake - env: - RUNNER_OS: ${{ runner.os }} - CC: ${{ matrix.os == 'macos-latest' && 'ccache clang' || 'ccache gcc' }} - CXX: ${{ matrix.os == 'macos-latest' && 'ccache clang++' || 'ccache g++' }} - run: | - mkdir -p build - cd build - eval $(opam env) - echo "CC: $CC" - echo "CXX: $CXX" - echo "OCAMLFIND: $(which ocamlfind)" - echo "OCAMLC: $(which ocamlc)" - echo "OCAMLOPT: $(which ocamlopt)" - echo "OCAML_VERSION: $(ocamlc -version)" - echo "OCAMLLIB: $OCAMLLIB" - env | grep OCAML - cmake .. \ - -G Ninja \ - -DZ3_BUILD_LIBZ3_SHARED=ON \ - -DZ3_BUILD_OCAML_BINDINGS=ON \ - -DZ3_BUILD_JAVA_BINDINGS=OFF \ - -DZ3_BUILD_PYTHON_BINDINGS=OFF \ - -DZ3_BUILD_CLI=OFF \ - -DZ3_BUILD_TEST_EXECUTABLES=OFF \ - -DCMAKE_VERBOSE_MAKEFILE=TRUE - - - name: Build Z3 and OCaml bindings - run: | - ccache -z || true - eval $(opam env) - cd build - ninja build_z3_ocaml_bindings - ccache -s || true - - - name: Compile ml_example.byte - run: | - eval $(opam env) - ocamlfind ocamlc -o ml_example.byte \ - -package zarith \ - -linkpkg \ - -I build/src/api/ml \ - -dllpath build/src/api/ml \ - build/src/api/ml/z3ml.cma \ - examples/ml/ml_example.ml - - - name: Run ml_example.byte - run: | - eval $(opam env) - ocamlrun ./ml_example.byte - - - name: Compile ml_example (native) - run: | - eval $(opam env) - ocamlfind ocamlopt -o ml_example \ - -package zarith \ - -linkpkg \ - -I build/src/api/ml \ - build/src/api/ml/z3ml.cmxa \ - examples/ml/ml_example.ml - - - name: Run ml_example (native) - run: ./ml_example \ No newline at end of file diff --git a/.github/workflows/ocaml.yaml b/.github/workflows/ocaml.yaml index d8b64b992..5adc75a82 100644 --- a/.github/workflows/ocaml.yaml +++ b/.github/workflows/ocaml.yaml @@ -1,4 +1,4 @@ -name: OCaml Binding CI (Ubuntu) +name: OCaml Binding CI (Ubuntu + macOS) on: push: @@ -7,44 +7,74 @@ on: branches: [ "**" ] jobs: - build-test-ocaml: - runs-on: ubuntu-latest + build-test: + strategy: + matrix: + os: [ ubuntu-latest, macos-latest ] + ocaml-version: ["5"] + fail-fast: false + runs-on: ${{ matrix.os }} steps: - name: Checkout code uses: actions/checkout@v4 + # Cache ccache (shared across runs) - name: Cache ccache uses: actions/cache@v4 with: path: ~/.ccache - key: ${{ runner.os }}-ccache-${{ github.ref }} + key: ${{ runner.os }}-ccache-${{ github.sha }} restore-keys: | ${{ runner.os }}-ccache- - - name: Install system dependencies + # Cache opam (compiler + packages) + - name: Cache opam + uses: actions/cache@v4 + with: + path: ~/.opam + key: ${{ runner.os }}-opam-${{ matrix.ocaml-version }}-${{ github.sha }} + restore-keys: | + ${{ runner.os }}-opam-${{ matrix.ocaml-version }}- + + # Setup OCaml via action + - uses: ocaml/setup-ocaml@v3 + with: + ocaml-compiler: ${{ matrix.ocaml-version }} + opam-disable-sandboxing: true + + # Platform-specific dependencies + - name: Install system dependencies (Ubuntu) + if: matrix.os == 'ubuntu-latest' run: | sudo apt-get update sudo apt-get install -y \ - opam bubblewrap m4 \ - libgmp-dev pkg-config \ - ninja-build ccache + bubblewrap m4 libgmp-dev pkg-config ninja-build ccache - - name: Init opam (no sandbox, no default switch) + - name: Install system dependencies (macOS) + if: matrix.os == 'macos-latest' run: | - opam init --bare --no-setup --disable-sandboxing - opam switch create 5.3.0 - eval $(opam env) - opam install -y ocamlfind zarith - eval $(opam env) + brew install gmp pkg-config ninja ccache + - name: Install required opam packages + run: opam install -y ocamlfind zarith + + # Configure - name: Configure with CMake + env: + CC: ${{ matrix.os == 'macos-latest' && 'ccache clang' || 'ccache gcc' }} + CXX: ${{ matrix.os == 'macos-latest' && 'ccache clang++' || 'ccache g++' }} run: | - eval $(opam env) - export CC="ccache gcc" - export CXX="ccache g++" mkdir -p build cd build + eval $(opam env) + echo "CC: $CC" + echo "CXX: $CXX" + echo "OCAMLFIND: $(which ocamlfind)" + echo "OCAMLC: $(which ocamlc)" + echo "OCAMLOPT: $(which ocamlopt)" + echo "OCAML_VERSION: $(ocamlc -version)" + echo "OCAMLLIB: $OCAMLLIB" cmake .. \ -G Ninja \ -DZ3_BUILD_LIBZ3_SHARED=ON \ @@ -57,19 +87,15 @@ jobs: - name: Build Z3 and OCaml bindings run: | + ccache -z || true eval $(opam env) - export CC="ccache gcc" - export CXX="ccache g++" - ocamlc -version - ccache -z # reset stats cd build ninja build_z3_ocaml_bindings - ccache -s # show stats + ccache -s || true - name: Compile ml_example.byte run: | eval $(opam env) - ocamlc -version ocamlfind ocamlc -o ml_example.byte \ -package zarith \ -linkpkg \ @@ -81,12 +107,12 @@ jobs: - name: Run ml_example.byte run: | eval $(opam env) + export DYLD_LIBRARY_PATH=$(pwd)/build ocamlrun ./ml_example.byte - name: Compile ml_example (native) run: | eval $(opam env) - ocamlopt -version ocamlfind ocamlopt -o ml_example \ -package zarith \ -linkpkg \ @@ -96,4 +122,5 @@ jobs: - name: Run ml_example (native) run: | - ./ml_example + export DYLD_LIBRARY_PATH=$(pwd)/build + ./ml_example \ No newline at end of file diff --git a/src/api/ml/CMakeLists.txt b/src/api/ml/CMakeLists.txt index e3f3168ad..d4e781e6e 100644 --- a/src/api/ml/CMakeLists.txt +++ b/src/api/ml/CMakeLists.txt @@ -7,14 +7,14 @@ set(bc_ext ".byte") set(z3ml_src ${CMAKE_CURRENT_SOURCE_DIR}) set(z3ml_bin ${CMAKE_CURRENT_BINARY_DIR}) -if (Z3_BUILD_OCAML_EXTERNAL_LIBZ3) - add_custom_target(libz3_z3ml +if (Z3_EXTERNAL_LIBZ3) + add_custom_target(libz3_ocaml ALL - DEPENDS ${Z3_BUILD_OCAML_EXTERNAL_LIBZ3}/libz3${so_ext} + DEPENDS ${Z3_EXTERNAL_LIBZ3}/libz3${so_ext} ) - set(libz3_path ${Z3_BUILD_OCAML_EXTERNAL_LIBZ3}) + set(libz3_path ${Z3_EXTERNAL_LIBZ3}) else() - add_custom_target(libz3_z3ml + add_custom_target(libz3_ocaml ALL DEPENDS libz3 ) @@ -60,14 +60,6 @@ add_custom_command( set(z3ml_common_flags "-package" "zarith" "-I" "${z3ml_bin}") - # add_custom_command( -# 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 -# COMMENT "Copying z3.ml and z3.mli to build area") # z3native_stubs.c depends on nothing execute_process( @@ -136,12 +128,6 @@ add_custom_command( 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" COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} "-o" "${z3ml_bin}/z3.cmi" "-c" "${z3ml_src}/z3.mli" @@ -153,8 +139,6 @@ COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags} "-c" "${z3ml_src}/z3.ml" DEPENDS ${z3ml_bin}/z3enums.cmo ${z3ml_bin}/z3native.cmo - # ${z3ml_bin}/z3.ml - # ${z3ml_bin}/z3.mli ${z3ml_src}/z3.ml ${z3ml_src}/z3.mli COMMENT "Building z3.cmo" @@ -216,7 +200,7 @@ add_custom_command( "-I" "${z3ml_bin}" "${z3ml_bin}/z3ml.cmxa" DEPENDS - libz3_z3ml + libz3_ocaml ${z3ml_bin}/z3native_stubs.o ${z3ml_bin}/z3enums.cmo ${z3ml_bin}/z3native.cmo @@ -227,6 +211,23 @@ add_custom_command( COMMENT "Building z3ml.{cma,cmxa,cmxs}, dllz3ml.so, and libz3ml.a" VERBATIM) +set(META_INPUT_FILE "${z3ml_src}/META.in") +set(META_OUTPUT_FILE "${z3ml_bin}/META") + +set(Z3_VERSION_STRING "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}") + +configure_file( + "${META_INPUT_FILE}" + "${META_OUTPUT_FILE}" + @ONLY +) + +add_custom_target( + generate_meta ALL + DEPENDS "${META_OUTPUT_FILE}" + COMMENT "Generating META file for OCaml bindings" +) + ############################################################################### # Example ############################################################################### @@ -235,29 +236,6 @@ execute_process( COMMAND ${OCAMLFIND} query zarith OUTPUT_VARIABLE ocaml_pkg_zarith_path OUTPUT_STRIP_TRAILING_WHITESPACE) - -# Always define patch_z3ml_dylib for dependency consistency -if(APPLE) - add_custom_command( - OUTPUT ${z3ml_bin}/patched_dllz3ml - COMMAND install_name_tool -id "$" "$" - COMMAND install_name_tool -change "@rpath/libz3.${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.dylib" "$" "${z3ml_bin}/dllz3ml.so" - COMMAND touch ${z3ml_bin}/patched_dllz3ml - DEPENDS ${z3ml_bin}/dllz3ml.so - COMMENT "Patch install name and reference for macOS" - VERBATIM - ) -else() - add_custom_command( - OUTPUT ${z3ml_bin}/patched_dllz3ml - COMMAND ${CMAKE_COMMAND} -E touch ${z3ml_bin}/patched_dllz3ml - COMMENT "Dummy patch target for non-macOS" - VERBATIM - ) -endif() - -add_custom_target(patch_z3ml_dylib ALL - DEPENDS ${z3ml_bin}/patched_dllz3ml) add_custom_target(build_z3_ocaml_bindings ALL @@ -267,7 +245,7 @@ add_custom_target(build_z3_ocaml_bindings ${z3ml_bin}/z3ml.cmxs ${z3ml_bin}/dllz3ml.so ${z3ml_bin}/libz3ml.a - patch_z3ml_dylib + ${META_OUTPUT_FILE} ) # test @@ -284,7 +262,7 @@ add_custom_command( -dllpath "${z3ml_bin}" "${z3ml_bin}/z3ml.cma" "${z3ml_example_src}" - COMMAND ocamlrun "${z3ml_bin}/ml_example.byte" > "${z3ml_bin}/ml_example.bc.log" + COMMAND env DYLD_LIBRARY_PATH=${PROJECT_BINARY_DIR} ocamlrun ${z3ml_bin}/ml_example.byte > ${z3ml_bin}/ml_example.bc.log COMMENT "Run OCaml bytecode example" VERBATIM ) @@ -298,7 +276,7 @@ add_custom_command( -I "${z3ml_bin}" "${z3ml_bin}/z3ml.cmxa" "${z3ml_example_src}" - COMMAND "${z3ml_bin}/ml_example" > "${z3ml_bin}/ml_example.log" + COMMAND env DYLD_LIBRARY_PATH=${PROJECT_BINARY_DIR} ${z3ml_bin}/ml_example > ${z3ml_bin}/ml_example.log COMMENT "Run OCaml native example" VERBATIM ) diff --git a/src/api/ml/META.in b/src/api/ml/META.in index ad27e6b0b..edeaa7f0c 100644 --- a/src/api/ml/META.in +++ b/src/api/ml/META.in @@ -1,5 +1,5 @@ # META file for the "z3" package: -version = "@VERSION@" +version = "@Z3_VERSION_STRING@" description = "Z3 Theorem Prover (OCaml API)" requires = "zarith threads" archive(byte) = "z3ml.cma" diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 8f46e551c..4d5238957 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -239,11 +239,13 @@ sig type parameter = P_Int of int | P_Dbl of float + | P_Rat of string | P_Sym of Symbol.symbol | P_Srt of Sort.sort | P_Ast of AST.ast | P_Fdl of func_decl - | P_Rat of string + | P_Internal of string + | P_ZStr of string val get_kind : parameter -> Z3enums.parameter_kind val get_int : parameter -> int @@ -284,20 +286,25 @@ end = struct type parameter = | P_Int of int | P_Dbl of float + | P_Rat of string | P_Sym of Symbol.symbol | P_Srt of Sort.sort | P_Ast of AST.ast | P_Fdl of func_decl - | P_Rat of string + | P_Internal of string + | P_ZStr of string let get_kind = function | P_Int _ -> PARAMETER_INT | P_Dbl _ -> PARAMETER_DOUBLE + | P_Rat _ -> PARAMETER_RATIONAL | P_Sym _ -> PARAMETER_SYMBOL | P_Srt _ -> PARAMETER_SORT | P_Ast _ -> PARAMETER_AST | P_Fdl _ -> PARAMETER_FUNC_DECL - | P_Rat _ -> PARAMETER_RATIONAL + | P_Internal _ -> PARAMETER_INTERNAL + | P_ZStr _ -> PARAMETER_ZSTRING + let get_int = function | P_Int x -> x @@ -307,6 +314,10 @@ end = struct | P_Dbl x -> x | _ -> raise (Error "parameter is not a float") + let get_rational = function + | P_Rat x -> x + | _ -> raise (Error "parameter is not a rational string") + let get_symbol = function | P_Sym x -> x | _ -> raise (Error "parameter is not a symbol") @@ -322,10 +333,6 @@ end = struct let get_func_decl = function | P_Fdl x -> x | _ -> raise (Error "parameter is not a func_decl") - - let get_rational = function - | P_Rat x -> x - | _ -> raise (Error "parameter is not a rational string") end let mk_func_decl (ctx:context) (name:Symbol.symbol) (domain:Sort.sort list) (range:Sort.sort) = @@ -378,11 +385,14 @@ end = struct match parameter_kind_of_int (Z3native.get_decl_parameter_kind (gc x) x i) with | PARAMETER_INT -> Parameter.P_Int (Z3native.get_decl_int_parameter (gc x) x i) | PARAMETER_DOUBLE -> Parameter.P_Dbl (Z3native.get_decl_double_parameter (gc x) x i) + | PARAMETER_RATIONAL -> Parameter.P_Rat (Z3native.get_decl_rational_parameter (gc x) x i) | PARAMETER_SYMBOL-> Parameter.P_Sym (Z3native.get_decl_symbol_parameter (gc x) x i) | PARAMETER_SORT -> Parameter.P_Srt (Z3native.get_decl_sort_parameter (gc x) x i) | PARAMETER_AST -> Parameter.P_Ast (Z3native.get_decl_ast_parameter (gc x) x i) | PARAMETER_FUNC_DECL -> Parameter.P_Fdl (Z3native.get_decl_func_decl_parameter (gc x) x i) - | PARAMETER_RATIONAL -> Parameter.P_Rat (Z3native.get_decl_rational_parameter (gc x) x i) + | PARAMETER_INTERNAL -> Parameter.P_Internal ("interal parameter") + | PARAMETER_ZSTRING -> Parameter.P_ZStr ("internal string") + in List.init n f diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index b7a74049f..7afc01918 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -304,11 +304,13 @@ sig type parameter = P_Int of int | P_Dbl of float + | P_Rat of string | P_Sym of Symbol.symbol | P_Srt of Sort.sort | P_Ast of AST.ast | P_Fdl of func_decl - | P_Rat of string + | P_Internal of string + | P_ZStr of string (** The kind of the parameter. *) val get_kind : parameter -> Z3enums.parameter_kind