Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Dependency on libpoly not relocatable #10681

Open
gussmith23 opened this issue Apr 24, 2024 · 0 comments
Open

Dependency on libpoly not relocatable #10681

gussmith23 opened this issue Apr 24, 2024 · 0 comments
Assignees

Comments

@gussmith23
Copy link

Describe the bug

#10440 made cvc5's build relocatable -- great!! Thank you so much!

It seems like there might be lingering hardcoded paths, though.

For example, I had to do the following change on Mac to fix libcvc5.1.dylib. A similar patchelf command would have been needed on Linux, I think:

$ install_name_tool -change "/Users/runner/work/lakeroad/lakeroad/cvc5/build/deps/lib/libpoly.0.dylib" @rpath/libpoly.0.dylib "/Users/gus/Downloads/lakeroad 3/deps/cvc5/lib/libcvc5.1.dylib"
$ install_name_tool -change "/Users/runner/work/lakeroad/lakeroad/cvc5/build/deps/lib/libpolyxx.0.dylib" @rpath/libpolyxx.0.dylib "/Users/gus/Downloads/lakeroad 3/deps/cvc5/lib/libcvc5.1.dylib"

The other libraries seem to not be hardcoding paths, but specifically this libpoly path is hardcoded.

Command line arguments: Command line arguments passed to cvc5 if applicable
cvc5 version/commit: 1d05a49
Operating system: MacOS 13 x64

configure.sh output

+ cd ./build
-- The C compiler identification is AppleClang 15.0.0.15000040
+ make -j 2
-- The CXX compiler identification is AppleClang 15.0.0.15000040
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Check for working C compiler: /Applications/Xcode_15.0.1.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/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: /Applications/Xcode_15.0.1.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/c++ - skipped
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Found Git: /usr/local/bin/git (found version "2.44.0")
fatal: not a git repository (or any of the parent directories): .git
-- 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 - Success
-- Configuring with C flag '-Wno-unused-private-field'
-- Performing Test HAVE_CXX_FLAG_Wunused_private_field
-- Performing Test HAVE_CXX_FLAG_Wunused_private_field - Success
-- Configuring with CXX flag '-Wno-unused-private-field'
-- 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 - Failed
-- Performing Test HAVE_CXX_FLAG_Wclass_memaccess
-- Performing Test HAVE_CXX_FLAG_Wclass_memaccess - Failed
-- Disabling unit tests since assertions are disabled.
-- Found Python: /Users/runner/hostedtoolcache/Python/3.10.14/x64/bin/python3 (found version "3.10.14") found components: Interpreter
-- Found GMP (unknown version): /usr/local/lib/libgmp.dylib
-- Looking for getc_unlocked
-- Looking for getc_unlocked - not found
-- Building CaDiCaL rel-1.7.4: /Users/runner/work/lakeroad/lakeroad/cvc5/build/deps/lib/libcadical.a
-- Building Poly 0.1.13: /Users/runner/work/lakeroad/lakeroad/cvc5/build/deps/lib/libpoly.dylib, /Users/runner/work/lakeroad/lakeroad/cvc5/build/deps/lib/libpolyxx.dylib
-- Building SymFPU: /Users/runner/work/lakeroad/lakeroad/cvc5/build/deps/include/
-- Performing Test CVC5_NEED_INT64_T_OVERLOADS
-- Performing Test CVC5_NEED_INT64_T_OVERLOADS - Success
-- 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 - not found
-- Looking for clock_gettime
-- Looking for clock_gettime - found
-- Looking for ffs
-- Looking for ffs - found
-- Looking for optreset
-- Looking for optreset - 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.1.2

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              : on
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 -Wno-unused-private-field -Wsuggest-override -Wnon-virtual-dtor -Wimplicit-fallthrough -Wshadow
CFLAGS         : -O3 -Wall -Wno-unused-private-field -fexceptions -Wimplicit-fallthrough -Wshadow
Linker flags   : 

Install prefix : /Users/runner/work/lakeroad/lakeroad/lakeroad/deps/cvc5

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 (17.8s)
-- Generating done (1.6s)
-- Build files have been written to: /Users/runner/work/lakeroad/lakeroad/cvc5/build
@daniel-larraz daniel-larraz self-assigned this Apr 24, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants