Add workflow using matrix.

.github/workflows/ocaml-all.yaml

@@ -0,0 +1,243 @@
+name: OCaml Binding CI (Ubuntu + macOS)
+
+on:
+  push:
+    branches: [ "**" ]
+  pull_request:
+    branches: [ "**" ]
+
+jobs:
+  no-matrix:
+    name: No matrix job
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Setup OCaml (no matrix)
+        uses: ocaml/setup-ocaml@v3
+        with:
+          ocaml-compiler: 5.3.0
+          opam-disable-sandboxing: true
+
+      - name: Debug PATH and ENV (no matrix)
+        run: |
+          echo "GITHUB_ENV:"
+          cat $GITHUB_ENV || echo "❌ Not found"
+
+          echo ""
+          echo "GITHUB_PATH:"
+          cat $GITHUB_PATH || echo "❌ Not found"
+
+          echo "PATH:"
+          echo "$PATH" | tr ':' '\n'
+          echo ""
+          echo "which ocamlc:"
+          which ocamlc || echo "❌ Not found"
+          echo ""
+          echo "OPAM_SWITCH_PREFIX: $OPAM_SWITCH_PREFIX"
+
+  build-test:
+    strategy:
+      matrix:
+        # ubuntu-latest,
+        os: [ 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
+          
+      - name: Debug after setup-ocaml
+        run: |
+          echo "GITHUB_ENV:"
+          cat $GITHUB_ENV || echo "❌ Not found"
+
+          echo ""
+          echo "GITHUB_PATH:"
+          cat $GITHUB_PATH || echo "❌ Not found"
+
+          echo "PATH after setup:"
+          echo "$PATH" | tr ':' '\n'
+      
+          echo ""
+          echo "which ocamlfind:"
+          which ocamlfind || echo "❌ Not found"
+      
+          echo ""
+          echo "OPAM_SWITCH_PREFIX: $OPAM_SWITCH_PREFIX"
+
+      # 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
+
+      - name: 🔍 Debug ocamlfind + ocamlc.opt issue
+        run: |
+          set -e  # fail on error
+
+          eval $(opam env)
+      
+          echo "🔎 ocamlc: $(which ocamlc)"
+          echo "🔎 ocamlopt: $(which ocamlopt)"
+          echo "🔎 ocamlfind: $(which ocamlfind)"
+          echo "🔎 All ocamlfind on path:"
+          which -a ocamlfind
+      
+          echo ""
+          echo "📄 Writing test.ml"
+          echo 'let () = print_endline "Hello from OCaml"' > test.ml
+      
+          echo ""
+          echo "🧪 ocamlc compile"
+          ocamlc test.ml -o test_bytecode
+      
+          echo ""
+          echo "🧪 ocamlopt compile"
+          ocamlopt test.ml -o test_native
+      
+          echo ""
+          echo "🧪 ocamlfind ocamlc compile"
+          ocamlfind ocamlc -package zarith -linkpkg test.ml -o test_bytecode_find
+      
+          echo ""
+          echo "🧪 ocamlfind ocamlopt compile"
+          ocamlfind ocamlopt -package zarith -linkpkg test.ml -o test_native_find
+      
+          # echo ""
+          # echo "🧪 FULLPATH ocamlfind ocamlc compile"
+          # /home/runner/work/z3/z3/_opam/bin/ocamlfind ocamlc -package zarith -linkpkg test.ml -o test_bytecode_full
+      
+          # echo ""
+          # echo "🧪 FULLPATH ocamlfind ocamlopt compile"
+          # /home/runner/work/z3/z3/_opam/bin/ocamlfind ocamlopt -package zarith -linkpkg test.ml -o test_native_full
+      
+          echo ""
+          echo "✅ All compiles passed."
+
+      - name: 🧪 Debug OPAM + GITHUB_PATH setup
+        run: |
+          echo "🔍 PATH at this step:"
+          echo "$PATH" | tr ':' '\n'
+      
+          echo ""
+          echo "📁 Listing \$GITHUB_PATH file (if exists):"
+          if [ -f "$GITHUB_PATH" ]; then
+            cat "$GITHUB_PATH"
+          else
+            echo "❌ GITHUB_PATH file does not exist at $GITHUB_PATH"
+          fi
+      
+          echo ""
+          echo "📦 OPAM_SWITCH_PREFIX = $OPAM_SWITCH_PREFIX"
+          echo ""
+          echo "📂 Listing contents of \$OPAM_SWITCH_PREFIX/bin:"
+          ls -al "$OPAM_SWITCH_PREFIX/bin" || echo "❌ Directory does not exist"
+      
+          echo ""
+          echo "🔍 Check if PATH includes _opam/bin:"
+          echo "$PATH" | grep "_opam/bin" || echo "❌ _opam/bin NOT in PATH"
+      
+          echo ""
+          echo "✅ Done."
+        
+      # 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

@@ -63,7 +63,7 @@ jobs:
           ocamlc -version
           ccache -z  # reset stats
           cd build
-          ninja -j$(nproc) build_z3_ocaml_bindings
+          ninja build_z3_ocaml_bindings
           ccache -s  # show stats
 
       - name: Compile ml_example.byte

src/api/ml/CMakeLists.txt

@@ -60,6 +60,15 @@ 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(
   COMMAND ${OCAMLFIND} ocamlc "-where"
@@ -78,6 +87,9 @@ add_custom_command(
   COMMENT "Building z3native_stubs.o"
   VERBATIM)
 
+message(STATUS "PATH: $ENV{PATH}")
+message(STATUS "OCAMLFIND: $ENV{OCAMLFIND}")
+
 # z3enum.ml depends on nothing
 add_custom_command(
   OUTPUT ${z3ml_bin}/z3enums.mli
@@ -124,6 +136,12 @@ 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"
@@ -135,6 +153,8 @@ 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"
@@ -212,63 +232,33 @@ add_custom_command(
 # Example
 ###############################################################################
 
-
 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 "@loader_path/libz3.dylib" "${CMAKE_BINARY_DIR}/libz3.dylib"
+    COMMAND install_name_tool -change libz3.dylib "@loader_path/libz3.dylib" "${z3ml_bin}/dllz3ml.so"
+    COMMAND touch ${z3ml_bin}/patched_dllz3ml
+    DEPENDS ${z3ml_bin}/dllz3ml.so
+    COMMENT "Patch macOS dynamic lib loader path"
+    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()
 
-set(z3ml_example_src ${PROJECT_SOURCE_DIR}/examples/ml/ml_example.ml)
-
-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" "${z3ml_bin}"
-    "-dllpath" "${z3ml_bin}"
-    "-I" ${ocaml_stublibs_path}
-    "-dllpath" ${ocaml_stublibs_path}
-    "${ocaml_pkg_zarith_path}/zarith.cma"
-    "${z3ml_bin}/z3ml.cma"
-    ${z3ml_example_src}
-  COMMAND 
-    "ocamlrun" "${z3ml_bin}/ml_example${bc_ext}"
-    ">" "${z3ml_bin}/ml_example.bc.log"
-  DEPENDS
-    ${z3ml_bin}/z3ml.cma
-    ${z3ml_bin}/dllz3ml.so
-    ${z3ml_example_src}
-  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}"
-    "-package" "zarith"
-    "-linkpkg"
-    "-I" "${z3ml_bin}"
-    "${z3ml_bin}/z3ml.cmxa"
-    "${z3ml_example_src}"
-  COMMAND "${z3ml_bin}/ml_example${exe_ext}"
-    ">" "${z3ml_bin}/ml_example.log"
-  DEPENDS
-    ${z3ml_bin}/z3ml.cmxa
-    ${z3ml_bin}/dllz3ml.so
-    ${z3ml_example_src}
-  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(patch_z3ml_dylib ALL
+  DEPENDS ${z3ml_bin}/patched_dllz3ml)
 
 add_custom_target(build_z3_ocaml_bindings
   ALL
@@ -278,7 +268,40 @@ add_custom_target(build_z3_ocaml_bindings
     ${z3ml_bin}/z3ml.cmxs
     ${z3ml_bin}/dllz3ml.so
     ${z3ml_bin}/libz3ml.a
-    build_ocaml_example
+    patch_z3ml_dylib
+)
+
+# test
+
+set(z3ml_example_src ${PROJECT_SOURCE_DIR}/examples/ml/ml_example.ml)
+
+add_custom_command(
+  TARGET build_z3_ocaml_bindings POST_BUILD
+  COMMAND "${OCAMLFIND}" ocamlc
+    -o "${z3ml_bin}/ml_example.byte"
+    -package zarith
+    -linkpkg
+    -I "${z3ml_bin}"
+    -dllpath "${z3ml_bin}"
+    "${z3ml_bin}/z3ml.cma"
+    "${z3ml_example_src}"
+  COMMAND ocamlrun "${z3ml_bin}/ml_example.byte" > "${z3ml_bin}/ml_example.bc.log"
+  COMMENT "Run OCaml bytecode example"
+  VERBATIM
+)
+
+add_custom_command(
+  TARGET build_z3_ocaml_bindings POST_BUILD
+  COMMAND "${OCAMLFIND}" ocamlopt
+    -o "${z3ml_bin}/ml_example"
+    -package zarith
+    -linkpkg
+    -I "${z3ml_bin}"
+    "${z3ml_bin}/z3ml.cmxa"
+    "${z3ml_example_src}"
+  COMMAND "${z3ml_bin}/ml_example" > "${z3ml_bin}/ml_example.log"
+  COMMENT "Run OCaml native example"
+  VERBATIM
 )
 
 ###############################################################################