Z3Prover / z3

The Z3 Theorem Prover
Other
10.29k stars 1.48k forks source link

build of Z3 through opam while installing fstar fails on mac M1 machine due to clang warning #5273

Closed smoothdeveloper closed 3 years ago

smoothdeveloper commented 3 years ago

I intend to install fstar through opam install fstar which pulls and builds Z3.

<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[z3.4.8.5] downloaded from https://github.com/Z3Prover/z3/archive/Z3-4.8.5.tar.gz
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[ERROR] The compilation of z3 failed at "/Users/gauthiersegay/.opam/opam-init/hooks/sandbox.sh build make -C build -j 7".
#=== ERROR while compiling z3.4.8.5 ===========================================#
# context     2.0.8 | macos/arm64 | ocaml-base-compiler.4.12.0 | https://opam.ocaml.org#e24f43ca
# path        ~/.opam/default/.opam-switch/build/z3.4.8.5
# command     ~/.opam/opam-init/hooks/sandbox.sh build make -C build -j 7
# exit-code   2
# env-file    ~/.opam/log/z3-93059-6aa130.env
# output-file ~/.opam/log/z3-93059-6aa130.out
### output ###
# [...]
# clang: warning: argument unused during compilation: '-msse2' [-Wunused-command-line-argument]
# g++ -o libz3.dylib -dynamiclib api/dll/install_tactic.o api/dll/mem_initializer.o api/dll/gparams_register_modules.o api/dll/dll.o api/api_array.o api/api_fpa.o api/api_arith.o api/api_datatype.o api/z3_replayer.o api/api_model.o api/api_log_macros.o api/api_ast_map.o api/api_datalog.o api/api_ast_vector.o api/api_commands.o api/api_opt.o api/api_special_relations.o api/api_algebraic.o api/ap[...]
# g++  -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 tactic[...]
# cp libz3.a libz3-static.a
# ocamlfind ocamlc -package num  -ccopt "-D_MP_INTERNAL -DNDEBUG -D_EXTERNAL_RELEASE   -fvisibility=hidden -c -msse -msse2 -D_NO_OMP_ -O3 -Wno-unknown-pragmas -Wno-overloaded-virtual -Wno-unused-value -fPIC -I /Users/gauthiersegay/.opam/default/lib/ocaml -I ../src/api -I ../src/api/ml -o api/ml/z3native_stubs.o" -c ../src/api/ml/z3native_stubs.c
# clang: warning: argument unused during compilation: '-msse' [-Wunused-command-line-argument]
# clang: warning: argument unused during compilation: '-msse2' [-Wunused-command-line-argument]
# cp libz3.dylib python
# 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: *** [api/ml/z3ml.cma] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build z3 4.8.5
+- 
- No changes have been performed

Reporting to track the issue, looking for possible workaround.

NikolajBjorner commented 3 years ago

you don't have omp installed. New versions of z3 do not use omp at all. You are building an older version.

hacdias commented 3 years ago

@smoothdeveloper I have the same issue, did you manage to fix/workaround it?