Package cryptominisat 5 #22817

sagetrac-tmonteil · 2017-04-15T23:26:49Z

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.

Depends on #22814
Depends on #22999

Component: packages: experimental

Keywords: days86, thursdaysbdx, sdl

Author: Thierry Monteil, François Bissey

Branch/Commit: fd86b98

Reviewer: Sébastien Labbé

Issue created by migration from https://trac.sagemath.org/ticket/22817

The text was updated successfully, but these errors were encountered:

sagetrac-tmonteil · 2017-04-15T23:31:17Z

Changed dependencies from #22814 to #22814, #22818

sagetrac-tmonteil · 2017-05-03T10:21:01Z

Branch: u/tmonteil/package_cryptominisat_5

sagetrac-tmonteil · 2017-05-14T16:26:49Z

Commit: 67f23e7

sagetrac-tmonteil · 2017-05-14T16:26:49Z

New commits:

`67f23e7`	`#22817 : package cryptominisat 5.0.1`

dimpase · 2017-05-15T10:35:07Z

comment:4

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

videlec · 2017-05-18T07:29:16Z

comment:5

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).

seblabbe · 2017-05-18T11:49:52Z

comment:6

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?

sagetrac-tmonteil · 2017-05-18T11:57:21Z

comment:7

Replying to @seblabbe:

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

Yes it should.

seblabbe · 2017-05-18T11:59:54Z

Changed keywords from days86 to days86, thursdaysbdx

seblabbe · 2017-05-18T12:10:10Z

comment:9

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.

seblabbe · 2017-05-18T12:11:15Z

Attachment: cmake-3.8.0.log

dimpase · 2017-05-18T12:14:49Z

comment:10

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

sagetrac-tmonteil · 2017-05-18T12:53:17Z

comment:11

Replying to @videlec:

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) ?

seblabbe · 2017-05-18T22:07:02Z

comment:12

On top of current #22999, I get

[cryptominisat-5.0.1] Successfully installed cryptominisat-5.0.1

on OSX 10.10.

sagetrac-tmonteil · 2017-05-19T06:30:45Z

comment:13

Replying to @seblabbe:

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.

videlec · 2017-05-19T17:49:07Z

comment:14

Replying to @sagetrac-tmonteil:

Replying to @seblabbe:
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)

seblabbe · 2017-05-19T19:58:28Z

comment:15

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...

kiwifb · 2017-05-22T23:37:12Z

comment:16

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:

`6e93c20`	`Merge branch 'develop' into package_cryptominisat_5`
`a8db509`	`patch to get install_name to be properly installed on OS X. Subtle QA for install by using GNUInstallDirs - may need more love.`
`fd86b98`	`Make sure we find sage's zlib rather the system one.`

kiwifb · 2017-05-22T23:37:12Z

Changed commit from 67f23e7 to fd86b98

kiwifb · 2017-05-22T23:37:12Z

Changed branch from u/tmonteil/package_cryptominisat_5 to u/fbissey/package_cryptominisat_5

kiwifb · 2017-05-22T23:44:55Z

comment:17

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.

seblabbe · 2017-05-24T08:49:54Z

comment:18

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).

kiwifb · 2017-05-24T08:52:25Z

comment:19

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).

seblabbe · 2017-05-24T09:10:47Z

comment:20

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

kiwifb · 2017-05-24T09:14:33Z

comment:21

Yup. All clear.

sagetrac-tmonteil · 2017-05-24T12:35:41Z

comment:22

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).

seblabbe · 2017-05-24T12:42:29Z

comment:23

Replying to @seblabbe:

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

?

sagetrac-tmonteil · 2017-05-24T12:52:21Z

comment:24

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.

seblabbe · 2017-05-24T21:12:18Z

comment:25

Replying to @sagetrac-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.

dimpase · 2017-05-25T09:10:44Z

comment:26

Let's make this dependent on #22999.

sagetrac-tmonteil · 2017-05-25T09:24:29Z

comment:27

See also [/22818#comment:50 this discussion].

sagetrac-tmonteil · 2017-05-25T09:24:29Z

Changed dependencies from #22814, #22818 to #22814, #22818, #22999

seblabbe · 2017-06-10T21:04:06Z

Changed author from Thierry Monteil to Thierry Monteil, François Bissey

seblabbe · 2017-06-10T21:04:06Z

Reviewer: Sébastien Labbé

sagetrac-tmonteil · 2017-06-11T21:04:39Z

Changed dependencies from #22814, #22818, #22999 to #22814, #22999

sagetrac-tmonteil · 2017-06-11T21:04:39Z

comment:29

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

vbraun · 2017-06-13T06:51:44Z

Changed branch from u/fbissey/package_cryptominisat_5 to fd86b98

sagetrac-tmonteil · 2019-08-27T19:45:19Z

Changed keywords from days86, thursdaysbdx to days86, thursdaysbdx, sdl

sagetrac-tmonteil mannequin added this to the sage-8.0 milestone Apr 15, 2017

sagetrac-tmonteil mannequin added c: packages: experimental labels Apr 15, 2017

This comment has been minimized.

Sign in to view

sagetrac-tmonteil mannequin added the s: needs review label May 14, 2017

seblabbe added s: needs work and removed s: needs review labels May 19, 2017

seblabbe added s: needs review and removed s: needs work labels May 24, 2017

seblabbe added s: positive review and removed s: needs review labels Jun 10, 2017

vbraun removed the s: positive review label Jun 13, 2017

vbraun closed this as completed in 70a605e Jun 13, 2017

This was referenced Aug 27, 2019

Interface cryptominisat 5 #22818

Closed

Make cryptominisat an optional package #23219

Closed

Package cryptominisat 5 #22817

Package cryptominisat 5 #22817

Comments

sagetrac-tmonteil mannequin commented Apr 15, 2017

This comment has been minimized.

sagetrac-tmonteil mannequin commented Apr 15, 2017

sagetrac-tmonteil mannequin commented May 3, 2017

sagetrac-tmonteil mannequin commented May 14, 2017

sagetrac-tmonteil mannequin commented May 14, 2017

dimpase commented May 15, 2017

videlec commented May 18, 2017

seblabbe commented May 18, 2017

sagetrac-tmonteil mannequin commented May 18, 2017

seblabbe commented May 18, 2017

seblabbe commented May 18, 2017

seblabbe commented May 18, 2017

dimpase commented May 18, 2017

sagetrac-tmonteil mannequin commented May 18, 2017

seblabbe commented May 18, 2017

sagetrac-tmonteil mannequin commented May 19, 2017

videlec commented May 19, 2017

seblabbe commented May 19, 2017

kiwifb commented May 22, 2017

kiwifb commented May 22, 2017

kiwifb commented May 22, 2017

kiwifb commented May 22, 2017

seblabbe commented May 24, 2017

kiwifb commented May 24, 2017

seblabbe commented May 24, 2017

kiwifb commented May 24, 2017

sagetrac-tmonteil mannequin commented May 24, 2017

seblabbe commented May 24, 2017

sagetrac-tmonteil mannequin commented May 24, 2017

seblabbe commented May 24, 2017

dimpase commented May 25, 2017

sagetrac-tmonteil mannequin commented May 25, 2017

sagetrac-tmonteil mannequin commented May 25, 2017

seblabbe commented Jun 10, 2017

seblabbe commented Jun 10, 2017

sagetrac-tmonteil mannequin commented Jun 11, 2017

sagetrac-tmonteil mannequin commented Jun 11, 2017

vbraun commented Jun 13, 2017

sagetrac-tmonteil mannequin commented Aug 27, 2019