Ask for suggestions for the next z3 package release

,

I was not aware that even editing a post would bring the post to the top. I was thinking I could do silent logging, but it turned out to be not the case.

I found another two days to continue on this topic, and now the CMake system works well for either the on-the-tree z3 (when building ocaml-z3 with z3 source) or off-the-tree z3 (when building ocaml-z3 with an external distro libz3).

The tentative command is

	cd build && cmake \
	-DCMAKE_VERBOSE_MAKEFILE=TRUE \
	-DZ3_BUILD_LIBZ3_SHARED=TRUE \
	-DZ3_BUILD_OCAML_BINDINGS=TRUE \
	-DZ3_BUILD_OCAML_EXTERNAL_LIBZ3=/path/to/distro-z3 \

If Z3_BUILD_OCAML_EXTERNAL_LIBZ3 is given, it will use that to build ocaml-z3. It should be compatible and flexible enough for different package managers,

The unpolished and undocumented CMakeLists.txt is here. I added a test-build and test-run for z3/ml_example.ml.

Besides CMake itself, ocamlrun also costs unexpected time since I realized there is no ocamlfind ocamlrun, so the correct cma must be provided manually. I also suspect whether ocamlrun really respects <opam-switch>/lib/stublibs because I have to provide -I ${ocaml_stublibs_path} -dllpath ${ocaml_stublibs_path} even it’s already provided by ocamlmklib.

The next step is

  1. to polish it then to PR for z3 The draft PR at github/z3
  2. to make opam packages
  3. to write down everything.

p.s. the side-of-side project, a better surface language for writing cmake is started. Enough CMake ast and basic pretty printing is done. I hope I can write no cmake after this topic…

1 Like