Opened 2 years ago

Closed 2 years ago

#22817 closed enhancement (fixed)

Package cryptominisat 5

Reported by: tmonteil Owned by:
Priority: major Milestone: sage-8.0
Component: packages: experimental Keywords: days86, thursdaysbdx
Cc: Merged in:
Authors: Thierry Monteil, François Bissey Reviewers: Sébastien Labbé
Report Upstream: N/A Work issues:
Branch: fd86b98 (Commits) Commit: fd86b98ca8cfe57743036ec32425ba95fd1b9028
Dependencies: #22814, #22999 Stopgaps:

Description (last modified by tmonteil)

Our cryptominisat is currently locked at version 2.9.6, which does not build on 32bit architecture, while the current version of cryptominisat is 5.0.1. This ticket aims at updating the package.

Note that our current cython interface does not work with cryptominisat 5. However, cryptominisat now offers it own python bindings, so we have to rewrite the interface to use that instead.

Note that cryptominisat 5 relies on cmake, which needs to be updated to compile on 32bit architecture as well, see #22814.

Tarball available at : https://github.com/msoos/cryptominisat/archive/5.0.1.tar.gz to be renamed cryptominisat-5.0.1.tar.gz

WARNING Do not merge this ticket until the Sage interface has been updated, see #22818.

Attachments (1)

cmake-3.8.0.log (140.1 KB) - added by slabbe 2 years ago.

Download all attachments as: .zip

Change History (31)

comment:1 Changed 2 years ago by tmonteil

  • Dependencies changed from #22814 to #22814, #22818
  • Description modified (diff)

comment:2 Changed 2 years ago by tmonteil

  • Branch set to u/tmonteil/package_cryptominisat_5

comment:3 Changed 2 years ago by tmonteil

  • Commit set to 67f23e7d5aa105f83637587cc8527d607da0c367
  • Status changed from new to needs_review

New commits:

67f23e7#22817 : package cryptominisat 5.0.1

comment:4 Changed 2 years ago by dimpase

works on freebsd/clang, which is a good approx of OSX.

comment:5 follow-up: Changed 2 years ago by vdelecroix

cryptominisat has a testsuite (see Testing section on github). It would be good to have a spkg-check to be able to run (ie when doing sage -i -c cryptominisat).

comment:6 follow-up: Changed 2 years ago by slabbe

On the first run I get:

