search

cvc5 / cvc5

cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems.
Other
1.03k stars 233 forks source link

Cannot build with `--static` if system `libgmp.so` is present but `libgmp.a` is missing #10089

Closed Selebrator closed 12 months ago

Selebrator commented 1 year ago

Describe the bug My system has libgmp.so, but is missing libgmp.a. As a result I cannot build with ./configure.sh --static. The configure and compile phase work just fine, but linking fails.

For reference, here are the files included in Arch Linux's GMP package.

I don't need this fixed for myself. I just thought you would want to know about it :)

cvc5 version/commit: 26308ebd1dd6314c9634dd9935aa6fdce91bd856 (latest as of writing) Operating system: Arch Linux

configure.sh options 

./configure.sh --prefix=build/install --auto-download --static

configure.sh output 

-- The C compiler identification is GNU 13.2.1
-- The CXX compiler identification is GNU 13.2.1
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Check for working C compiler: /usr/bin/cc - skipped
-- Detecting C compile features
-- Detecting C compile features - done
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Check for working CXX compiler: /usr/bin/c++ - skipped
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Found Git: /usr/bin/git (found version "2.42.0")
fatal: No names found, cannot describe anything.
-- Building Production build
-- Performing Test HAVE_C_FLAG_O3
-- Performing Test HAVE_C_FLAG_O3 - Success
-- Configuring with C flag '-O3'
-- Performing Test HAVE_CXX_FLAG_O3
-- Performing Test HAVE_CXX_FLAG_O3 - Success
-- Configuring with CXX flag '-O3'
-- Performing Test HAVE_C_FLAG_Wall
-- Performing Test HAVE_C_FLAG_Wall - Success
-- Configuring with C flag '-Wall'
-- Performing Test HAVE_CXX_FLAG_Wall
-- Performing Test HAVE_CXX_FLAG_Wall - Success
-- Configuring with CXX flag '-Wall'
-- Performing Test HAVE_C_FLAG_Wunused_private_field
-- Performing Test HAVE_C_FLAG_Wunused_private_field - Failed
-- Performing Test HAVE_CXX_FLAG_Wunused_private_field
-- Performing Test HAVE_CXX_FLAG_Wunused_private_field - Failed
-- Performing Test HAVE_C_FLAG_fexceptions
-- Performing Test HAVE_C_FLAG_fexceptions - Success
-- Configuring with C flag '-fexceptions'
-- Performing Test HAVE_CXX_FLAG_Wsuggest_override
-- Performing Test HAVE_CXX_FLAG_Wsuggest_override - Success
-- Configuring with CXX flag '-Wsuggest-override'
-- Performing Test HAVE_CXX_FLAG_Wnon_virtual_dtor
-- Performing Test HAVE_CXX_FLAG_Wnon_virtual_dtor - Success
-- Configuring with CXX flag '-Wnon-virtual-dtor'
-- Performing Test HAVE_C_FLAG_Wimplicit_fallthrough
-- Performing Test HAVE_C_FLAG_Wimplicit_fallthrough - Success
-- Configuring with C flag '-Wimplicit-fallthrough'
-- Performing Test HAVE_CXX_FLAG_Wimplicit_fallthrough
-- Performing Test HAVE_CXX_FLAG_Wimplicit_fallthrough - Success
-- Configuring with CXX flag '-Wimplicit-fallthrough'
-- Performing Test HAVE_C_FLAG_Wshadow
-- Performing Test HAVE_C_FLAG_Wshadow - Success
-- Configuring with C flag '-Wshadow'
-- Performing Test HAVE_CXX_FLAG_Wshadow
-- Performing Test HAVE_CXX_FLAG_Wshadow - Success
-- Configuring with CXX flag '-Wshadow'
-- Performing Test HAVE_CXX_FLAG_fno_extern_tls_init
-- Performing Test HAVE_CXX_FLAG_fno_extern_tls_init - Success
-- Configuring with CXX flag '-fno-extern-tls-init'
-- Performing Test HAVE_CXX_FLAG_Wclass_memaccess
-- Performing Test HAVE_CXX_FLAG_Wclass_memaccess - Success
-- Configuring with CXX flag '-Wno-class-memaccess'
-- Using GNU gold linker.
-- Disabling unit tests since assertions are disabled.
-- Found Python: /usr/bin/python3.11 (found version "3.11.5") found components: Interpreter
-- Found GMP (unknown version): /usr/lib/libgmp.so
-- Looking for getc_unlocked
-- Looking for getc_unlocked - not found
-- Building CaDiCaL rel-1.7.4: /home/lukas/tmp/cvc5/build/deps/lib/libcadical.a
-- Building Poly 0.1.13: /home/lukas/tmp/cvc5/build/deps/lib/libpicpoly.a, /home/lukas/tmp/cvc5/build/deps/lib/libpicpolyxx.a
-- Building SymFPU: /home/lukas/tmp/cvc5/build/deps/include/
-- Performing Test CVC5_NEED_INT64_T_OVERLOADS
-- Performing Test CVC5_NEED_INT64_T_OVERLOADS - Failed
-- Performing Test CVC5_NEED_HASH_UINT64_T_OVERLOAD
-- Performing Test CVC5_NEED_HASH_UINT64_T_OVERLOAD - Failed
-- Looking for unistd.h
-- Looking for unistd.h - found
-- Looking for sys/wait.h
-- Looking for sys/wait.h - found
-- Looking for C++ include ext/stdio_filebuf.h
-- Looking for C++ include ext/stdio_filebuf.h - found
-- Looking for clock_gettime
-- Looking for clock_gettime - found
-- Looking for ffs
-- Looking for ffs - found
-- Looking for optreset
-- Looking for optreset - not found
-- Looking for sigaltstack
-- Looking for sigaltstack - found
-- Looking for strerror_r
-- Looking for strerror_r - found
-- Looking for strtok_r
-- Looking for strtok_r - found
-- Looking for setitimer
-- Looking for setitimer - found
-- Performing Test STRERROR_R_CHAR_P
-- Performing Test STRERROR_R_CHAR_P - Failed
-- Performing Test COMPILER_HAS_HIDDEN_VISIBILITY
-- Performing Test COMPILER_HAS_HIDDEN_VISIBILITY - Success
-- Performing Test COMPILER_HAS_HIDDEN_INLINE_VISIBILITY
-- Performing Test COMPILER_HAS_HIDDEN_INLINE_VISIBILITY - Success
-- Performing Test COMPILER_HAS_DEPRECATED_ATTR
-- Performing Test COMPILER_HAS_DEPRECATED_ATTR - Success

