Compilation issue with 5.6.3 for SageMath 8.3 (archlinux gcc 8.1.1)

[videlec]

Compiling cryptominisat 5.6.3 ends with a compilation error

[ 84%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/cryptominisat.cpp.o
cd /opt/sage/local/var/tmp/sage/build/cryptominisat-5.6.3/src/cmsat5-src && /usr/lib/ccache/bin/g++  -DBOOST_TEST_DYN_LINK -DUSE_GAUSS -DUSE_M4RI -DUSE_ZLIB -Dlibcryptominisat5_EXPORTS -I/opt
/sage/local/include -I/opt/sage/local/var/tmp/sage/build/cryptominisat-5.6.3/src -I/opt/sage/local/var/tmp/sage/build/cryptominisat-5.6.3/src/cmsat5-src  -mtune=native -Wall -Wextra -Wunused 
-Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreacha
ble-code -ggdb3 -Wlogical-op -Wrestrict -Wnull-dereference -Wdouble-promotion -Wshadow -Wformat=2 -Wextra-semi -pedantic -Wno-class-memaccess -fPIC   -g -pthread -O2 -mtune=native -fPIC -std=
gnu++11 -o CMakeFiles/libcryptominisat5.dir/cryptominisat.cpp.o -c /opt/sage/local/var/tmp/sage/build/cryptominisat-5.6.3/src/src/cryptominisat.cpp
../src/cryptominisat.cpp:1059:17: error: no declaration matches 'void CMSat::SATSolver::start_getting_small_clauses(uint32_t, uint32_t)'
 void DLL_PUBLIC SATSolver::start_getting_small_clauses(uint32_t max_len, uint32_t max_glue)
                 ^~~~~~~~~
../src/cryptominisat.cpp:1059:17: note: no functions named 'void CMSat::SATSolver::start_getting_small_clauses(uint32_t, uint32_t)'
In file included from ../src/cryptominisat.cpp:24:
../../../../../../../include/cryptominisat5/cryptominisat.h:41:11: note: 'class CMSat::SATSolver' defined here
     class SATSolver
           ^~~~~~~~~
../src/cryptominisat.cpp:1065:17: error: no declaration matches 'bool CMSat::SATSolver::get_next_small_clause(std::vector<CMSat::Lit>&)'
 bool DLL_PUBLIC SATSolver::get_next_small_clause(std::vector<Lit>& out)
                 ^~~~~~~~~
../src/cryptominisat.cpp:1065:17: note: no functions named 'bool CMSat::SATSolver::get_next_small_clause(std::vector<CMSat::Lit>&)'
In file included from ../src/cryptominisat.cpp:24:
../../../../../../../include/cryptominisat5/cryptominisat.h:41:11: note: 'class CMSat::SATSolver' defined here
     class SATSolver
           ^~~~~~~~~
../src/cryptominisat.cpp:1071:17: error: no declaration matches 'void CMSat::SATSolver::end_getting_small_clauses()'
 void DLL_PUBLIC SATSolver::end_getting_small_clauses()
                 ^~~~~~~~~
../src/cryptominisat.cpp:1071:17: note: no functions named 'void CMSat::SATSolver::end_getting_small_clauses()'
In file included from ../src/cryptominisat.cpp:24:
../../../../../../../include/cryptominisat5/cryptominisat.h:41:11: note: 'class CMSat::SATSolver' defined here
     class SATSolver
           ^~~~~~~~~
make[4]: *** [cmsat5-src/CMakeFiles/libcryptominisat5.dir/build.make:596: cmsat5-src/CMakeFiles/libcryptominisat5.dir/cryptominisat.cpp.o] Error 1
make[4]: Leaving directory '/opt/sage/local/var/tmp/sage/build/cryptominisat-5.6.3/src'
make[3]: *** [CMakeFiles/Makefile2:198: cmsat5-src/CMakeFiles/libcryptominisat5.dir/all] Error 2
make[3]: Leaving directory '/opt/sage/local/var/tmp/sage/build/cryptominisat-5.6.3/src'
make[2]: *** [Makefile:130: all] Error 2
make[2]: Leaving directory '/opt/sage/local/var/tmp/sage/build/cryptominisat-5.6.3/src'

[msoos]

Ooops...Did you download the source tarball from the release page? Or did you clone? :) Try the tarball! I have Arch Linux and it works... (Sorry, don't have a computer here but you can see the Travis CI compiling in all configs. Just click the TravisCI icon on the GitHub page)

On Sun, 17 Jun 2018, 17:01 Vincent Delecroix, notifications@github.com wrote:

Compiling cryptominisat 5.6.3 ends with a compilation error

[ 84%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/cryptominisat.cpp.o cd /opt/sage/local/var/tmp/sage/build/cryptominisat-5.6.3/src/cmsat5-src && /usr/lib/ccache/bin/g++ -DBOOST_TEST_DYN_LINK -DUSE_GAUSS -DUSE_M4RI -DUSE_ZLIB -Dlibcryptominisat5_EXPORTS -I/opt /sage/local/include -I/opt/sage/local/var/tmp/sage/build/cryptominisat-5.6.3/src -I/opt/sage/local/var/tmp/sage/build/cryptominisat-5.6.3/src/cmsat5-src -mtune=native -Wall -Wextra -Wunused -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreacha ble-code -ggdb3 -Wlogical-op -Wrestrict -Wnull-dereference -Wdouble-promotion -Wshadow -Wformat=2 -Wextra-semi -pedantic -Wno-class-memaccess -fPIC -g -pthread -O2 -mtune=native -fPIC -std= gnu++11 -o CMakeFiles/libcryptominisat5.dir/cryptominisat.cpp.o -c /opt/sage/local/var/tmp/sage/build/cryptominisat-5.6.3/src/src/cryptominisat.cpp ../src/cryptominisat.cpp:1059:17: error: no declaration matches 'void CMSat::SATSolver::start_getting_small_clauses(uint32_t, uint32_t)' void DLL_PUBLIC SATSolver::start_getting_small_clauses(uint32_t max_len, uint32_t max_glue) ^~~~~ ../src/cryptominisat.cpp:1059:17: note: no functions named 'void CMSat::SATSolver::start_getting_small_clauses(uint32_t, uint32_t)' In file included from ../src/cryptominisat.cpp:24: ../../../../../../../include/cryptominisat5/cryptominisat.h:41:11: note: 'class CMSat::SATSolver' defined here class SATSolver ^~~~~ ../src/cryptominisat.cpp:1065:17: error: no declaration matches 'bool CMSat::SATSolver::get_next_small_clause(std::vector&)' bool DLL_PUBLIC SATSolver::get_next_small_clause(std::vector& out) ^~~~~ ../src/cryptominisat.cpp:1065:17: note: no functions named 'bool CMSat::SATSolver::get_next_small_clause(std::vector&)' In file included from ../src/cryptominisat.cpp:24: ../../../../../../../include/cryptominisat5/cryptominisat.h:41:11: note: 'class CMSat::SATSolver' defined here class SATSolver ^~~~~ ../src/cryptominisat.cpp:1071:17: error: no declaration matches 'void CMSat::SATSolver::end_getting_small_clauses()' void DLL_PUBLIC SATSolver::end_getting_small_clauses() ^~~~~ ../src/cryptominisat.cpp:1071:17: note: no functions named 'void CMSat::SATSolver::end_getting_small_clauses()' In file included from ../src/cryptominisat.cpp:24: ../../../../../../../include/cryptominisat5/cryptominisat.h:41:11: note: 'class CMSat::SATSolver' defined here class SATSolver ^~~~~ make[4]: [cmsat5-src/CMakeFiles/libcryptominisat5.dir/build.make:596: cmsat5-src/CMakeFiles/libcryptominisat5.dir/cryptominisat.cpp.o] Error 1 make[4]: Leaving directory '/opt/sage/local/var/tmp/sage/build/cryptominisat-5.6.3/src' make[3]: [CMakeFiles/Makefile2:198: cmsat5-src/CMakeFiles/libcryptominisat5.dir/all] Error 2 make[3]: Leaving directory '/opt/sage/local/var/tmp/sage/build/cryptominisat-5.6.3/src' make[2]: *** [Makefile:130: all] Error 2 make[2]: Leaving directory '/opt/sage/local/var/tmp/sage/build/cryptominisat-5.6.3/src'

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/msoos/cryptominisat/issues/496, or mute the thread https://github.com/notifications/unsubscribe-auth/ABReOc6W4Zz8MmON0x26gr1PKNIAN7hBks5t9ikPgaJpZM4Uqx1x .

[msoos]

See: https://travis-ci.org/msoos/cryptominisat you can check older compilations too.

On Sun, 17 Jun 2018, 17:53 Mate Soos, soos.mate@gmail.com wrote:

Ooops...Did you download the source tarball from the release page? Or did you clone? :) Try the tarball! I have Arch Linux and it works... (Sorry, don't have a computer here but you can see the Travis CI compiling in all configs. Just click the TravisCI icon on the GitHub page)

On Sun, 17 Jun 2018, 17:01 Vincent Delecroix, notifications@github.com wrote:

Compiling cryptominisat 5.6.3 ends with a compilation error

[ 84%] Building CXX object cmsat5-src/CMakeFiles/libcryptominisat5.dir/cryptominisat.cpp.o cd /opt/sage/local/var/tmp/sage/build/cryptominisat-5.6.3/src/cmsat5-src && /usr/lib/ccache/bin/g++ -DBOOST_TEST_DYN_LINK -DUSE_GAUSS -DUSE_M4RI -DUSE_ZLIB -Dlibcryptominisat5_EXPORTS -I/opt /sage/local/include -I/opt/sage/local/var/tmp/sage/build/cryptominisat-5.6.3/src -I/opt/sage/local/var/tmp/sage/build/cryptominisat-5.6.3/src/cmsat5-src -mtune=native -Wall -Wextra -Wunused -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreacha ble-code -ggdb3 -Wlogical-op -Wrestrict -Wnull-dereference -Wdouble-promotion -Wshadow -Wformat=2 -Wextra-semi -pedantic -Wno-class-memaccess -fPIC -g -pthread -O2 -mtune=native -fPIC -std= gnu++11 -o CMakeFiles/libcryptominisat5.dir/cryptominisat.cpp.o -c /opt/sage/local/var/tmp/sage/build/cryptominisat-5.6.3/src/src/cryptominisat.cpp ../src/cryptominisat.cpp:1059:17: error: no declaration matches 'void CMSat::SATSolver::start_getting_small_clauses(uint32_t, uint32_t)' void DLL_PUBLIC SATSolver::start_getting_small_clauses(uint32_t max_len, uint32_t max_glue) ^~~~~ ../src/cryptominisat.cpp:1059:17: note: no functions named 'void CMSat::SATSolver::start_getting_small_clauses(uint32_t, uint32_t)' In file included from ../src/cryptominisat.cpp:24: ../../../../../../../include/cryptominisat5/cryptominisat.h:41:11: note: 'class CMSat::SATSolver' defined here class SATSolver ^~~~~ ../src/cryptominisat.cpp:1065:17: error: no declaration matches 'bool CMSat::SATSolver::get_next_small_clause(std::vector&)' bool DLL_PUBLIC SATSolver::get_next_small_clause(std::vector& out) ^~~~~ ../src/cryptominisat.cpp:1065:17: note: no functions named 'bool CMSat::SATSolver::get_next_small_clause(std::vector&)' In file included from ../src/cryptominisat.cpp:24: ../../../../../../../include/cryptominisat5/cryptominisat.h:41:11: note: 'class CMSat::SATSolver' defined here class SATSolver ^~~~~ ../src/cryptominisat.cpp:1071:17: error: no declaration matches 'void CMSat::SATSolver::end_getting_small_clauses()' void DLL_PUBLIC SATSolver::end_getting_small_clauses() ^~~~~ ../src/cryptominisat.cpp:1071:17: note: no functions named 'void CMSat::SATSolver::end_getting_small_clauses()' In file included from ../src/cryptominisat.cpp:24: ../../../../../../../include/cryptominisat5/cryptominisat.h:41:11: note: 'class CMSat::SATSolver' defined here class SATSolver ^~~~~ make[4]: [cmsat5-src/CMakeFiles/libcryptominisat5.dir/build.make:596: cmsat5-src/CMakeFiles/libcryptominisat5.dir/cryptominisat.cpp.o] Error 1 make[4]: Leaving directory '/opt/sage/local/var/tmp/sage/build/cryptominisat-5.6.3/src' make[3]: [CMakeFiles/Makefile2:198: cmsat5-src/CMakeFiles/libcryptominisat5.dir/all] Error 2 make[3]: Leaving directory '/opt/sage/local/var/tmp/sage/build/cryptominisat-5.6.3/src' make[2]: *** [Makefile:130: all] Error 2 make[2]: Leaving directory '/opt/sage/local/var/tmp/sage/build/cryptominisat-5.6.3/src'

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/msoos/cryptominisat/issues/496, or mute the thread https://github.com/notifications/unsubscribe-auth/ABReOc6W4Zz8MmON0x26gr1PKNIAN7hBks5t9ikPgaJpZM4Uqx1x .

[videlec]

I downloaded the source tarball.

[msoos]

I'm traveling right now. Please use the precompiled binaries for the moment. I'll fix this once I'm back, in about a week :)

On Sun, 17 Jun 2018, 22:47 Vincent Delecroix, notifications@github.com wrote:

I downloaded the source tarball.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/msoos/cryptominisat/issues/496#issuecomment-397887588, or mute the thread https://github.com/notifications/unsubscribe-auth/ABReOdI3hN5ymH8-z9bC5WzZ2yyVKLdcks5t9noYgaJpZM4Uqx1x .

[msoos]

I'm back :) I'm sorry, I cannot reproduce this :( I have Arch Linux, just like you, I have gcc 8.1.0. All the automated builds all work with all the configs. I have downloaded the source, compiled, all worked. I am baffled. Can you please give me more details?

I need:

• Please delete the source, re-download it, unpack it, etc.
• Full cmake output
• Full build output
• Exact machine spec -- ARM? x86? AMD64?

Thanks a lot in advance!

[videlec]

Sorry for being not precise in my first message.

I am trying to build things inside SageMath which implies that many libraries and softwares do not come from my system but from SageMath (among other things, GMP, m4ri, cmake).

Actually, the following does succeed (with a lot of warnings though)

(sage-sh) $ cmake .
(sage-sh) $ make

The complete logs are cmake.log and make.log. But the following is not compiling

(sage-sh) $ cmake -DZLIB_ROOT="${SAGE_LOCAL}" .
(sage-sh) $ make

and the logs are cmake_with_zlib_root.log and make_with_zlib_root.log

[msoos]

well, so it's OK then, no? you definitely need that dzlib_root?

I think the problem is that sage math already comes with CryptoMiniSat. So that probably messes up things a lot. I'd rather if you just compiled it normally :) Is that an OK solution?

[msoos]

Hey, is this still and issue or may I close it? Thanks!

[videlec]

SageMath does not come with CryptoMiniSat. It is an experimental package, which means that it can be installed optionally. On my computer the CryptoMiniSat does not compile and this is the reason why I am trying to upgrade the package. But the more recent version also fails to build as I reported in this issue.

The DZLIB_ROOT is definitely needed since SageMath sources come with its own zlib (currently version 1.2.11).

[videlec]

for reference upstream ticket is https://trac.sagemath.org/ticket/25480

[msoos]

If I understand correctly, it's still the cryptominisat5/cryptominisat.h issue. You see this error:

/tmp/cryptominisat-5.6.3/src/cryptominisat.cpp:1059:17: error: no declaration matches 'void CMSat::SATSolver::start_getting_small_clauses(uint32_t, uint32_t)'
 void DLL_PUBLIC SATSolver::start_getting_small_clauses(uint32_t max_len, uint32_t max_glue)
                 ^~~~~~~~~

can only be because it's using a different cryptominisat5/cryptominisat.h that didn't have this new function declaration. And so it's complaining that this is being defined but it hasn't been declared. Note that the cryptominisat5/cryptominisat.h being generated during cmake does have this function declared. But old CMS versions did not. So an old version of CMS is most likely installed. Can you please delete it or remove it? Can you check for it in the included paths? (usually /usr/include and /usr/local/include but maybe now also the SageMath, even if it's not installed, the header might be there) -- according to my calculations, it must be reading an old cryptominisat5/cryptominisat.h. Thanks!

[videlec]

Indeed. Removing the old installation did the job (this was the install inside sage $SAGE_ROOT/local/include). I will need to start with that in the install script.

Thanks!

[msoos]

Glad it all worked out! Thanks for checking and getting back to me! Enjoy using the software and let me know if you have any issues :)

Mate

On Thu, 5 Jul 2018, 08:24 Vincent Delecroix, notifications@github.com wrote:

Closed #496 https://github.com/msoos/cryptominisat/issues/496.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/msoos/cryptominisat/issues/496#event-1717281114, or mute the thread https://github.com/notifications/unsubscribe-auth/ABReOQsuH07jnLE1cjiZ33BxtZYbDEYUks5uDbEFgaJpZM4Uqx1x .