Z3 build on opam 2.2 Windows fails

[jrrk2]

I don't know if this is the correct place to report it, but: opam fails to install the z3 ocaml bindings on Windows:

* An option like /linkXXX is an abbrevation for '-link XXX'.

* An option like -Wl,-XXX is an abbreviation for '-link -XXX'.

* FlexDLL's object files are searched by default in the same directory as

flexlink, or in the directory given by the environment variable FLEXDIR

if it is defined.

* Extra argument can be passed in the environment variable FLEXLINKFLAGS.

#

Homepage: http://alain.frisch.fr/flexdll.html

File "caml_startup", line 1:

Error: Error during linking (exit code 2)

make: *** [Makefile:5321: api/ml/z3ml.cmxs] Error 2

make: Leaving directory '/cygdrive/c/Users/jonat/AppData/Local/opam/5.2.0/.opam-switch/build/z3.4.13.0-3/build'

[wintersteiger]

Can you add the entire build log? Because of the flexlink complaints I suspect that some variable received an invalid value. It could also mean that some dependency is missing, but it's impossible to tell without the rest of the log.

If it's not specific to Z3, but an opam issue, https://github.com/ocaml/opam-repository/issues would be the right place to report it.

[jrrk2]

z3err.zip

full output attached as a zip file

[wintersteiger]

Ah! There we go: flexlink: unknown option '-static-libgcc'.

This seems to be an issue with a mixed cygwin + mingw setup. We may have to either remove that option or add -link -static-libgcc, but I have no idea how those changes would affect existing (recent) installations. In your case, it may be easier and faster to switch the C compiler to the cygwin gcc.

[nadlertz]

Ah! There we go: flexlink: unknown option '-static-libgcc'.

This seems to be an issue with a mixed cygwin + mingw setup. We may have to either remove that option or add -link -static-libgcc, but I have no idea how those changes would affect existing (recent) installations. In your case, it may be easier and faster to switch the C compiler to the cygwin gcc.

We encounter the same problem. Removing -static-libgcc would make our application dependent on shared libraries which is not what we want. We want z3 to be contained inside the application.

Adding the -link flag doesn't seem to work either. I can't find any information on this flag. Does it even exist? When adding it we get the error:

g++ -o libz3.dll -shared api/dll/dll.o api/dll/gparams_register_modules.o api/dll/install_tactic.o api/dll/mem_initializer.o api/api_algebraic.o api/api_arith.o api/api_array.o api/api_ast.o api/api_ast_map.o api/api_ast_vector.o api/api_bv.o api/api_commands.o api/api_config_params.o api/api_context.o api/api_datalog.o api/api_datatype.o api/api_fpa.o api/api_goal.o api/api_log.o api/api_log_macros.o api/api_model.o api/api_numeral.o api/api_opt.o api/api_params.o api/api_parsers.o api/api_pb.o api/api_polynomial.o api/api_qe.o api/api_quant.o api/api_rcf.o api/api_seq.o api/api_solver.o api/api_special_relations.o api/api_stats.o api/api_tactic.o api/z3_replayer.o cmd_context/extra_cmds/extra_cmds.lib opt/opt.lib tactic/portfolio/portfolio.lib tactic/fpa/fpa_tactics.lib tactic/ufbv/ufbv_tactic.lib tactic/smtlogics/smtlogic_tactics.lib muz/fp/fp.lib muz/bmc/bmc.lib muz/ddnf/ddnf.lib muz/tab/tab.lib muz/clp/clp.lib muz/spacer/spacer.lib muz/rel/rel.lib muz/transforms/transforms.lib muz/dataflow/dataflow.lib muz/base/muz.lib tactic/fd_solver/fd_solver.lib sat/sat_solver/sat_solver.lib qe/qe.lib tactic/sls/sls_tactic.lib smt/tactic/smt_tactic.lib tactic/bv/bv_tactics.lib nlsat/tactic/nlsat_tactic.lib sat/tactic/sat_tactic.lib sat/smt/sat_smt.lib smt/smt.lib smt/proto_model/proto_model.lib math/subpaving/tactic/subpaving_tactic.lib solver/assertions/solver_assertions.lib tactic/arith/arith_tactics.lib tactic/core/core_tactics.lib ast/fpa/fpa.lib ackermannization/ackermannization.lib tactic/aig/aig_tactic.lib ast/pattern/pattern.lib parsers/smt2/smt2parser.lib cmd_context/cmd_context.lib solver/solver.lib qe/lite/qe_lite.lib qe/mbp/mbp.lib tactic/tactic.lib ast/sls/ast_sls.lib ast/simplifiers/simplifiers.lib ast/converters/converters.lib model/model.lib ast/macros/macros.lib ast/proofs/proofs.lib ast/substitution/substitution.lib ast/normal_forms/normal_forms.lib ast/rewriter/bit_blaster/bit_blaster.lib ast/rewriter/rewriter.lib math/lp/lp.lib nlsat/nlsat.lib sat/sat.lib math/grobner/grobner.lib ast/euf/euf.lib parsers/util/parser_util.lib smt/params/smt_params.lib ast/ast.lib math/subpaving/subpaving.lib math/realclosure/realclosure.lib params/params.lib math/automata/automata.lib math/hilbert/hilbert.lib math/simplex/simplex.lib math/dd/dd.lib math/interval/interval.lib math/polynomial/polynomial.lib util/util.lib -lpthread  -link -static-libgcc -static-libstdc++ -Wl,--out-implib,libz3.dll.a
/usr/lib/gcc/x86_64-pc-msys/11.3.0/../../../../x86_64-pc-msys/bin/ld/usr/lib/gcc/x86_64-pc-msys/11.3.0/../../../../x86_64-pc-msys/bin/ld: cannot find -link: No such file or directory
: cannot find -link: No such file or directory
collect2: error: ld returned 1 exit status

