WIP: Migrating OCaml binding to CMake #7254

arbipher · 2024-06-17T00:49:31Z

It's my WIP working on migrating the building of OCaml binding to CMake.

I think the majority of the work is done. I started by mimicking the other bindings and some llvm cmake for ocaml, but then I just manually wrote enough custom commands and dependencies. The actual building commands should have the same result as the previously generated python scripts, though I think I simplified some unnecessary dependencies and compiler flags.

tldr;

  cd build && cmake \
-G "Ninja" \
-DZ3_BUILD_LIBZ3_SHARED=TRUE \
-DZ3_BUILD_OCAML_BINDINGS=TRUE \
-DZ3_USE_LIB_GMP=TRUE \
../

It should just work. I also build and run the ml_examples.ml for both bytecode and native code in the cmake to make sure it works. I observe all z3 bindings are using shared library so I wonder maybe I don't even need to make a static version for the ocaml-binding.

I also add one argument -DZ3_BUILD_OCAML_EXTERNAL_LIBZ3=/path/to/libz3.so to support building ocaml building with an external z3 library that is often installed by some other distro package managers.

Now the remaining work is :

The installation part. I really don't have a good idea for non opam installation.
Test it on macos. I knew the problem and the two-line fix for macos's problem. It's in the comments yet.
Remove unnecessary files.
Write some good document for it.
Tune for the CI.
(this is out of z3 but) Make opam package for this new building script. However, I guess I have to adjust both sides to try letting it work well.

p.s. for ocaml users, I also have a post for discussion.

wintersteiger

Overall this looks like a good start, but it needs a lot of clean-up and extensions before it will be usable in practice.

wintersteiger · 2024-06-26T13:48:23Z

makefile

+	-ocamlcflags -bin-annot \
+	-package zarith \
+	-lz3 -lstdc++ -lpthread\
+	-lgmp \


GMP is optional, so this should be guarded.

wintersteiger · 2024-06-26T13:49:30Z

src/api/ml/z3.mli

@@ -3712,6 +3713,31 @@ end
    For example:
    (set_global_param "pp.decimal" "true")
    will set the parameter "decimal" in the module "pp" to true.
+
+    Legal parameters are:


These parameters can change and nobody will update this list. We could perhaps try to get this list programmatically?

Oh, this comes from my previous learning/experimenting notes so it shouldn't be included here.

I agree with your point.

wintersteiger · 2024-06-26T13:51:37Z

src/api/ml/CMakeLists.txt

