On macos, depqbf gives a Dl error

[maelvls]

Dear Simon,

Yesterday, I tried to use DepQBF because Quantor is unable to give a value for some outer-scope existential variables.

I installed depqbf using opam install depqbf (macos). But when running make test:

Fatal error: exception Dl.DL_error("dlsym(RTLD_DEFAULT, qdpll_delete): symbol not found")

After some (extensive) search, I found the issue yallop/ocaml-ctypes#41 talking about this specific problem. Apparently, even though the static libqdpll.a is the one selected (I double checked by removing the dynamic library), the symbol is not imported in the final binary (same error for byte or native).

To work around this problem, I have changed in _oasis (in the qbf-depqbf section)

CCLib: -L/usr/local/lib/ -lqdpll

to

CCLib: "-force_load /usr/local/lib/libqdpll.a"

This solves the problem and make test works on both ubuntu and macos (provided that libffi-dev is installed on ubuntu and libffi installed on macos using brew).

---

Side note: I also added some comments in the README in order to debug the most common issues.

[c-cube]

Is it specific to clang? gcc seems to fail (see travis build).

edit: ah, I see that some commits address this. I'll wait for CI, thanks for the contribution anyway!

[maelvls]

The -force_load seems to be clang-specific; so I changed _oasis to

if system(macosx)
    CCLib:              -force_load /usr/local/lib/libqdpll.a
  else
    CCLib:              -L/usr/local/lib -lqdpll

I am still struggling with the installation of qdpll.a on linux (on macos, brew install depqbf is enough; apt install depqbf only installs the binary).
I'll fix the

[c-cube]

Do you think this is ready to merge? The failures on travis seem to be due to problems with installing depqbf…

[maelvls]

Hi! I am kind of stuck with depqbf installation on Linux; I must have the PIC version of libqbpll.a (which is not really easy to do with the makefile coming with Depqbf). I'll give one more asap. For now, the PR can be closed or put in stale mode. Have a nice end of weekend!!

[c-cube]

would this still make sense?

[maelvls]

It doesn’t make sense anymore since the new dune config does not allow us to build with depqbf 😅

I’ll close it for now