Opened 3 years ago

Closed 3 years ago

#25480 closed enhancement (fixed)

Upgrade to cryptominisat 5.6.6 (and make it an optional package again)

Reported by: vdelecroix Owned by:
Priority: major Milestone: sage-8.7
Component: packages: optional Keywords: cryptominisat, upgrade
Cc: tmonteil, embray, saraedum, slelievre Merged in:
Authors: Vincent Delecroix, Thierry Monteil Reviewers: Jeroen Demeyer, Vincent Delecroix
Report Upstream: N/A Work issues:
Branch: d483861 (Commits, GitHub, GitLab) Commit: d48386132cb3e2646647f14b8465f0eb4aa58543
Dependencies: Stopgaps:

Status badges

Description (last modified by tmonteil)

Update cryptominisat to 5.6.6.

Tarball at

https://github.com/msoos/cryptominisat/archive/5.6.6.tar.gz

(to be renamed cryptominisat-5.6.6.tar.gz)

Compilation issues which had caused cryptominisat to be downgraded from "optional" to "experimental" in Sage are fixed in the 5.6.x releases. Note that old installations have to be removed because of interference of header files (see e.g. issue 5).

Attachments (1)

cryptominisat-5.6.5.log (10.1 KB) - added by tmonteil 3 years ago.

Download all attachments as: .zip

Change History (41)

comment:1 Changed 3 years ago by vdelecroix

  • Branch set to u/vdelecroix/25480
  • Commit set to cbf02c938a7a89f3c753aebdcd9a57996037ba84

Experimental branch (for the prerelease). I will update the branch as soon as the definitive release is out. Please test in the meantime (works for me with Python2 but did not check with Python3).


New commits:

cbf02c925480: upgrade cryptominisat

comment:2 Changed 3 years ago by slelievre

  • Cc embray slelievre added; ebray removed
  • Keywords cryptominisat upgrade added

comment:3 Changed 3 years ago by slelievre

  • Description modified (diff)
  • Summary changed from upgrade cryptominisat (and put back as optional) to Upgrade to cryptominisat 5.6.1 (and make it an optional package again)

comment:4 Changed 3 years ago by slelievre

  • Description modified (diff)

Cryptominisat 5.6.3 was released, do you mind using that instead of 5.6.1?

comment:5 Changed 3 years ago by slelievre

  • Cc saraedum added
  • Summary changed from Upgrade to cryptominisat 5.6.1 (and make it an optional package again) to Upgrade to cryptominisat 5.6.3 (and make it an optional package again)

comment:6 Changed 3 years ago by vdelecroix

  • Description modified (diff)

comment:7 Changed 3 years ago by vdelecroix

Still not able to build crypotiminisat (archlinux and gcc 8.1.1)

