search

sagemath / sage

Main repository of SageMath
https://www.sagemath.org
Other
1.48k stars 488 forks source link

Package cryptominisat 5 #22817

Closed edd8e884-f507-429a-b577-5d554626c0fe closed 7 years ago

edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago

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

edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago

Description changed:

--- 
+++ 
@@ -6,5 +6,5 @@

 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.
+**WARNING** Do not merge this ticket until the Sage interface has been updated, see #22818.
edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago

Changed dependencies from #22814 to #22814, #22818

edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago

Branch: u/tmonteil/package_cryptominisat_5

edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago

Commit: 67f23e7

edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago

New commits:

67f23e7#22817 : package cryptominisat 5.0.1
dimpase commented 7 years ago
comment:4

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

videlec commented 7 years ago
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 commented 7 years ago
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?

edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago
comment:7

Replying to @seblabbe:

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

Yes it should.

seblabbe commented 7 years ago

Changed keywords from days86 to days86, thursdaysbdx

seblabbe commented 7 years ago
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 commented 7 years ago

Attachment: cmake-3.8.0.log

dimpase commented 7 years ago
comment:10

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

edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago
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 commented 7 years ago
comment:12

On top of current #22999, I get

[cryptominisat-5.0.1] Successfully installed cryptominisat-5.0.1

on OSX 10.10.

edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago
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 commented 7 years ago
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 commented 7 years ago
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 commented 7 years ago
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:

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.
kiwifb commented 7 years ago

Changed commit from 67f23e7 to fd86b98

kiwifb commented 7 years ago

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

kiwifb commented 7 years ago
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 commented 7 years ago
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 commented 7 years ago
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 commented 7 years ago
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 commented 7 years ago
comment:21

Yup. All clear.

edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago
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 commented 7 years ago
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

?

edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago
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 commented 7 years ago
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 commented 7 years ago
comment:26

Let's make this dependent on #22999.

edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago
comment:27

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

edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago

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

seblabbe commented 7 years ago

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

seblabbe commented 7 years ago

Reviewer: Sébastien Labbé

edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago

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

edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago
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 commented 7 years ago

Changed branch from u/fbissey/package_cryptominisat_5 to fd86b98

edd8e884-f507-429a-b577-5d554626c0fe commented 5 years ago

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