macOS Mojave: `opam install z3` fails with `ld: library not found for -lgomp`

[andreasabel]

macOS Mojave: opam install z3 fails with ld: library not found for -lgomp

The native C compiler of macOS Mojave does not seem to have library gomp. I installed the GNU C compiler (following https://stackoverflow.com/questions/64116617/libgomp-and-macosx) and it is in my PATH:

$ realpath $(which g++)
/usr/local/Cellar/gcc/10.2.0_2/bin/g++-10

Yet it is not picked up by opam, it calls clang++, and finally fails in ocamlmklib.

Is there a workaround, like telling opam which C compiler to use, or additional libraries to use?

Full log:

#=== ERROR while compiling z3.4.8.5 ===========================================#
# context     2.0.4 | macos/x86_64 | ocaml-base-compiler.4.11.1 | https://opam.ocaml.org#1fc79772
# path        ~/.opam/4.11.1/.opam-switch/build/z3.4.8.5
# command     ~/.opam/opam-init/hooks/sandbox.sh build make -C build -j 3
# exit-code   2
# env-file    ~/.opam/log/z3-10268-d4902a.env
# output-file ~/.opam/log/z3-10268-d4902a.out
### output ###
# [...]
# /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/ranlib: file: libz3.a(cooperate.o) has no symbols
# /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/ranlib: file: libz3.a(trace.o) has no symbols
# /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/ranlib: file: libz3.a(dense_matrix.o) has no symbols
# cp libz3.a libz3-static.a
# ocamlfind ocamlc -package num  -ccopt "-D_MP_INTERNAL -DNDEBUG -D_EXTERNAL_RELEASE   -fvisibility=hidden -c -mfpmath=sse -msse -msse2 -D_NO_OMP_ -O3 -Wno-unknown-pragmas -Wno-overloaded-virtual -Wno-unused-value -fPIC -I /Users/abel/.opam/4.11.1/lib/ocaml -I ../src/api -I ../src/api/ml -o api/ml/z3native_stubs.o" -c ../src/api/ml/z3native_stubs.c
# cp libz3.dylib python
# clang++  -o z3  shell/lp_frontend.o shell/dimacs_frontend.o shell/z3_log_frontend.o shell/install_tactic.o shell/mem_initializer.o shell/datalog_frontend.o shell/gparams_register_modules.o shell/opt_frontend.o shell/smtlib_frontend.o shell/main.o cmd_context/extra_cmds/extra_cmds.a api/api.a opt/opt.a tactic/portfolio/portfolio.a tactic/fpa/fpa_tactics.a tactic/smtlogics/smtlogic_tactics.a ta[...]
# ocamlmklib -o api/ml/z3ml -I api/ml -L. api/ml/z3native_stubs.o api/ml/z3enums.cmo api/ml/z3native.cmo api/ml/z3.cmo  -lz3-static -lstdc++ -lgomp 
# ld: library not found for -lgomp
# clang: error: linker command failed with exit code 1 (use -v to see invocation)
# make: *** [Makefile:4464: api/ml/z3ml.cma] Error 2
# make: Leaving directory '/Users/abel/.opam/4.11.1/.opam-switch/build/z3.4.8.5/build'

[NikolajBjorner]

@c-cube Do you have an idea?

[c-cube]

I see the following in opam-repository:

packages/z3/z3.4.8.5/files/4468.patch
252:+            LIBZ3 = '-l' + z3link + ' -lstdc++' + ' -lgomp'

so I suspect that this version has a typo and it should be -lgmp. Try opam pin z3 4.8.11 instead to get a more recent version?

[NikolajBjorner]

Good catch on old the version/patch. Note also that z3 uses pthreads and not omp any longer. Maybe gmp depending on zarith dependencies or if z3 is compiled with optional gmp. There are no cycles to support old versions.

[andreasabel]

I confirm that 4.8.11 builds fine on my system, but fstar, my installation goal, requires 4.8.5. I reported this conflict to the fstar repo at https://github.com/FStarLang/FStar/issues/2344.

[c-cube]

I think you can use something like opam pin z3 4.8.5 --edit to modify the package locally (here, fix the patch maybe).

[andreasabel]

I think you can use something like opam pin z3 4.8.5 --edit to modify the package locally (here, fix the patch maybe).

Thanks @c-cube ! But I think I leave the fixing to the Fstar crowd...