+  set(libz3_path ${PROJECT_BINARY_DIR})
+endif()
+
+add_custom_command(


When using a custom command and target, will these always rebuild, even when there are no changes to the inputs?

No. add_custom_command will check the depends and outputs to decide whether to run it. CMake also checks them statically to make sure these commands are valid.

wintersteiger · 2024-06-26T13:52:34Z

src/api/ml/CMakeLists.txt

+  VERBATIM
+)
+
+add_custom_command(


It shouldn't be necessary to copy source files around, the other targets that use them can just as well reference the source directory.

It's subtle and I prefer to copy them. The reason is ocamlc may generate some intermediate files at the source location. It general, it can also simplify the dependencies of custom commands when some files are generated to be in the build path while some files are at the source path.

Oh yes, that's right. We do have to make sure everything is generated in the build directory, and sometimes that might indeed require copying source files around if the OCaml tools don't provide commandline flags to set the output path.

wintersteiger · 2024-06-26T13:53:14Z

src/api/ml/CMakeLists.txt

+if( APPLE )
+  set(ocaml_rpath "@executable_path/../libz3${so_ext}")
+elseif( UNIX )
+  set(ocaml_rpath "\\$ORIGIN/../libz3${so_ext}")


Windows/Cygwin?

At this moment, building on Windows/Cygwin is beyond my knowledge and I think even the support for OCaml on Windows is under heavy development. I may prefer to at least postpone it until the rest is done.

p.s. I notice there is some good news in the OCaml community.

Yeah, it's always been a bit neglected, but there are users, so we should make sure it works. BTW, the Opam people are also adding a Windows CI pipeline at the moment, so it might be required for Opam packages soon.

wintersteiger · 2024-06-26T13:57:37Z

cmake/modules/AddOCaml.cmake

+    set(ocaml_rpath "@executable_path/../../../lib${LLVM_LIBDIR_SUFFIX}")
+  elseif( UNIX )
+    set(ocaml_rpath "\\$ORIGIN/../../../lib${LLVM_LIBDIR_SUFFIX}")
+  endif()


Windows/Cygwin

wintersteiger · 2024-06-26T13:58:49Z

cmake/modules/AddOCaml.cmake

+# INCLUDES  Path for header files for C sources.
+# CFLAGS    Additional arguments passed when compiling C stubs.
+# PKG       Names of ocamlfind packages this library depends on.
+# LLVM      Names of LLVM libraries this library depends on.


Is this LLVM-only? If so, we need to add support for other compilers. If not, we should change those names.

It will remove it. It's the starting point of this work but later I realized the requirements for ocaml-llvm and ocaml-z3 are different.

wintersteiger · 2024-06-26T13:59:33Z

cmake/modules/AddOCaml.cmake

+  endforeach()
+
+  install(FILES ${install_files}
+          DESTINATION "${LLVM_OCAML_INSTALL_PATH}/llvm")


Not sure where this will attempt to install files to, but clearly ..../llvm will not make sense for any other compilers.

wintersteiger · 2024-06-26T14:00:07Z

cmake/modules/AddOCaml.cmake

+    add_custom_command(TARGET "ocaml_${name}" POST_BUILD
+      COMMAND "${CMAKE_COMMAND}" "-E" "copy" "${install_file}"
+                                             "${LLVM_LIBRARY_DIR}/ocaml/llvm/"
+      COMMENT "Copying OCaml library component ${filename} to intermediate area"


Suggested change

COMMENT "Copying OCaml library component ${filename} to intermediate area"

COMMENT "Installing OCaml library component ${filename}"

wintersteiger · 2024-06-26T14:01:02Z

README-CMake.md

@@ -292,6 +292,9 @@ The following useful options can be passed to CMake whilst configuring.
 * ``Z3_INSTALL_JAVA_BINDINGS`` - BOOL. If set to ``TRUE`` and ``Z3_BUILD_JAVA_BINDINGS`` is ``TRUE`` then running the ``install`` target will install Z3's Java bindings.
 * ``Z3_JAVA_JAR_INSTALLDIR`` - STRING. The path to directory to install the Z3 Java ``.jar`` file. This path should be relative to ``CMAKE_INSTALL_PREFIX``.
 * ``Z3_JAVA_JNI_LIB_INSTALLDIRR`` - STRING. The path to directory to install the Z3 Java JNI bridge library. This path should be relative to ``CMAKE_INSTALL_PREFIX``.
+* ``Z3_BUILD_OCAML_BINDINGS`` - BOOL. If set to ``TRUE`` then Z3's OCaml bindings will be built.
+* ``Z3_BUILD_JULIA_BINDINGS`` - BOOL. If set to ``TRUE`` then Z3's Julia bindings will be built.
+* ``Z3_INSTALL_JULIA_BINDINGS`` - BOOL. If set to ``TRUE`` and ``Z3_BUILD_JULIA_BINDINGS`` is ``TRUE`` then running the ``install`` target will install Z3's Julia bindings.


Add similar option for the OCaml bindings?

arbipher · 2024-07-02T16:55:11Z

Thank you so much for your careful examination. This is one reason I would like to make this immature draft PR.
I am learning how z3 is installed on some platforms so my change won't break them. Also, I am still thinking how the ocaml-binding should be installed.

I will check your changes one by one later.

NikolajBjorner · 2024-11-02T18:30:17Z

It would be absolutely great to cmake-ify the ocaml bindings for uniform build support and allow to retarget release processes to use the more portable cmake system.

arbipher · 2024-11-03T00:01:28Z

Aha, I was occupied by some random things after the previous effect on this issue in July. I hope to pick this up this month.

…n the bin.

arbipher · 2025-04-19T19:38:39Z

I made some updates (finally) to the PR. After it looks good to you, I can cherry-pick them to the latest commit and make another PR.

For the previous review,

I removed all the necessary source file copying.
I deleted AddOCaml.make, which was used for llvm.

I added Github Action and made it work on both ubuntu and macOS. They work (finally finally) on my forked repo.

For the linking especially rpath-related, since platforms like Debian (discourage), homebrew(hacking) or even opam have its own mechanism to handle, in this build I just figured out a way (mainly for macOS) to make two working build and run as sanity check.

The next step is to allow external libz3 and allow binding to be built with them. I am still not very clear on the current Windows support for ocaml as well as the users will use a Windows native binding.

NikolajBjorner · 2025-04-19T20:19:28Z

Regarding Windows + OCaml: It isn't (was never before) a big use case and nowadays it is very easy to start up wsl2/ubuntu for ocaml development.

I sometimes tease @msprotz on his past heroic efforts in this space, so thanks for the reminder.

arbipher · 2025-04-19T20:54:30Z

Cool for the merging. There is a debug helper makefile in it (which shouldn't be a big deal and I will remove it in the next PR for the next steps).

arbipher added 9 commits June 16, 2024 20:07

Update doc for mk_context.

b70ba6e

Migrating to cmake.

c998cf2

Migrating to cmake. It builds both internal or external libz3.

e8c1947

Start to work on platform-specific problem.

7844113

Messy notes.

64b7a3a

debug.

dbc7889

Cleanup a bit.

f0082a7

Fixing shared lib extension.

f855456

Minor.

4b32075

wintersteiger suggested changes Jun 26, 2024

View reviewed changes

jollheef mentioned this pull request Oct 27, 2024

z3: missing Z3Config.cmake NixOS/nixpkgs#105358

Open

CertainLach mentioned this pull request Mar 16, 2025

prusa-slicer: 2.9.0 -> 2.9.1 NixOS/nixpkgs#390476

Open

13 tasks

arbipher force-pushed the cmake-ocaml-binding branch 2 times, most recently from f401083 to 4b32075 Compare April 17, 2025 07:07

arbipher added 4 commits April 17, 2025 03:08

Resume working on this PR.

b03efc7

Remove including AddOCaml.

7a78bd4

Keep z3.ml and z3.mli in the src but specify the generated file i…

7943538

…n the bin.

Keep ml_example.ml in the src.

bf21d02

arbipher force-pushed the cmake-ocaml-binding branch 3 times, most recently from 4d6153f to 9c7e799 Compare April 18, 2025 08:27

Try github action for ocaml.

a405046

arbipher force-pushed the cmake-ocaml-binding branch 5 times, most recently from 42f1f44 to 63d8171 Compare April 18, 2025 18:13

arbipher force-pushed the cmake-ocaml-binding branch 18 times, most recently from b599979 to 738954d Compare April 18, 2025 23:00

Add workflow using matrix.

eac9908

arbipher force-pushed the cmake-ocaml-binding branch 2 times, most recently from affef6c to ea9716b Compare April 19, 2025 16:18

Fix mac linking once more.

ac10869

arbipher force-pushed the cmake-ocaml-binding branch from ea9716b to ac10869 Compare April 19, 2025 16:26

Bypass @rpath in building sanity check.

4237ebd

arbipher mentioned this pull request Apr 19, 2025

Z3 does not build by default on ubuntu 24.04 ocaml/opam-repository#25807

Open

NikolajBjorner marked this pull request as ready for review April 19, 2025 20:23

NikolajBjorner merged commit f7aec02 into Z3Prover:master Apr 19, 2025
10 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

WIP: Migrating OCaml binding to CMake #7254

WIP: Migrating OCaml binding to CMake #7254

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

	COMMENT "Copying OCaml library component ${filename} to intermediate area"
	COMMENT "Installing OCaml library component ${filename}"

WIP: Migrating OCaml binding to CMake #7254

WIP: Migrating OCaml binding to CMake #7254

Uh oh!

Conversation

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!