Compiling on Redhat 7

[sjreilly1960]

Hi, I'm trying to compile boolector (to be used in Yosys) on Redhat 7 and get an error in the make -C build -j$(nproc) command; Redhat 7 uses cmake3 rather than cmake, so I had to modilfy the configure.sh to call that;

`./configure.sh -- The C compiler identification is GNU 4.8.5 -- The CXX compiler identification is GNU 4.8.5 -- Check for working C compiler: /usr/bin/cc -- Check for working C compiler: /usr/bin/cc - works -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Detecting C compile features -- Detecting C compile features - done -- Check for working CXX compiler: /usr/bin/c++ -- Check for working CXX compiler: /usr/bin/c++ - works -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Detecting CXX compile features -- Detecting CXX compile features - done -- LIB directory is '/site/apps/yosys/boolector/build/lib' -- BIN directory is '/site/apps/yosys/boolector/build/bin' -- Performing Test HAVE_FLAG_std_gnu99 -- Performing Test HAVE_FLAG_std_gnu99 - Success -- Configuring with C flag '-std=gnu99' -- Configuring with CXX flag '-std=gnu++11' -- Performing Test HAVE_FLAG_W -- Performing Test HAVE_FLAG_W - Success -- Configuring with C flag '-W' -- Configuring with CXX flag '-W' -- Performing Test HAVE_FLAG_Wall -- Performing Test HAVE_FLAG_Wall - Success -- Configuring with C flag '-Wall' -- Configuring with CXX flag '-Wall' -- Performing Test HAVE_FLAG_Wextra -- Performing Test HAVE_FLAG_Wextra - Success -- Configuring with C flag '-Wextra' -- Configuring with CXX flag '-Wextra' -- Performing Test HAVE_FLAG_Wredundant_decls -- Performing Test HAVE_FLAG_Wredundant_decls - Success -- Configuring with C flag '-Wredundant-decls' -- Configuring with CXX flag '-Wredundant-decls' -- No build type set, options are: Debug;Release -- Building Release build -- Performing Test HAVE_FLAG_O3 -- Performing Test HAVE_FLAG_O3 - Success -- Configuring with C flag '-O3' -- Configuring with CXX flag '-O3' -- Performing Test HAVE_SIGNALS -- Performing Test HAVE_SIGNALS - Success -- Performing Test HAVE_TIME_UTILS -- Performing Test HAVE_TIME_UTILS - Success -- Performing Test HAVE_NO_EXPORT_DYNAMIC -- Performing Test HAVE_NO_EXPORT_DYNAMIC - Success -- Found Btor2Tools: /site/apps/yosys/boolector/deps/install/include
-- Found Btor2Tools library: /site/apps/yosys/boolector/deps/install/lib/libbtor2parser.a -- Looking for pthread.h -- Looking for pthread.h - found -- Performing Test CMAKE_HAVE_LIBC_PTHREAD -- Performing Test CMAKE_HAVE_LIBC_PTHREAD - Failed -- Check if compiler accepts -pthread -- Check if compiler accepts -pthread - yes -- Found Threads: TRUE
-- Found Lingeling: /site/apps/yosys/boolector/deps/install/include
-- Found Lingeling library: /site/apps/yosys/boolector/deps/install/lib/liblgl.a -- Could NOT find CaDiCaL (missing: CaDiCaL_INCLUDE_DIR CaDiCaL_LIBRARIES) -- Could NOT find CryptoMiniSat (missing: CryptoMiniSat_INCLUDE_DIR CryptoMiniSat_LIBRARIES) -- Could NOT find PicoSAT (missing: PicoSAT_INCLUDE_DIR PicoSAT_LIBRARIES) -- Could NOT find MiniSat (missing: MiniSat_INCLUDE_DIR MiniSat_LIBRARIES) -- Found Git: /usr/bin/git (found version "1.8.3.1") -- Configuring done -- Generating done -- Build files have been written to: /site/apps/yosys/boolector/build/googletest [ 11%] Performing update step for 'googletest' [ 22%] No configure step for 'googletest' [ 33%] No build step for 'googletest' [ 44%] No install step for 'googletest' [ 55%] No test step for 'googletest' [ 66%] Completed 'googletest' [100%] Built target googletest -- Found PythonInterp: /usr/bin/python (found version "2.7.5") -- Build type: Release -- Shared build: no -- ASAN support: no -- UBSAN support: no -- Assertions enabled: no -- gcov support: no -- gprof support: no -- Logging support: no -- Python bindings: no -- Time statistics: no -- CaDiCaL: no -- CryptoMiniSat: no -- Lingeling: yes -- MiniSat: no -- PicoSAT: no -- GMP: no -- Configuring done -- Generating done -- Build files have been written to: /site/apps/yosys/boolector/build

make -C build -j$(nproc) make: Entering directory /site/apps/yosys/boolector/build' make[1]: Entering directory/site/apps/yosys/boolector/build' make[2]: Entering directory /site/apps/yosys/boolector/build' make[2]: Entering directory/site/apps/yosys/boolector/build' make[2]: Leaving directory /site/apps/yosys/boolector/build' [ 1%] Built target gtest make[2]: Entering directory/site/apps/yosys/boolector/build' Scanning dependencies of target boolector make[2]: Leaving directory /site/apps/yosys/boolector/build' [ 2%] Built target gtest_main make[2]: Leaving directory/site/apps/yosys/boolector/build' make[2]: Entering directory /site/apps/yosys/boolector/build' [ 2%] Building C object src/CMakeFiles/boolector.dir/btorclone.c.o [ 4%] Building C object src/CMakeFiles/boolector.dir/btorcore.c.o [ 4%] Building C object src/CMakeFiles/boolector.dir/btorsat.c.o [ 5%] Building C object src/CMakeFiles/boolector.dir/parser/btorbtor2.c.o [ 5%] Building C object src/CMakeFiles/boolector.dir/preprocess/btorskel.c.o [ 7%] Building C object src/CMakeFiles/boolector.dir/sat/btorlgl.c.o [ 7%] Linking CXX static library ../lib/libboolector.a make[2]: Leaving directory/site/apps/yosys/boolector/build' [ 52%] Built target boolector make[2]: Entering directory /site/apps/yosys/boolector/build' make[2]: Entering directory/site/apps/yosys/boolector/build' Scanning dependencies of target boolector-bin make[2]: Leaving directory /site/apps/yosys/boolector/build' make[2]: Entering directory/site/apps/yosys/boolector/build' [ 52%] Building C object src/CMakeFiles/boolector-bin.dir/btormain.c.o Scanning dependencies of target btormc make[2]: Leaving directory /site/apps/yosys/boolector/build' make[2]: Entering directory/site/apps/yosys/boolector/build' [ 52%] Building C object src/CMakeFiles/btormc.dir/btormcmain.c.o [ 52%] Linking CXX executable ../bin/btormc [ 52%] Linking CXX executable ../bin/boolector /usr/bin/ld: cannot find -lstdc++ /usr/bin/ld: cannot find -lm /usr/bin/ld: cannot find -lpthread /usr/bin/ld: cannot find -lc collect2: error: ld returned 1 exit status make[2]: [bin/btormc] Error 1 make[2]: Leaving directory `/site/apps/yosys/boolector/build' make[1]: [src/CMakeFiles/btormc.dir/all] Error 2 make[1]: Waiting for unfinished jobs.... /usr/bin/ld: cannot find -lstdc++ /usr/bin/ld: cannot find -lm /usr/bin/ld: cannot find -lpthread /usr/bin/ld: cannot find -lc collect2: error: ld returned 1 exit status make[2]: [bin/boolector] Error 1 make[2]: Leaving directory /site/apps/yosys/boolector/build' make[1]: *** [src/CMakeFiles/boolector-bin.dir/all] Error 2 make[1]: Leaving directory/site/apps/yosys/boolector/build' make: *** [all] Error 2 make: Leaving directory /site/apps/yosys/boolector/build'

It all seemed to be going well until that point. TIA, Steve

[aytey]

Try passing in -shared to Boolector’s configure script.

Or install the static glibc libraries on CentOS.

[sjreilly1960]

@andrewvaughanj Many thanks for your help. I already had all the glibc packages installed, but using "./configure.sh --shared" allowed the compile to complete.

[aytey]

I don't have a CentOS 7 VM immediately to hand, so I can't check this, but I think you need glibc-static to get the static versions.

Anyway, great that it is working for you!