[ 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'
********************************************************************************
Error building cryptominisat-5.6.3
********************************************************************************

comment:8 Changed 3 years ago by git

  • Commit changed from cbf02c938a7a89f3c753aebdcd9a57996037ba84 to 88474da0f4ae6f70be0c1e4f1e7778ea808fd1aa

Branch pushed to git repo; I updated commit sha1. This was a forced push. New commits:

88474da25480: upgrade cryptominisat

comment:9 Changed 3 years ago by git

  • Commit changed from 88474da0f4ae6f70be0c1e4f1e7778ea808fd1aa to deb30ee018a66fac019a66103fdd1561d8ff4bd6

Branch pushed to git repo; I updated commit sha1. This was a forced push. New commits:

deb30ee25480: upgrade cryptominisat

comment:10 Changed 3 years ago by git

  • Commit changed from deb30ee018a66fac019a66103fdd1561d8ff4bd6 to 935d788fa29a8a4b3b882570e528efda8e3417eb

Branch pushed to git repo; I updated commit sha1. New commits:

935d78825480: make cryptominisat optional again

comment:11 Changed 3 years ago by vdelecroix

  • Status changed from new to needs_review

comment:12 Changed 3 years ago by vdelecroix

  • Description modified (diff)

comment:13 Changed 3 years ago by jdemeyer

  • Status changed from needs_review to needs_work

cryptominisat links to libm4ri, so that should be a normal dependency:

        linux-vdso64.so.1 =>  (0x00003fff925a0000)
        libm4ri-0.0.20140914.so => /home/jdemeyer/sage-test/local/lib/libm4ri-0.0.20140914.so (0x00003fff923f0000)
        libstdc++.so.6 => /usr/lib/powerpc64le-linux-gnu/libstdc++.so.6 (0x00003fff921d0000)
        libm.so.6 => /lib/powerpc64le-linux-gnu/libm.so.6 (0x00003fff920e0000)
        libgcc_s.so.1 => /lib/powerpc64le-linux-gnu/libgcc_s.so.1 (0x00003fff920b0000)
        libpthread.so.0 => /lib/powerpc64le-linux-gnu/libpthread.so.0 (0x00003fff92070000)
        libc.so.6 => /lib/powerpc64le-linux-gnu/libc.so.6 (0x00003fff91ea0000)
        libpng16.so.16 => /home/jdemeyer/sage-test/local/lib/libpng16.so.16 (0x00003fff91e20000)
        /lib64/ld64.so.2 (0x00003fff925c0000)
        libz.so.1 => /home/jdemeyer/sage-test/local/lib/libz.so.1 (0x00003fff91de0000)

comment:14 Changed 3 years ago by jdemeyer

Same for libz and libpng.

comment:15 Changed 3 years ago by jdemeyer

  • Reviewers set to Jeroen Demeyer

comment:16 Changed 3 years ago by jdemeyer

This seems to build only Python 3 bindings. From the logfile:

-- Found PythonInterp: /home/jdemeyer/sage-git/local/bin/python3 (found suitable version "3.6.1", minimum required is "3")
-- Found PythonLibs: /home/jdemeyer/sage-git/local/lib/libpython3.6m.so (found suitable version "3.6.1", minimum required is "3")
-- Python 3 -- PYTHON_EXECUTABLE=/home/jdemeyer/sage-git/local/bin/python3
-- Python 3 -- PYTHON_LIBRARIES=/home/jdemeyer/sage-git/local/lib/libpython3.6m.so
-- Python 3 -- PYTHON_INCLUDE_DIRS=/home/jdemeyer/sage-git/local/include/python3.6m
-- Python 3 -- PYTHONLIBS_VERSION_STRING=3.6.1

comment:17 Changed 3 years ago by git

  • Commit changed from 935d788fa29a8a4b3b882570e528efda8e3417eb to 1a1d00723c4919e91dd229c422424831cceba13e

Branch pushed to git repo; I updated commit sha1. New commits:

1a1d00725480: force Python2 + dependencies

comment:18 Changed 3 years ago by vdelecroix

  • Status changed from needs_work to needs_review

It is apparently not possible to compile for both Python2 and Python3 (see issue 498). For now Python2 is forced.

comment:19 Changed 3 years ago by vdelecroix

  • Status changed from needs_review to needs_work

This is annoying

-- Found m4ri: /usr/lib/libm4ri.so  
-- OK, Found M4RI lib at /usr/lib/libm4ri.so and includes at /usr/include

should be using the one from Sage...

comment:20 Changed 3 years ago by vdelecroix

Though linking looks fine

$ ldd /opt/sage/local/lib/libcryptominisat5.so
...
        libm4ri-0.0.20140914.so => /opt/sage/local/lib/libm4ri-0.0.20140914.so (0x00007f10dc270000)
...

comment:21 Changed 3 years ago by git

  • Commit changed from 1a1d00723c4919e91dd229c422424831cceba13e to 85d14cc75300bdff7bd2fc2b51195e350ffd648d

Branch pushed to git repo; I updated commit sha1. This was a forced push. New commits:

1cee4c725480: upgrade cryptominisat
d6aa12025480: make cryptominisat optional again
85d14cc25480: force Python2 + dependencies

comment:22 Changed 3 years ago by vdelecroix

  • Status changed from needs_work to needs_review

rebased on rc0. Installation should work with both python2 and python3.

I was not able to properly fix the configuration to detect m4ri nicely.

comment:23 Changed 3 years ago by jdemeyer

  • Status changed from needs_review to needs_work

13

comment:24 Changed 3 years ago by vdelecroix

  • Status changed from needs_work to needs_info

Not happy with?

  • build/pkgs/cryptominisat/dependencies

    diff --git a/build/pkgs/cryptominisat/dependencies b/build/pkgs/cryptominisat/dependencies
    index df51e31274..a199426946 100644
    a b  
    1 $(PYTHON) | cmake sqlite m4ri boost_cropped
     1$(PYTHON) | cmake sqlite m4ri boost_cropped zlib libpng

comment:25 Changed 3 years ago by jdemeyer

I meant normal dependencies meaning before the | symbol.

comment:26 Changed 3 years ago by git

  • Commit changed from 85d14cc75300bdff7bd2fc2b51195e350ffd648d to 2d9675c3c7e741ed27639c87bf98a73a4618e726

Branch pushed to git repo; I updated commit sha1. New commits:

2d9675c25480: fix dependencies

comment:27 Changed 3 years ago by vdelecroix

  • Status changed from needs_info to needs_review

comment:28 Changed 3 years ago by embray

  • Status changed from needs_review to needs_work

*sigh* It seems shortly after my fix to DESTDIR support they broke it again with https://github.com/msoos/cryptominisat/commit/63a629f5e363a467abff1fa29becf42fe55b79f9 and https://github.com/msoos/cryptominisat/commit/b3cd73f369d4ea14f12824f0f3c4a06a9aa0e1b1 by not understanding the difference between "root", "prefix", and "DESTDIR". I will raise this issue once again upstream, but in the meantime, unless we want to wait for another upstream release, this will have to be patched again...

comment:29 Changed 3 years ago by embray

Upstream PR if you want to make a patch from it: https://github.com/msoos/cryptominisat/pull/499

comment:30 Changed 3 years ago by embray

Other than that issue, LGTM.

comment:31 Changed 3 years ago by slelievre

  • Description modified (diff)
  • Milestone changed from sage-8.3 to sage-8.4
  • Summary changed from Upgrade to cryptominisat 5.6.3 (and make it an optional package again) to Upgrade to cryptominisat 5.6.4 (and make it an optional package again)

Cryptominisat 5.6.4 was released. Would be nice to get this in Sage 8.4.

comment:32 Changed 3 years ago by tmonteil

  • Description modified (diff)
  • Summary changed from Upgrade to cryptominisat 5.6.4 (and make it an optional package again) to Upgrade to cryptominisat 5.6.5 (and make it an optional package again)

CryptoMiniSat? 5.6.5 is out and contains Erik's fix, let's see how it works.

Last edited 3 years ago by tmonteil (previous) (diff)

comment:33 Changed 3 years ago by tmonteil

  • Branch changed from u/vdelecroix/25480 to u/tmonteil/25480

Changed 3 years ago by tmonteil

comment:34 Changed 3 years ago by tmonteil

  • Commit changed from 2d9675c3c7e741ed27639c87bf98a73a4618e726 to eab8ad8144de2a5aaa4dd020b3cb6cf979a8d7a2

Not happy (see log).


New commits:

f5dc814Merge branch 'u/vdelecroix/25480' of trac.sagemath.org:sage into HEAD
eab8ad8#25480 : update cryptominisat to 5.6.5

comment:35 Changed 3 years ago by git

  • Commit changed from eab8ad8144de2a5aaa4dd020b3cb6cf979a8d7a2 to 8bae4cdb3c45c957c88d81b43d8c2e5cb843af68

Branch pushed to git repo; I updated commit sha1. New commits:

ef1397aMerge branch 'u/tmonteil/25480' of trac.sagemath.org:sage into HEAD
8bae4cd#25480 : update cryptominisat to 5.6.6

comment:36 Changed 3 years ago by tmonteil

  • Authors changed from Vincent Delecroix to Vincent Delecroix, Thierry Monteil
  • Description modified (diff)
  • Status changed from needs_work to needs_review
  • Summary changed from Upgrade to cryptominisat 5.6.5 (and make it an optional package again) to Upgrade to cryptominisat 5.6.6 (and make it an optional package again)

Seems to work well with 5.6.6 ! The only problem i found is when the help2man command from the autotools experimental package is available.

Last edited 3 years ago by tmonteil (previous) (diff)

comment:37 Changed 3 years ago by git

  • Commit changed from 8bae4cdb3c45c957c88d81b43d8c2e5cb843af68 to d48386132cb3e2646647f14b8465f0eb4aa58543

Branch pushed to git repo; I updated commit sha1. New commits:

48338deMerge branch 'u/tmonteil/25480' of trac.sagemath.org:sage into HEAD
d483861#25480 : update a doctest after #26676 has been merged.

comment:38 Changed 3 years ago by tmonteil

  • Milestone changed from sage-8.4 to sage-8.6

I updated a doctest coming from #26676 (which has been merged). Still needs review.

comment:39 Changed 3 years ago by vdelecroix

  • Milestone changed from sage-8.6 to sage-8.7
  • Reviewers changed from Jeroen Demeyer to Jeroen Demeyer, Vincent Delecroix
  • Status changed from needs_review to positive_review

builds fine and tests pass for me.

comment:40 Changed 3 years ago by vbraun

  • Branch changed from u/tmonteil/25480 to d48386132cb3e2646647f14b8465f0eb4aa58543
  • Resolution set to fixed
  • Status changed from positive_review to closed
Note: See TracTickets for help on using tickets.