Build instructions in README seem to be incomplete.

[aniemetz]

Maybe I'm doing something wrong but I tried to follow the README instructions to build ocaml-bitwuzla and when I call dune build it fails with:

File "dune", line 20, characters 16-41:
20 |   (include_dirs vendor/bitwuzla/src/api/c))
                     ^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Include directory "vendor/bitwuzla/src/api/c" does not exist.

I assume the vendor/bitwuzla/ directory needs to be initialized with the sources. What's the preferred way to do this?

[recoules]

Right! I should add to the readme that it is required to initialize the submodules before. git submodule init or directly during clone: git clone --recurse-submodules git@github.com:bitwuzla/ocaml-bitwuzla.git

[aniemetz]

Just for the record, in the first case, you need

git submodule init
git submodule update

[aniemetz]

Hm, with this, dune build fails for cadical for me, though:

File "vendor/cadical/src/_unknown_", line 1, characters 0-0:
Error: File unavailable: vendor/cadical/src/makefile

[aniemetz]

Same when I do the init/update during clone.

[recoules]

Yes, the only solution for now is to manually delete the broken symlink... (see arminbiere/cadical#36; e070b27)

[aniemetz]

Does CaDiCaL 808dfac53a compile for you? That's the commit that was checked out and it doesn't compile for me.

[recoules]

What is your os? As far as I know, it compiles on "debian-family", "alpine" or "fedora". I am not quite sur about "centos" or "archlinux".

Tests are running at https://opam.ci.ocaml.org/github/ocaml/opam-repository/commit/2430eccba10347f4f97ff3a7e2c726b44b61933f

[aniemetz]

@recoules I'm wondering why the dependencies are set up via git modules. I recommend setting up all dependencies with the setup- scripts provided in https://github.com/bitwuzla/bitwuzla/tree/main/contrib, so that this is always in sync with what we have configured for Bitwuzla.

[recoules]

Does checkout the commit 88623ef solve your issue?

[aniemetz]

I'm on Arch with gcc 11.1. It seems that CaDiCaL does not compile with gcc 11.1 (it does with gcc 10.2 on Arch).

[aniemetz]

Does checkout the commit 88623ef solve your issue?

Nope, master CaDiCaL doesn't compile for me (the size_t issue in reap.cpp).

[aniemetz]

This is, of course, independent from the build setup for ocaml-bitwuzla.

[recoules]

@recoules I'm wondering why the dependencies are set up via git modules. I recommend setting up all dependencies with the setup- scripts provided in https://github.com/bitwuzla/bitwuzla/tree/main/contrib, so that this is always in sync with what we have configured for Bitwuzla.

As far as I know, I am in sync with the scripts from contrib. Yet, we can not download the dependencies during the opam package installation while dune-release offer an option to directly handle submodule.

Nope, master CaDiCaL doesn't compile for me (the size_t issue in reap.cpp).

See https://github.com/bitwuzla/ocaml-bitwuzla/blob/master/vendor/quickfix-size_t-doe-not-name-a-type.patch

[aniemetz]

You do not apply the symFPU patch, though, do you? https://github.com/bitwuzla/bitwuzla/blob/main/contrib/setup-symfpu.sh#L23

[recoules]

You do not apply the symFPU patch, though, do you? https://github.com/bitwuzla/bitwuzla/blob/main/contrib/setup-symfpu.sh#L23

Yes, the patches are applied by dune in its workspace juste before the compilation take place.

[aniemetz]

I installed the test dependency, but dune runtest doesn't seem to do anything. Any pointers? Sorry for being so dumb, but I have 0 experience with ocaml :disappointed:

[recoules]

Well, you can try to modify any %expect_test in test/t_bitwuzla_c.ml and run it again. If it still does nothing, there is a problem, if it print a diff, that is just that there is no (visible) bug ;-)

[aniemetz]

OK, all good :partying_face:

Would be good to update the README with the info about how to set up the submodules when you have time.

[recoules]

Tomorrow (UTC+2 ^^), I will check the results of the opam-ci. I will update the README accordingly too (sorry, first time I package a software for multiple os/arch/dependencies).

c ya,

[recoules]

I have just updated the README with additional information.

[aniemetz]

LGTM