[cmake-3.8.0] sage_bootstrap.tarball.FileNotMirroredError: tarball does not exist on mirror network
[cmake-3.8.0] ************************************************************************
[cmake-3.8.0] Error downloading cmake-3.8.0.tar.gz
[cmake-3.8.0] ************************************************************************
[cmake-3.8.0] Please email sage-devel (http://groups.google.com/group/sage-devel)
[cmake-3.8.0] explaining the problem and including the log file
[cmake-3.8.0]   /Users/slabbe/Applications/sage-git/logs/pkgs/cmake-3.8.0.log
[cmake-3.8.0] Describe your computer, operating system, etc.
[cmake-3.8.0] ************************************************************************

Should not cmake tar ball be already on the mirror network?

comment:7 in reply to: ↑ 6 Changed 2 years ago by tmonteil

Replying to slabbe:

Should not cmake tar ball be already on the mirror network?

Yes it should.

comment:8 Changed 2 years ago by slabbe

  • Keywords thursdaysbdx added

comment:9 Changed 2 years ago by slabbe

I now get problem compiling cmake ...

$ MAKE='make -j2' sage -i cryptominisat

...

Scanning dependencies of target OSXScriptLauncher
[ 26%] Building CXX object Source/CMakeFiles/OSXScriptLauncher.dir/CPack/OSXScriptLauncher.cxx.o
[ 26%] Building C object Utilities/cmlibarchive/libarchive/CMakeFiles/cmlibarchive.dir/archive_read_support_format_warc.c.o
[ 26%] Building C object Utilities/cmlibarchive/libarchive/CMakeFiles/cmlibarchive.dir/archive_read_support_format_xar.c.o
In file included from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX10.9.sdk/usr/include/dispatch/dispatch.h:50:0,
                 from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX10.9.sdk/System/Library/Frameworks/CoreFoundation.framework/Headers/CFStream.h:15,
                 from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX10.9.sdk/System/Library/Frameworks/CoreFoundation.framework/Headers/CFPropertyList.h:13,
                 from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX10.9.sdk/System/Library/Frameworks/CoreFoundation.framework/Headers/CoreFoundation.h:55,
                 from CPack/OSXScriptLauncher.cxx:11:
../../../../../../../include/dispatch/object.h:321:1: error: 'DISPATCH_UNAVAILABLE' does not name a type
 DISPATCH_UNAVAILABLE
 ^
In file included from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX10.9.sdk/usr/include/dispatch/dispatch.h:50:0,
                 from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX10.9.sdk/System/Library/Frameworks/CoreFoundation.framework/Headers/CFStream.h:15,
                 from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX10.9.sdk/System/Library/Frameworks/CoreFoundation.framework/Headers/CFPropertyList.h:13,
                 from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX10.9.sdk/System/Library/Frameworks/CoreFoundation.framework/Headers/CoreFoundation.h:55,
                 from CPack/OSXScriptLauncher.cxx:11:
../../../../../../../include/dispatch/object.h:358:1: error: 'DISPATCH_UNAVAILABLE' does not name a type
 DISPATCH_UNAVAILABLE
 ^
In file included from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX10.9.sdk/usr/include/dispatch/dispatch.h:50:0,
                 from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX10.9.sdk/System/Library/Frameworks/CoreFoundation.framework/Headers/CFStream.h:15,
                 from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX10.9.sdk/System/Library/Frameworks/CoreFoundation.framework/Headers/CFPropertyList.h:13,
                 from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX10.9.sdk/System/Library/Frameworks/CoreFoundation.framework/Headers/CoreFoundation.h:55,
                 from CPack/OSXScriptLauncher.cxx:11:
../../../../../../../include/dispatch/object.h:387:1: error: 'DISPATCH_UNAVAILABLE' does not name a type
 DISPATCH_UNAVAILABLE
 ^
In file included from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX10.9.sdk/usr/include/dispatch/dispatch.h:50:0,
                 from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX10.9.sdk/System/Library/Frameworks/CoreFoundation.framework/Headers/CFStream.h:15,
                 from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX10.9.sdk/System/Library/Frameworks/CoreFoundation.framework/Headers/CFPropertyList.h:13,
                 from /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX10.9.sdk/System/Library/Frameworks/CoreFoundation.framework/Headers/CoreFoundation.h:55,
                 from CPack/OSXScriptLauncher.cxx:11:
../../../../../../../include/dispatch/object.h:418:1: error: 'DISPATCH_UNAVAILABLE' does not name a type
 DISPATCH_UNAVAILABLE
 ^
make[4]: *** [Source/CMakeFiles/OSXScriptLauncher.dir/CPack/OSXScriptLauncher.cxx.o] Error 1
make[3]: *** [Source/CMakeFiles/OSXScriptLauncher.dir/all] Error 2
make[3]: *** Waiting for unfinished jobs....

...

[cmake-3.8.0] [ 33%] Building C object Utilities/cmlibarchive/libarchive/CMakeFiles/cmlibarchive.dir/archive_write_set_format_zip.c.o
[cmake-3.8.0] [ 34%] Building C object Utilities/cmlibarchive/libarchive/CMakeFiles/cmlibarchive.dir/archive_write_set_options.c.o
[cmake-3.8.0] [ 34%] Building C object Utilities/cmlibarchive/libarchive/CMakeFiles/cmlibarchive.dir/archive_write_set_passphrase.c.o
[cmake-3.8.0] [ 34%] Building C object Utilities/cmlibarchive/libarchive/CMakeFiles/cmlibarchive.dir/filter_fork_posix.c.o
[cmake-3.8.0] [ 34%] Building C object Utilities/cmlibarchive/libarchive/CMakeFiles/cmlibarchive.dir/xxhash.c.o
[cmake-3.8.0] [ 34%] Linking C static library libcmlibarchive.a
[cmake-3.8.0] [ 34%] Built target cmlibarchive
[cmake-3.8.0] make[2]: *** [all] Error 2
[cmake-3.8.0] Error installing CMake.
[cmake-3.8.0] 
[cmake-3.8.0] real	7m50.136s
[cmake-3.8.0] user	6m17.332s
[cmake-3.8.0] sys	2m2.742s
[cmake-3.8.0] ************************************************************************
[cmake-3.8.0] Error installing package cmake-3.8.0
[cmake-3.8.0] ************************************************************************

I will upload the cmake-3.8.0.log file in a moment.

Last edited 2 years ago by slabbe (previous) (diff)

Changed 2 years ago by slabbe

comment:10 Changed 2 years ago by dimpase

Please try #22999 - this ticket upgrades cmake to 3.8.1, and we are going forward with it anyway.

comment:11 in reply to: ↑ 5 Changed 2 years ago by tmonteil

Replying to vdelecroix:

cryptominisat has a testsuite (see Testing section on github). It would be good to have a spkg-check to be able to run (ie when doing sage -i -c cryptominisat).

Indeed, i noticed that too. However, if i understand correctly, spkg-check is run after spkg-install, but in the current case, things should be done before the make (e.g. passing -DENABLE_TESTING=ON option to cmake). How to achieve this ?

Also, the testing requires the installation of 7 additionnal modules. Should i package each of them or rebuild a custom tarball from a git submodule command (with the effect to package the last commit in master, not the last official release) ?

comment:12 follow-up: Changed 2 years ago by slabbe

On top of current #22999, I get

[cryptominisat-5.0.1] Successfully installed cryptominisat-5.0.1

on OSX 10.10.

comment:13 in reply to: ↑ 12 ; follow-up: Changed 2 years ago by tmonteil

Replying to slabbe:

On top of current #22999, I get

[cryptominisat-5.0.1] Successfully installed cryptominisat-5.0.1

on OSX 10.10.

Great !

Regarding comment:5 i propose to postpone the self tests to another ticket.

comment:14 in reply to: ↑ 13 Changed 2 years ago by vdelecroix

Replying to tmonteil:

Replying to slabbe: Regarding comment:5 i propose to postpone the self tests to another ticket.

This is good for me. Did you open a ticket yet?

(note that the package installation went fine on ArchLinux with gcc 6.3.1)

Last edited 2 years ago by vdelecroix (previous) (diff)

comment:15 Changed 2 years ago by slabbe

  • Status changed from needs_review to needs_work

Something must be done regarding this package for OSX (see 22818#comment:33) because

sage: from pycryptosat import Solver
---------------------------------------------------------------------------
ImportError                               Traceback (most recent call last)
<ipython-input-3-280927e3230f> in <module>()
----> 1 from pycryptosat import Solver

ImportError: dlopen(/Users/slabbe/Applications/sage-git/local/lib/python2.7/site-packages/pycryptosat.so, 2): Library not loaded: libcryptominisat5.5.0.dylib
  Referenced from: /Users/slabbe/Applications/sage-git/local/lib/python2.7/site-packages/pycryptosat.so
  Reason: image not found

even if it has successfully installed...

Last edited 2 years ago by slabbe (previous) (diff)

comment:16 Changed 2 years ago by fbissey

  • Branch changed from u/tmonteil/package_cryptominisat_5 to u/fbissey/package_cryptominisat_5
  • Commit changed from 67f23e7d5aa105f83637587cc8527d607da0c367 to fd86b98ca8cfe57743036ec32425ba95fd1b9028

OK as mentioned on #22818 the package needs some love on OS X. I did a few QA on CMakeList.txt and tried not to get too carried away. As a bonus I changed spkg-install to find sage's zlib rather than the system one.

People should check for adverse effects on linux. But on OS X things should now work better.


New commits:

6e93c20Merge branch 'develop' into package_cryptominisat_5
a8db509patch to get install_name to be properly installed on OS X. Subtle QA for install by using GNUInstallDirs - may need more love.
fd86b98Make sure we find sage's zlib rather the system one.
Last edited 2 years ago by fbissey (previous) (diff)

comment:17 Changed 2 years ago by fbissey

Actually I'd be particularly interested to see if there are no side effects on debian (ubuntu should be a fine proxy for debian). debian has some particular install rules for libraries that I may have exposed.

comment:18 follow-up: Changed 2 years ago by slabbe

  • Status changed from needs_work to needs_review

On *Ubuntu 16.04*, on top of 8.0.beta7, I get

$ make cryptominisat
...
[cmake-3.8.0] Successfully installed cmake-3.8.0
...
[cryptominisat-5.0.1] Successfully installed cryptominisat-5.0.1

Then,

sage: from pycryptosat import Solver
sage: s = Solver()
sage: s.add_clause((1r,1r,1r,1r,-1r))
sage: s.solve()
(True, (None, False))

I will check whether it works on my OSX later (my osx being at home).

comment:19 Changed 2 years ago by fbissey

I had no doubt the installation would be successful. I am just wondering if the library will end in a strange place compared to normal (local/lib/x86_64/ for example).

comment:20 Changed 2 years ago by slabbe

Does this answer your question?

slabbe@miami local $ find | grep cryptominisat
./include/cryptominisat5
./include/cryptominisat5/cryptominisat_c.h
./include/cryptominisat5/cryptominisat.h
./include/cryptominisat5/solvertypesmini.h
./var/lib/sage/installed/cryptominisat-5.0.1
./lib/libcryptominisat5.so.5.0
./lib/cmake/cryptominisat5
./lib/cmake/cryptominisat5/cryptominisat5Config.cmake
./lib/cmake/cryptominisat5/cryptominisat5Targets-relwithdebinfo.cmake
./lib/cmake/cryptominisat5/cryptominisat5Targets.cmake
./lib/python2.7/site-packages/sage/sat/solvers/cryptominisat
./lib/python2.7/site-packages/sage/sat/solvers/cryptominisat/cryptominisat.pxd
./lib/python2.7/site-packages/sage/sat/solvers/cryptominisat/solverconf.pxd
./lib/python2.7/site-packages/sage/sat/solvers/cryptominisat/__init__.pyc
./lib/python2.7/site-packages/sage/sat/solvers/cryptominisat/decl.pxd
./lib/python2.7/site-packages/sage/sat/solvers/cryptominisat/solverconf_helper.h
./lib/python2.7/site-packages/sage/sat/solvers/cryptominisat/__init__.py
./lib/python2.7/site-packages/sage/sat/solvers/cryptominisat/cryptominisat_helper.h
./lib/libcryptominisat5.so
./bin/cryptominisat5_simple

slabbe@miami local $ find | grep cryptosat
./lib/python2.7/site-packages/pycryptosat.so
./lib/python2.7/site-packages/pycryptosat-5.0.1-py2.7.egg-info

comment:21 Changed 2 years ago by fbissey

Yup. All clear.

comment:22 Changed 2 years ago by tmonteil

Is seems good on my 64bit laptop too (i can not test on my 32bit VM since it is currently used to detect and fix broken self-tests for standard packages, see #23058, #23057, #23056, #23055, #23045).

comment:23 in reply to: ↑ 18 Changed 2 years ago by slabbe

Replying to slabbe:

On *Ubuntu 16.04*, on top of 8.0.beta7, I get

$ make cryptominisat
...
[cmake-3.8.0] Successfully installed cmake-3.8.0
...
[cryptominisat-5.0.1] Successfully installed cryptominisat-5.0.1

In fact, I think I have a problem on Ubuntu, on another run of make, I get Solver.h: Aucun fichier ou dossier de ce type:

[sagelib-8.0.beta7] [2/3] creating build/temp.linux-x86_64-2.7/home/slabbe/GitBox/sage/src/build/cythonized/sage/sat/solvers/cryptominisat
[sagelib-8.0.beta7] gcc -fno-strict-aliasing -g -O2 -DNDEBUG -g -fwrapv -O3 -Wall -Wno-unused -fPIC -Isage/sat/solvers/cryptominisat -I/home/slabbe/GitBox/sage/local/lib/python2.7/site-packages/cysignals -I/home/slabbe/GitBox/sage/local/include/cmsat -I/home/slabbe/GitBox/sage/local/include -I/home/slabbe/GitBox/sage/local/include/python2.7 -I/home/slabbe/GitBox/sage/local/lib/python2.7/site-packages/numpy/core/include -I/home/slabbe/GitBox/sage/src -I/home/slabbe/GitBox/sage/src/sage/ext -I/home/slabbe/GitBox/sage/src/build/cythonized -I/home/slabbe/GitBox/sage/src/build/cythonized/sage/ext -I/home/slabbe/GitBox/sage/local/include/python2.7 -c /home/slabbe/GitBox/sage/src/build/cythonized/sage/sat/solvers/cryptominisat/cryptominisat.cpp -o build/temp.linux-x86_64-2.7/home/slabbe/GitBox/sage/src/build/cythonized/sage/sat/solvers/cryptominisat/cryptominisat.o -fno-strict-aliasing
[sagelib-8.0.beta7] /home/slabbe/GitBox/sage/src/build/cythonized/sage/sat/solvers/cryptominisat/cryptominisat.cpp:499:20: fatal error: Solver.h: Aucun fichier ou dossier de ce type
[sagelib-8.0.beta7] compilation terminated.
[sagelib-8.0.beta7] [3/3] gcc -fno-strict-aliasing -g -O2 -DNDEBUG -g -fwrapv -O3 -Wall -Wno-unused -fPIC -I/home/slabbe/GitBox/sage/local/include/cmsat -I/home/slabbe/GitBox/sage/local/include -I/home/slabbe/GitBox/sage/local/include/python2.7 -I/home/slabbe/GitBox/sage/local/lib/python2.7/site-packages/numpy/core/include -I/home/slabbe/GitBox/sage/src -I/home/slabbe/GitBox/sage/src/sage/ext -I/home/slabbe/GitBox/sage/src/build/cythonized -I/home/slabbe/GitBox/sage/src/build/cythonized/sage/ext -I/home/slabbe/GitBox/sage/local/include/python2.7 -c /home/slabbe/GitBox/sage/src/build/cythonized/sage/sat/solvers/cryptominisat/solverconf.cpp -o build/temp.linux-x86_64-2.7/home/slabbe/GitBox/sage/src/build/cythonized/sage/sat/solvers/cryptominisat/solverconf.o -fno-strict-aliasing
[sagelib-8.0.beta7] error: command 'gcc' failed with exit status 1
[sagelib-8.0.beta7] /home/slabbe/GitBox/sage/src/build/cythonized/sage/sat/solvers/cryptominisat/solverconf.cpp:493:20: fatal error: Solver.h: Aucun fichier ou dossier de ce type
[sagelib-8.0.beta7] compilation terminated.
[sagelib-8.0.beta7] Makefile:34 : la recette pour la cible « sage » a échouée

Maybe the right command to install is (like for cbc) :

make cryptominisat sagelib

?

comment:24 follow-up: Changed 2 years ago by tmonteil

Yes, this is because the old cython interface only compiles with cryptominisat 2. This ticket is enough to compile cryptominisat 5, but you have to apply #22818 if you want to compile Sage.

comment:25 in reply to: ↑ 24 Changed 2 years ago by slabbe

Replying to tmonteil:

Yes, this is because the old cython interface only compiles with cryptominisat 2. This ticket is enough to compile cryptominisat 5, but you have to apply #22818 if you want to compile Sage.

Thank you for your answer, it helped me today to make my sage to work again when I needed it.

comment:26 Changed 2 years ago by dimpase

Let's make this dependent on #22999.

comment:27 Changed 2 years ago by tmonteil

  • Dependencies changed from #22814, #22818 to #22814, #22818, #22999

See also this discussion.

comment:28 Changed 2 years ago by slabbe

  • Authors changed from Thierry Monteil to Thierry Monteil, François Bissey
  • Reviewers set to Sébastien Labbé
  • Status changed from needs_review to positive_review

comment:29 Changed 2 years ago by tmonteil

  • Dependencies changed from #22814, #22818, #22999 to #22814, #22999

Let me just remove the cyclic dependency, which might let think that none of both ticket is ready. The description is clear enough.

comment:30 Changed 2 years ago by vbraun

  • Branch changed from u/fbissey/package_cryptominisat_5 to fd86b98ca8cfe57743036ec32425ba95fd1b9028
  • Resolution set to fixed
  • Status changed from positive_review to closed
Note: See TracTickets for help on using tickets.