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.

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

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

WIP: Migrating OCaml binding to CMake #7254

WIP: Migrating OCaml binding to CMake #7254

arbipher commented Jun 17, 2024 •

edited

Loading

wintersteiger left a comment

wintersteiger Jun 26, 2024

arbipher Jul 2, 2024

wintersteiger Jun 26, 2024

arbipher Jul 2, 2024

wintersteiger Jun 26, 2024

arbipher Jul 2, 2024

wintersteiger Jun 26, 2024

arbipher Jul 2, 2024

wintersteiger Jul 11, 2024

wintersteiger Jun 26, 2024

arbipher Jul 2, 2024

wintersteiger Jul 11, 2024

wintersteiger Jun 26, 2024

wintersteiger Jun 26, 2024

arbipher Jul 2, 2024

wintersteiger Jun 26, 2024

wintersteiger Jun 26, 2024

wintersteiger Jun 26, 2024

arbipher commented Jul 2, 2024

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

WIP: Migrating OCaml binding to CMake #7254

Are you sure you want to change the base?

WIP: Migrating OCaml binding to CMake #7254

Conversation

arbipher commented Jun 17, 2024 • edited Loading

wintersteiger left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

arbipher commented Jul 2, 2024

arbipher commented Jun 17, 2024 •

edited

Loading