[jrrk2]

Thanks for your input. It seems to work on WSL already so i’m going with that as a workaround for now. Although static linking is desirable in many ways it can cause problems in obscure circumstances (for example when stuff is happening in the dynamic loader).

Sent from my iPhone

On 4 Sep 2024, at 10:04, Niclas Adlertz @.***> wrote:



Ah! There we go: flexlink: unknown option '-static-libgcc'.

This seems to be an issue with a mixed cygwin + mingw setup. We may have to either remove that option or add -link -static-libgcc, but I have no idea how those changes would affect existing (recent) installations. In your case, it may be easier and faster to switch the C compiler to the cygwin gcc.

We encounter the same problem. Removing -static-libgcc would make our application dependent on shared libraries which is not what we want. We want z3 to be contained inside the application.

Adding the -link flag doesn't seem to work either. I can't find any information on this flag. Does it even exist? When adding it we get the error:

g++ -o libz3.dll -shared api/dll/dll.o api/dll/gparams_register_modules.o api/dll/install_tactic.o api/dll/mem_initializer.o api/api_algebraic.o api/api_arith.o api/api_array.o api/api_ast.o api/api_ast_map.o api/api_ast_vector.o api/api_bv.o api/api_commands.o api/api_config_params.o api/api_context.o api/api_datalog.o api/api_datatype.o api/api_fpa.o api/api_goal.o api/api_log.o api/api_log_macros.o api/api_model.o api/api_numeral.o api/api_opt.o api/api_params.o api/api_parsers.o api/api_pb.o api/api_polynomial.o api/api_qe.o api/api_quant.o api/api_rcf.o api/api_seq.o api/api_solver.o api/api_special_relations.o api/api_stats.o api/api_tactic.o api/z3_replayer.o cmd_context/extra_cmds/extra_cmds.lib opt/opt.lib tactic/portfolio/portfolio.lib tactic/fpa/fpa_tactics.lib tactic/ufbv/ufbv_tactic.lib tactic/smtlogics/smtlogic_tactics.lib muz/fp/fp.lib muz/bmc/bmc.lib muz/ddnf/ddnf.lib muz/tab/tab.lib muz/clp/clp.lib muz/spacer/spacer.lib muz/rel/rel.lib muz/transforms/transforms.lib muz/dataflow/dataflow.lib muz/base/muz.lib tactic/fd_solver/fd_solver.lib sat/sat_solver/sat_solver.lib qe/qe.lib tactic/sls/sls_tactic.lib smt/tactic/smt_tactic.lib tactic/bv/bv_tactics.lib nlsat/tactic/nlsat_tactic.lib sat/tactic/sat_tactic.lib sat/smt/sat_smt.lib smt/smt.lib smt/proto_model/proto_model.lib math/subpaving/tactic/subpaving_tactic.lib solver/assertions/solver_assertions.lib tactic/arith/arith_tactics.lib tactic/core/core_tactics.lib ast/fpa/fpa.lib ackermannization/ackermannization.lib tactic/aig/aig_tactic.lib ast/pattern/pattern.lib parsers/smt2/smt2parser.lib cmd_context/cmd_context.lib solver/solver.lib qe/lite/qe_lite.lib qe/mbp/mbp.lib tactic/tactic.lib ast/sls/ast_sls.lib ast/simplifiers/simplifiers.lib ast/converters/converters.lib model/model.lib ast/macros/macros.lib ast/proofs/proofs.lib ast/substitution/substitution.lib ast/normal_forms/normal_forms.lib ast/rewriter/bit_blaster/bit_blaster.lib ast/rewriter/rewriter.lib math/lp/lp.lib nlsat/nlsat.lib sat/sat.lib math/grobner/grobner.lib ast/euf/euf.lib parsers/util/parser_util.lib smt/params/smt_params.lib ast/ast.lib math/subpaving/subpaving.lib math/realclosure/realclosure.lib params/params.lib math/automata/automata.lib math/hilbert/hilbert.lib math/simplex/simplex.lib math/dd/dd.lib math/interval/interval.lib math/polynomial/polynomial.lib util/util.lib -lpthread -link -static-libgcc -static-libstdc++ -Wl,--out-implib,libz3.dll.a /usr/lib/gcc/x86_64-pc-msys/11.3.0/../../../../x86_64-pc-msys/bin/ld/usr/lib/gcc/x86_64-pc-msys/11.3.0/../../../../x86_64-pc-msys/bin/ld: cannot find -link: No such file or directory : cannot find -link: No such file or directory collect2: error: ld returned 1 exit status

— Reply to this email directly, view it on GitHubhttps://github.com/Z3Prover/z3/issues/7359#issuecomment-2328311664, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AE6VVMZGEZU3K33K4WX6YDDZU3EIPAVCNFSM6AAAAABNII75TKVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGMRYGMYTCNRWGQ. You are receiving this because you authored the thread.Message ID: @.***>

[wintersteiger]

Adding the -link flag doesn't seem to work either. I can't find any information on this flag. Does it even exist?

It's an option to flexlink, not to the compiler/linker. It instructs flexlink to pass the following argument to the linker.