cvc5 1.0.8

Build profile             : production

Assertions                : off
Debug symbols             : off
Debug context mem mgr     : off

Muzzle                    : off
Statistics                : on
Tracing                   : off

ASan                      : off
UBSan                     : off
TSan                      : off
Coverage (gcov)           : off
Profiling (gprof)         : off
Unit tests                : off
Valgrind                  : off

Shared build              : off
Python bindings           : off
Java bindings             : off
Interprocedural opt.      : off

CryptoMiniSat             : off
GLPK                      : off
Kissat                    : off
LibPoly                   : on (local)
CoCoALib                  : off
MP library                : gmp (system)
Editline                  : off

Api docs                  : off

CPPLAGS (-D...): NDEBUG CVC5_STATISTICS_ON CVC5_USE_POLY
CXXFLAGS       : -O3 -Wall -Wsuggest-override -Wnon-virtual-dtor -Wimplicit-fallthrough -Wshadow -fno-extern-tls-init -Wno-class-memaccess
CFLAGS         : -O3 -Wall -fexceptions -Wimplicit-fallthrough -Wshadow
Linker flags   :  -fuse-ld=gold

Install prefix : /home/lukas/tmp/cvc5/build/install

cvc5 license: modified BSD

Note that this configuration is NOT built against any GPL'ed libraries, so
it is covered by the (modified) BSD license.  To build against GPL'ed
libraries which can improve cvc5's performance on arithmetic and bit-vector
logics, use the 'configure.sh' script to re-configure with '--best --gpl'.

Now change to 'build' and type 'make', followed by 'make check' or 'make install'.

-- Configuring done (4.2s)
-- Generating done (0.2s)
-- Build files have been written to: /home/lukas/tmp/cvc5/build

make output

