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

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

.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:
+  build-test:
-    runs-on: ubuntu-latest
+    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 \
+            bubblewrap m4 libgmp-dev pkg-config ninja-build ccache
-            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
+          brew install gmp pkg-config ninja ccache
-          opam switch create 5.3.0
-          eval $(opam env)
-          opam install -y ocamlfind zarith
-          eval $(opam env)
 
+      - 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

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)
+if (Z3_EXTERNAL_LIBZ3)
-  add_custom_target(libz3_z3ml
+  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 "$<TARGET_FILE:libz3>" "$<TARGET_FILE:libz3>"
-    COMMAND install_name_tool -change "@rpath/libz3.${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.dylib" "$<TARGET_FILE:libz3>" "${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
 )

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"

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
 

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