3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-07 13:16:25 +00:00
z3/.github/workflows/ocaml.yaml
Shiwei Weng 翁士伟 f7aec02503
WIP: Migrating OCaml binding to CMake (#7254)
* 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.
2025-04-19 13:41:27 -07:00

99 lines
2.6 KiB
YAML

name: OCaml Binding CI (Ubuntu)
on:
push:
branches: [ "**" ]
pull_request:
branches: [ "**" ]
jobs:
build-test-ocaml:
runs-on: ubuntu-latest
steps:
- name: Checkout code
uses: actions/checkout@v4
- name: Cache ccache
uses: actions/cache@v4
with:
path: ~/.ccache
key: ${{ runner.os }}-ccache-${{ github.ref }}
restore-keys: |
${{ runner.os }}-ccache-
- name: Install system dependencies
run: |
sudo apt-get update
sudo apt-get install -y \
opam bubblewrap m4 \
libgmp-dev pkg-config \
ninja-build ccache
- name: Init opam (no sandbox, no default switch)
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)
- name: Configure with CMake
run: |
eval $(opam env)
export CC="ccache gcc"
export CXX="ccache g++"
mkdir -p build
cd build
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: |
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
- name: Compile ml_example.byte
run: |
eval $(opam env)
ocamlc -version
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)
ocamlopt -version
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