[  0%] Creating directories for 'SymFPU-EP'
[  0%] Creating directories for 'Poly-EP'
[  0%] Generating type_enumerator.cpp
[  1%] Generating options/options.stamp
[  1%] Building CXX object src/context/CMakeFiles/cvc5context.dir/context.cpp.o
[  0%] Creating directories for 'CaDiCaL-EP'
-- Found Git: /usr/bin/git (found version "2.42.0")
fatal: No names found, cannot describe anything.
[  1%] Built target gen-versioninfo
[  1%] Performing download step (download, verify and extract) for 'SymFPU-EP'
[  1%] Performing download step (download, verify and extract) for 'CaDiCaL-EP'
[  1%] Performing download step (download, verify and extract) for 'Poly-EP'
[  1%] Generating Trace_tags.h
[  1%] Building CXX object src/context/CMakeFiles/cvc5context.dir/context_mm.cpp.o
[  1%] Built target gen-options
[  1%] Generating kind.h
[  1%] Built target gen-tags
[  1%] Generating rewrites.{h,cpp}
[  1%] Built target gen-rewrites
[  1%] Generating metakind.h
[  1%] Generating theory_traits.h
-- SymFPU-EP download command succeeded.  See also /home/lukas/tmp/cvc5/build/deps/src/SymFPU-EP-stamp/SymFPU-EP-download-*.log
[  1%] No update step for 'SymFPU-EP'
[  1%] No patch step for 'SymFPU-EP'
[  1%] Generating node_manager.h
[  1%] No configure step for 'SymFPU-EP'
[  2%] No build step for 'SymFPU-EP'
[  2%] Generating type_checker.cpp
[  2%] Built target cvc5context
[  2%] Performing install step for 'SymFPU-EP'
[  2%] Generating smt2_tokens.h
[  2%] Built target gen-tokens
-- SymFPU-EP install command succeeded.  See also /home/lukas/tmp/cvc5/build/deps/src/SymFPU-EP-stamp/SymFPU-EP-install-*.log
[  2%] Completed 'SymFPU-EP'
[  3%] Building CXX object src/base/CMakeFiles/cvc5base.dir/check.cpp.o
[  3%] Built target SymFPU-EP
[  3%] Building CXX object src/base/CMakeFiles/cvc5base.dir/configuration.cpp.o
-- Poly-EP download command succeeded.  See also /home/lukas/tmp/cvc5/build/deps/src/Poly-EP-stamp/Poly-EP-download-*.log
[  3%] No update step for 'Poly-EP'
-- CaDiCaL-EP download command succeeded.  See also /home/lukas/tmp/cvc5/build/deps/src/CaDiCaL-EP-stamp/CaDiCaL-EP-download-*.log
[  3%] Performing patch step for 'Poly-EP'
[  3%] No update step for 'CaDiCaL-EP'
[  3%] Generating rewriter_tables.h
[  3%] No patch step for 'CaDiCaL-EP'
-- Poly-EP patch command succeeded.  See also /home/lukas/tmp/cvc5/build/deps/src/Poly-EP-stamp/Poly-EP-patch-*.log
[  3%] Performing configure step for 'CaDiCaL-EP'
[  3%] Performing configure step for 'Poly-EP'
-- CaDiCaL-EP configure command succeeded.  See also /home/lukas/tmp/cvc5/build/deps/src/CaDiCaL-EP-stamp/CaDiCaL-EP-configure-*.log
[  3%] Performing build step for 'CaDiCaL-EP'
[  3%] Built target gen-theory
[  3%] Building CXX object src/base/CMakeFiles/cvc5base.dir/exception.cpp.o
[  3%] Generating type_properties.h
[  3%] Building CXX object src/base/CMakeFiles/cvc5base.dir/listener.cpp.o
[  3%] Building CXX object src/base/CMakeFiles/cvc5base.dir/output.cpp.o
-- Poly-EP configure command succeeded.  See also /home/lukas/tmp/cvc5/build/deps/src/Poly-EP-stamp/Poly-EP-configure-*.log
[  4%] Performing build step for 'Poly-EP'
[  4%] Building CXX object src/base/CMakeFiles/cvc5base.dir/versioninfo.cpp.o
[  5%] Generating kind.cpp
[  5%] Built target cvc5base
[  5%] Generating type_properties.cpp
[  5%] Generating metakind.cpp
[  5%] Generating node_manager.cpp
[  5%] Built target gen-expr
[  6%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/commands.cpp.o
[  6%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/command_status.cpp.o
[  6%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/input.cpp.o
[  6%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/lexer.cpp.o
[  6%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/parser.cpp.o
[  6%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/parse_op.cpp.o
[  6%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/parser_state.cpp.o
[  6%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/parser_utils.cpp.o
[  6%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/smt2/smt2_state.cpp.o
[  7%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/smt2/smt2_cmd_parser.cpp.o
[  7%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/smt2/smt2_lexer.cpp.o
[  7%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/smt2/smt2_parser.cpp.o
[  7%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/smt2/smt2_term_parser.cpp.o
[  7%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/sym_manager.cpp.o
-- Poly-EP build command succeeded.  See also /home/lukas/tmp/cvc5/build/deps/src/Poly-EP-stamp/Poly-EP-build-*.log
[  7%] Performing install step for 'Poly-EP'
-- Poly-EP install command succeeded.  See also /home/lukas/tmp/cvc5/build/deps/src/Poly-EP-stamp/Poly-EP-install-*.log
[  7%] Performing cleanup step for 'Poly-EP'
[  7%] Completed 'Poly-EP'
[  7%] Built target Poly-EP
[  7%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/symbol_table.cpp.o
[  7%] Building CXX object src/parser/CMakeFiles/cvc5parser-objs.dir/tokens.cpp.o
[  7%] Built target cvc5parser-objs
[  7%] Building CXX object src/parser/CMakeFiles/cvc5parserapi-objs.dir/__/api/cpp/cvc5_parser.cpp.o
-- CaDiCaL-EP build command succeeded.  See also /home/lukas/tmp/cvc5/build/deps/src/CaDiCaL-EP-stamp/CaDiCaL-EP-build-*.log
[  7%] Performing install step for 'CaDiCaL-EP'
[  7%] Built target cvc5parserapi-objs
-- CaDiCaL-EP install command succeeded.  See also /home/lukas/tmp/cvc5/build/deps/src/CaDiCaL-EP-stamp/CaDiCaL-EP-install-*.log
[  7%] Completed 'CaDiCaL-EP'
[  7%] Built target CaDiCaL-EP
[  7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/api/cpp/cvc5.cpp.o
[  7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/decision/assertion_list.cpp.o
[  7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/decision/justification_strategy.cpp.o
[  7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/api/cpp/cvc5_types.cpp.o
[  7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/api/cpp/cvc5_proof_rule.cpp.o
[  7%] Building CXX object src/CMakeFiles/cvc5-obj.dir/decision/justify_info.cpp.o
[  8%] Building CXX object src/CMakeFiles/cvc5-obj.dir/decision/decision_engine.cpp.o
[  8%] Building CXX object src/CMakeFiles/cvc5-obj.dir/decision/justify_cache.cpp.o
[  8%] Building CXX object src/CMakeFiles/cvc5-obj.dir/decision/justify_stack.cpp.o
[  8%] Building CXX object src/CMakeFiles/cvc5-obj.dir/decision/justify_stats.cpp.o
[  8%] Building C object src/CMakeFiles/cvc5-obj.dir/lib/clock_gettime.c.o
[  8%] Building C object src/CMakeFiles/cvc5-obj.dir/lib/ffs.c.o
[  8%] Building C object src/CMakeFiles/cvc5-obj.dir/lib/strtok_r.c.o
[ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/omt/bitvector_optimizer.cpp.o
[ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/omt/integer_optimizer.cpp.o
[ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/omt/omt_optimizer.cpp.o
[ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/language.cpp.o
[ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/managed_streams.cpp.o
[ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/option_exception.cpp.o
[ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/options_handler.cpp.o
[ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/assertion_pipeline.cpp.o
[ 10%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/learned_literal_manager.cpp.o
[ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/ackermann.cpp.o
[ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/apply_substs.cpp.o
[ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bool_to_bv.cpp.o
[ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_eager_atoms.cpp.o
[ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_gauss.cpp.o
[ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_intro_pow2.cpp.o
[ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_to_bool.cpp.o
[ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/bv_to_int.cpp.o
[ 11%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/extended_rewriter_pass.cpp.o
[ 12%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/foreign_theory_rewrite.cpp.o
[ 12%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/fun_def_fmf.cpp.o
[ 12%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/global_negate.cpp.o
[ 12%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/ho_elim.cpp.o
[ 12%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/int_to_bv.cpp.o
[ 12%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/ite_removal.cpp.o
[ 12%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/ite_simp.cpp.o
[ 12%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/learned_rewrite.cpp.o
[ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/miplib_trick.cpp.o
[ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/nl_ext_purify.cpp.o
[ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/non_clausal_simp.cpp.o
[ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/pseudo_boolean_processor.cpp.o
[ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/quantifiers_preprocess.cpp.o
[ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/real_to_int.cpp.o
[ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/rewrite.cpp.o
[ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/sep_skolem_emp.cpp.o
[ 13%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/sort_infer.cpp.o
[ 14%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/static_learning.cpp.o
[ 14%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/static_rewrite.cpp.o
[ 14%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/strings_eager_pp.cpp.o
[ 14%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/sygus_inference.cpp.o
[ 14%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/synth_rew_rules.cpp.o
[ 14%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/theory_preprocess.cpp.o
[ 14%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/passes/unconstrained_simplifier.cpp.o
[ 14%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/preprocessing_pass.cpp.o
[ 14%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/preprocessing_pass_context.cpp.o
[ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/preprocessing_pass_registry.cpp.o
[ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/util/boolean_simplification.cpp.o
[ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/preprocessing/util/ite_utilities.cpp.o
[ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/printer/ast/ast_printer.cpp.o
[ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/printer/let_binding.cpp.o
[ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/printer/printer.cpp.o
[ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/printer/smt2/smt2_printer.cpp.o
[ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alf/alf_node_converter.cpp.o
[ 15%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alf/alf_print_channel.cpp.o
[ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/alf/alf_proof_rule.cpp.o
[ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/annotation_proof_generator.cpp.o
[ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/assumption_proof_generator.cpp.o
[ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/buffered_proof_generator.cpp.o
[ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/conv_proof_generator.cpp.o
[ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/conv_seq_proof_generator.cpp.o
[ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/dot/dot_printer.cpp.o
[ 16%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/eager_proof_generator.cpp.o
[ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lazy_proof.cpp.o
[ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lazy_proof_chain.cpp.o
[ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lazy_tree_proof_generator.cpp.o
[ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_list_sc_node_converter.cpp.o
[ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_node_converter.cpp.o
[ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_post_processor.cpp.o
[ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_printer.cpp.o
[ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_print_channel.cpp.o
[ 17%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/lfsc/lfsc_util.cpp.o
[ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/method_id.cpp.o
[ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/print_expr.cpp.o
[ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof.cpp.o
[ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_checker.cpp.o
[ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_ensure_closed.cpp.o
[ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_generator.cpp.o
[ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_letify.cpp.o
[ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_node.cpp.o
[ 19%] Building CXX object src/CMakeFiles/cvc5-obj.dir/proof/proof_node_algorithm.cpp.o
 --- I had to crop because GitHub does not allow long comments ---
 --- There was an error creating your Issue: body is too long (maximum is 65536 characters). ---
[ 80%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/theory_engine_statistics.cpp.o
[ 80%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/theory_inference.cpp.o
[ 80%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/theory_inference_manager.cpp.o
[ 80%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/theory_model.cpp.o
[ 80%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/theory_model_builder.cpp.o
[ 80%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/theory_preprocessor.cpp.o
[ 80%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/theory_rewriter.cpp.o
[ 80%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/theory_state.cpp.o
[ 80%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/trust_substitutions.cpp.o
[ 82%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/type_set.cpp.o
[ 82%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/cardinality_extension.cpp.o
[ 82%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/conversions_solver.cpp.o
[ 82%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/equality_engine.cpp.o
[ 82%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/equality_engine_iterator.cpp.o
[ 82%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/eq_proof.cpp.o
[ 82%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/function_const.cpp.o
[ 82%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/lambda_lift.cpp.o
[ 83%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/proof_checker.cpp.o
[ 83%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/proof_equality_engine.cpp.o
[ 83%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/ho_extension.cpp.o
[ 83%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/symmetry_breaker.cpp.o
[ 83%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/theory_uf.cpp.o
[ 83%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/theory_uf_model.cpp.o
[ 83%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/theory_uf_rewriter.cpp.o
[ 83%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/theory_uf_type_rules.cpp.o
[ 83%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/uf/type_enumerator.cpp.o
[ 84%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/valuation.cpp.o
[ 84%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/annotation_elim_node_converter.cpp.o
[ 84%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/array_store_all.cpp.o
[ 84%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/ascription_type.cpp.o
[ 84%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/attribute.cpp.o
[ 84%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/bound_var_manager.cpp.o
[ 84%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/cardinality_constraint.cpp.o
[ 84%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/codatatype_bound_variable.cpp.o
[ 84%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/elim_shadow_converter.cpp.o
[ 85%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/emptyset.cpp.o
[ 85%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/emptybag.cpp.o
[ 85%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/function_array_const.cpp.o
[ 85%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/match_trie.cpp.o
[ 85%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/nary_match_trie.cpp.o
[ 85%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/nary_term_util.cpp.o
[ 85%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/node.cpp.o
[ 85%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/node_algorithm.cpp.o
[ 85%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/node_builder.cpp.o
[ 86%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/node_converter.cpp.o
[ 86%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/node_trie.cpp.o
[ 86%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/node_trie_algorithm.cpp.o
[ 86%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/node_traversal.cpp.o
[ 86%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/node_value.cpp.o
[ 86%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/oracle_caller.cpp.o
[ 86%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/sequence.cpp.o
[ 86%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/skolem_manager.cpp.o
[ 87%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/subtype_elim_node_converter.cpp.o
[ 87%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/term_canonize.cpp.o
[ 87%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/term_context.cpp.o
[ 87%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/term_context_node.cpp.o
[ 87%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/term_context_stack.cpp.o
[ 87%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/type_matcher.cpp.o
[ 87%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/type_node.cpp.o
[ 87%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/dtype.cpp.o
[ 87%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/dtype_cons.cpp.o
[ 88%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/dtype_selector.cpp.o
[ 88%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/subs.cpp.o
[ 88%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/sygus_datatype.cpp.o
[ 88%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/sygus_grammar.cpp.o
[ 88%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/variadic_trie.cpp.o
[ 88%] Building CXX object src/CMakeFiles/cvc5-obj.dir/rewriter/basic_rewrite_rcons.cpp.o
[ 88%] Building CXX object src/CMakeFiles/cvc5-obj.dir/rewriter/rewrite_db.cpp.o
[ 88%] Building CXX object src/CMakeFiles/cvc5-obj.dir/rewriter/rewrite_db_proof_cons.cpp.o
[ 88%] Building CXX object src/CMakeFiles/cvc5-obj.dir/rewriter/rewrite_db_term_process.cpp.o
[ 89%] Building CXX object src/CMakeFiles/cvc5-obj.dir/rewriter/rewrite_proof_rule.cpp.o
[ 89%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/bitvector.cpp.o
[ 89%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/cocoa_globals.cpp.o
[ 89%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/cardinality.cpp.o
[ 89%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/cardinality_class.cpp.o
[ 89%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/didyoumean.cpp.o
[ 89%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/divisible.cpp.o
[ 89%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/finite_field_value.cpp.o
[ 89%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/floatingpoint.cpp.o
[ 91%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/floatingpoint_size.cpp.o
[ 91%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/floatingpoint_literal_symfpu.cpp.o
[ 91%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/floatingpoint_literal_symfpu_traits.cpp.o
[ 91%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/index.cpp.o
[ 91%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/ostream_util.cpp.o
[ 91%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/poly_util.cpp.o
[ 91%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/random.cpp.o
[ 91%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/resource_manager.cpp.o
[ 91%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/result.cpp.o
[ 92%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/real_algebraic_number_poly_imp.cpp.o
[ 92%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/regexp.cpp.o
[ 92%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/roundingmode.cpp.o
[ 92%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/safe_print.cpp.o
[ 92%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/sampler.cpp.o
[ 92%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/sexpr.cpp.o
[ 92%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/smt2_quote_string.cpp.o
[ 92%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/statistics_public.cpp.o
[ 93%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/statistics_registry.cpp.o
[ 93%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/statistics_stats.cpp.o
[ 93%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/statistics_value.cpp.o
[ 93%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/string.cpp.o
[ 93%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/synth_result.cpp.o
[ 93%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/uninterpreted_sort_value.cpp.o
[ 93%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/utility.cpp.o
[ 93%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/rational_gmp_imp.cpp.o
[ 93%] Building CXX object src/CMakeFiles/cvc5-obj.dir/util/integer_gmp_imp.cpp.o
[ 94%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/arith_options.cpp.o
[ 94%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/arrays_options.cpp.o
[ 94%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/base_options.cpp.o
[ 94%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/booleans_options.cpp.o
[ 94%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/builtin_options.cpp.o
[ 94%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/bv_options.cpp.o
[ 94%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/datatypes_options.cpp.o
[ 94%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/decision_options.cpp.o
[ 94%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/expr_options.cpp.o
[ 95%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/ff_options.cpp.o
[ 95%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/fp_options.cpp.o
[ 95%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/main_options.cpp.o
[ 95%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/parallel_options.cpp.o
[ 95%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/parser_options.cpp.o
[ 95%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/printer_options.cpp.o
[ 95%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/proof_options.cpp.o
[ 95%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/prop_options.cpp.o
[ 95%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/quantifiers_options.cpp.o
[ 96%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/sep_options.cpp.o
[ 96%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/sets_options.cpp.o
[ 96%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/smt_options.cpp.o
[ 96%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/strings_options.cpp.o
[ 96%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/theory_options.cpp.o
[ 96%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/uf_options.cpp.o
[ 96%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/io_utils.cpp.o
[ 96%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/options.cpp.o
[ 97%] Building CXX object src/CMakeFiles/cvc5-obj.dir/options/options_public.cpp.o
[ 97%] Building CXX object src/CMakeFiles/cvc5-obj.dir/main/options.cpp.o
[ 97%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/kind.cpp.o
[ 97%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/metakind.cpp.o
[ 97%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/node_manager.cpp.o
[ 97%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/type_checker.cpp.o
[ 97%] Building CXX object src/CMakeFiles/cvc5-obj.dir/expr/type_properties.cpp.o
[ 97%] Building CXX object src/CMakeFiles/cvc5-obj.dir/rewriter/rewrites.cpp.o
[ 97%] Building CXX object src/CMakeFiles/cvc5-obj.dir/theory/type_enumerator.cpp.o
[ 97%] Built target cvc5-obj
[ 97%] Building CXX object src/main/CMakeFiles/main.dir/portfolio_driver.cpp.o
[ 97%] Building CXX object src/main/CMakeFiles/main.dir/interactive_shell.cpp.o
[ 97%] Building CXX object src/main/CMakeFiles/main.dir/command_executor.cpp.o
[ 97%] Building CXX object src/main/CMakeFiles/main.dir/signal_handlers.cpp.o
[ 97%] Building CXX object src/main/CMakeFiles/main.dir/time_limit.cpp.o
[ 98%] Building CXX object src/main/CMakeFiles/main.dir/options.cpp.o
[100%] Linking CXX static library libcvc5.a
[100%] Built target cvc5
[100%] Linking CXX static library libcvc5parser.a
[100%] Built target cvc5parser
[100%] Built target main
[100%] Building CXX object src/main/CMakeFiles/main-test.dir/driver_unified.cpp.o
[100%] Building CXX object src/main/CMakeFiles/cvc5-bin.dir/driver_unified.cpp.o
[100%] Building CXX object src/main/CMakeFiles/cvc5-bin.dir/main.cpp.o
[100%] Linking CXX executable ../../bin/cvc5
[100%] Linking CXX static library libmain-test.a
[100%] Built target main-test
/usr/bin/ld.gold: error: cannot mix -static with dynamic object /usr/lib/libgmp.so
collect2: error: ld returned 1 exit status
make[2]: *** [src/main/CMakeFiles/cvc5-bin.dir/build.make:132: bin/cvc5] Error 1
make[1]: *** [CMakeFiles/Makefile2:1059: src/main/CMakeFiles/cvc5-bin.dir/all] Error 2
make: *** [Makefile:146: all] Error 2
Selebrator commented 1 year ago

I should have added that I would expect the build tool to build libgmp.a in this case, as is done with all other missing dependencies. At least that is what I thought the --auto-download option is for.

mpreiner commented 12 months ago

The build system only builds a missing dependency if it is not found at all. In your case it does find the shared library, but it can't be used in a static build since it was not compiled with PIC enabled. We could restrict the library suffixes CMAKE_FIND_LIBRARY_SUFFIXES when doing a static build, but I'm not sure if this will break any other dependencies. I'll have a look. In the meantime it may be better to install the static GMP library on your system (https://aur.archlinux.org/packages/libgmp-static).