Update on building OCaml binding with CMake

[arbipher]

As discussed in #7684, it should be a working CMake for OCaml binding after #7254.

The CI in my z3 fork builds and tests it on Ubuntu and macOS. I will make a z3 package (probably z3.dev) on opam when this is merged.

I fixed the OCaml z3 building warning by just completing the missing variants and putting an explanatory string as python did.

z3/src/api/python/z3/z3.py

Lines 847 to 850 in d717dae

	elif k == Z3_PARAMETER_INTERNAL:
	result[i] = "internal parameter"
	elif k == Z3_PARAMETER_ZSTRING:
	result[i] = "internal string"

I don't add demo functions for those in ml_example.ml since I found it's not that easy. Let's leave it for next time (to understand the alignment between OCaml API, C API, and the C++ definitions).

[Copilot]

Pull Request Overview

This PR updates the OCaml binding build process to fully support CMake-based builds, adds missing parameter variants, and refines CI workflows for Ubuntu and macOS.

• Expose new P_Rat, P_Internal, and P_ZStr variants in OCaml API, aligning with Python’s explanatory strings
• Revise CMakeLists: rename targets, generate META from META.in, remove legacy patch logic, and update META.in version placeholder
• Enhance GitHub Actions to use a matrix for Ubuntu/macOS, cache ccache and opam, and properly set up OCaml toolchain

Reviewed Changes

Copilot reviewed 6 out of 6 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
src/api/ml/z3.mli	Added missing P_Rat, P_Interal, P_ZStr variants
src/api/ml/z3.ml	Implemented get_kind, get_rational, and parameter matching
src/api/ml/META.in	Switched version placeholder to @Z3_VERSION_STRING@
src/api/ml/CMakeLists.txt	Renamed build targets, auto-generate META, removed old patches
.github/workflows/ocaml.yaml	Expanded CI to Ubuntu + macOS, added caching and matrix setup

Comments suppressed due to low confidence (2)

src/api/ml/CMakeLists.txt:70

• [nitpick] There’s a large block of commented-out commands here; consider removing or moving them to an archive section to keep the file clean.

add_custom_command(

src/api/ml/CMakeLists.txt:10

• Renaming the CMake option from Z3_BUILD_OCAML_EXTERNAL_LIBZ3 to Z3_BUILD_EXTERNAL_LIBZ3 is a breaking change; please document it in the build instructions or provide an alias for backward compatibility.

if (Z3_BUILD_EXTERNAL_LIBZ3)

[arbipher]

The copilot review is cool! We get free access through GitHub Student Pack and the university. I started to heavily use these LLM tools with coding and wording (but I don't use it for the typechecking for the code, a missed corner case).

However, it cannot solve the most tricky cases for these z3 OCaml binding's building, linking, and demoing scenarios. I think the problem is that the area is relatively underexplored, so even humans lack clear invariants. I have been exploring some semantics and static checking for these areas for a while, and I believe we don't need that long for machines to solve these questions more reliably.

[NikolajBjorner]

It's all the rage and yes more is coming online and mainstream, but first for mainstream use cases.