videlec
commented
6 years ago Commit: cbf02c9
Closed videlec closed 5 years ago
videlec
commented
6 years ago 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:
cbf02c9 | 25480: upgrade cryptominisat |
videlec
commented
6 years ago Branch: u/vdelecroix/25480
slel
commented
6 years ago Changed keywords from none to cryptominisat, upgrade
slel
commented
6 years ago Description changed:
---
+++
@@ -1,3 +1,7 @@
-Upstream cryptominisat fixed compilation issues. There is a prerelease available at
+Cryptominisat 5.6.1 is now available:
- https://github.com/msoos/cryptominisat/releases/tag/5.6.0
+- https://github.com/msoos/cryptominisat/releases/
+
+It fixes compilation issues which had made us downgrade it
+from "optional" to "experimental" in Sage.
+Description changed:
---
+++
@@ -1,7 +1,9 @@
-Cryptominisat 5.6.1 is now available:
+Cryptominisat 5.6.3 is now available:
-- https://github.com/msoos/cryptominisat/releases/
+- releases: https://github.com/msoos/cryptominisat/releases/
+- tarball: https://github.com/msoos/cryptominisat/archive/5.6.3.tar.gz
-It fixes compilation issues which had made us downgrade it
-from "optional" to "experimental" in Sage.
+Compilation issues which had caused cryptominisat to be
+downgraded from "optional" to "experimental" in Sage
+are fixed in the 5.6.x releases.
Cryptominisat 5.6.3 was released, do you mind using that instead of 5.6.1?
videlec
commented
6 years ago Description changed:
---
+++
@@ -1,9 +1,9 @@
-Cryptominisat 5.6.3 is now available:
+Update cryptominisat to 5.6.3.
-- releases: https://github.com/msoos/cryptominisat/releases/
-- tarball: https://github.com/msoos/cryptominisat/archive/5.6.3.tar.gz
+Tarball at
-Compilation issues which had caused cryptominisat to be
-downgraded from "optional" to "experimental" in Sage
-are fixed in the 5.6.x releases.
+ https://github.com/msoos/cryptominisat/archive/5.6.3.tar.gz
+(to be renamed cryptominisat-5.6.3.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.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
********************************************************************************
7ed8c4ca-6d56-4ae9-953a-41e42b4ed313
commented
6 years ago 7ed8c4ca-6d56-4ae9-953a-41e42b4ed313
commented
6 years ago Branch pushed to git repo; I updated commit sha1. This was a forced push. New commits:
88474da | 25480: upgrade cryptominisat |
7ed8c4ca-6d56-4ae9-953a-41e42b4ed313
commented
6 years ago Branch pushed to git repo; I updated commit sha1. This was a forced push. New commits:
deb30ee | 25480: upgrade cryptominisat |
7ed8c4ca-6d56-4ae9-953a-41e42b4ed313
commented
6 years ago 7ed8c4ca-6d56-4ae9-953a-41e42b4ed313
commented
6 years ago 7ed8c4ca-6d56-4ae9-953a-41e42b4ed313
commented
6 years ago Branch pushed to git repo; I updated commit sha1. New commits:
935d788 | 25480: make cryptominisat optional again |
videlec
commented
6 years ago Description changed:
---
+++
@@ -6,4 +6,4 @@
(to be renamed cryptominisat-5.6.3.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.
+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 installation have to be removed because of interference of header files (see e.g. [issue 5](https://github.com/msoos/cryptominisat/issues/496)).
jdemeyer
commented
6 years ago 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)Same for libz and libpng.
jdemeyer
commented
6 years ago Reviewer: Jeroen Demeyer
jdemeyer
commented
6 years ago 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.1Branch pushed to git repo; I updated commit sha1. New commits:
1a1d007 | 25480: force Python2 + dependencies |
7ed8c4ca-6d56-4ae9-953a-41e42b4ed313
commented
6 years ago videlec
commented
6 years ago It is apparently not possible to compile for both Python2 and Python3 (see issue 498). For now Python2 is forced.
videlec
commented
6 years ago This is annoying
-- Found m4ri: /usr/lib/libm4ri.so
-- OK, Found M4RI lib at /usr/lib/libm4ri.so and includes at /usr/includeshould be using the one from Sage...
videlec
commented
6 years ago 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)
...rebased on rc0. Installation should work with both python2 and python3.
I was not able to properly fix the configuration to detect m4ri nicely.
jdemeyer
commented
6 years ago [comment:13]
videlec
commented
6 years ago Not happy with?
diff --git a/build/pkgs/cryptominisat/dependencies b/build/pkgs/cryptominisat/dependencies
index df51e31274..a199426946 100644
--- a/build/pkgs/cryptominisat/dependencies
+++ b/build/pkgs/cryptominisat/dependencies
@@ -1,4 +1,4 @@
-$(PYTHON) | cmake sqlite m4ri boost_cropped
+$(PYTHON) | cmake sqlite m4ri boost_cropped zlib libpngI meant normal dependencies meaning before the | symbol.
7ed8c4ca-6d56-4ae9-953a-41e42b4ed313
commented
6 years ago 7ed8c4ca-6d56-4ae9-953a-41e42b4ed313
commented
6 years ago Branch pushed to git repo; I updated commit sha1. New commits:
2d9675c | 25480: fix dependencies |
embray
commented
6 years ago 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...
embray
commented
6 years ago Upstream PR if you want to make a patch from it: https://github.com/msoos/cryptominisat/pull/499
embray
commented
6 years ago Other than that issue, LGTM.
slel
commented
6 years ago Description changed:
---
+++
@@ -1,9 +1,9 @@
-Update cryptominisat to 5.6.3.
+Update cryptominisat to 5.6.4.
Tarball at
- https://github.com/msoos/cryptominisat/archive/5.6.3.tar.gz
+ https://github.com/msoos/cryptominisat/archive/5.6.4.tar.gz
-(to be renamed cryptominisat-5.6.3.tar.gz)
+(to be renamed cryptominisat-5.6.4.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 installation have to be removed because of interference of header files (see e.g. [issue 5](https://github.com/msoos/cryptominisat/issues/496)).
+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](https://github.com/msoos/cryptominisat/issues/496)).Cryptominisat 5.6.4 was released. Would be nice to get this in Sage 8.4.
edd8e884-f507-429a-b577-5d554626c0fe
commented
6 years ago Description changed:
---
+++
@@ -1,9 +1,9 @@
-Update cryptominisat to 5.6.4.
+Update cryptominisat to 5.6.5.
Tarball at
- https://github.com/msoos/cryptominisat/archive/5.6.4.tar.gz
+ https://github.com/msoos/cryptominisat/archive/5.6.5.tar.gz
-(to be renamed cryptominisat-5.6.4.tar.gz)
+(to be renamed cryptominisat-5.6.5.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](https://github.com/msoos/cryptominisat/issues/496)).CryptoMiniSat 5.6.5 is out and contains Erik's fix, let's see how it works.
edd8e884-f507-429a-b577-5d554626c0fe
commented
6 years ago Changed branch from u/vdelecroix/25480 to u/tmonteil/25480
edd8e884-f507-429a-b577-5d554626c0fe
commented
6 years ago Attachment: cryptominisat-5.6.5.log
edd8e884-f507-429a-b577-5d554626c0fe
commented
6 years ago edd8e884-f507-429a-b577-5d554626c0fe
commented
6 years ago 7ed8c4ca-6d56-4ae9-953a-41e42b4ed313
commented
5 years ago 7ed8c4ca-6d56-4ae9-953a-41e42b4ed313
commented
5 years ago edd8e884-f507-429a-b577-5d554626c0fe
commented
5 years ago Changed author from Vincent Delecroix to Vincent Delecroix, Thierry Monteil
edd8e884-f507-429a-b577-5d554626c0fe
commented
5 years ago 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.
edd8e884-f507-429a-b577-5d554626c0fe
commented
5 years ago Description changed:
---
+++
@@ -1,9 +1,9 @@
-Update cryptominisat to 5.6.5.
+Update cryptominisat to 5.6.6.
Tarball at
- https://github.com/msoos/cryptominisat/archive/5.6.5.tar.gz
+ https://github.com/msoos/cryptominisat/archive/5.6.6.tar.gz
-(to be renamed cryptominisat-5.6.5.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](https://github.com/msoos/cryptominisat/issues/496)).
Update cryptominisat to 5.6.6.
Tarball at
(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).
CC: @sagetrac-tmonteil @embray @saraedum @slel
Component: packages: optional
Keywords: cryptominisat, upgrade
Author: Vincent Delecroix, Thierry Monteil
Branch/Commit:
d483861Reviewer: Jeroen Demeyer, Vincent Delecroix
Issue created by migration from https://trac.sagemath.org/ticket/25480