diff --git a/.github/workflows/ocaml-all.yaml b/.github/workflows/ocaml-all.yaml new file mode 100644 index 000000000..c2fdc50be --- /dev/null +++ b/.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 \ No newline at end of file diff --git a/.github/workflows/ocaml.yaml b/.github/workflows/ocaml.yaml index bf2c62b84..d8b64b992 100644 --- a/.github/workflows/ocaml.yaml +++ b/.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 diff --git a/src/api/ml/CMakeLists.txt b/src/api/ml/CMakeLists.txt index cbff3c232..0b089b9ee 100644 --- a/src/api/ml/CMakeLists.txt +++ b/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" @@ -211,64 +231,34 @@ 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 ) ###############################################################################