Opened 3 years ago
Closed 3 years ago
#27319 closed task (fixed)
Upgrade to Cryptominisat 5.6.8
Reported by:  slelievre  Owned by:  

Priority:  major  Milestone:  sage8.9 
Component:  packages: optional  Keywords:  upgrade, cryptominisat 
Cc:  embray, jdemeyer, saraedum, slelievre, tmonteil, vdelecroix, mjo  Merged in:  
Authors:  Frédéric Chapoton  Reviewers:  Thierry Monteil 
Report Upstream:  N/A  Work issues:  
Branch:  d219646 (Commits, GitHub, GitLab)  Commit:  d219646cd4dec96a1b4e53cce1f14aa9905377c3 
Dependencies:  Stopgaps: 
Description (last modified by )
This ticket is to upgrade to Cryptominisat 5.6.8.
Tarball (to be renamed cryptominisat5.6.8.tar.gz):
Our last upgrade was to Cryptominisat 5.6.6 in #25480.
Release notes (from the Cryptominisat releases page on GitHub):
 Cryptominisat 5.6.7
Some fixes and misc improvements. Also, a slightly changed naming for the independent variables. They are really sampling variables and so the interface has been renamed accordingly.
 Cryptominisat 5.6.8
Fixing Windows build
Change History (24)
comment:1 Changed 3 years ago by
 Component changed from PLEASE CHANGE to packages: optional
 Type changed from PLEASE CHANGE to task
comment:2 Changed 3 years ago by
 Description modified (diff)
 Summary changed from Upgrade to cryptominisat 5.6.7 to Upgrade to Cryptominisat 5.6.8
comment:3 Changed 3 years ago by
 Milestone changed from sage8.7 to sage8.8
comment:4 Changed 3 years ago by
 Branch set to u/chapoton/27319
 Commit set to 3a89fb243abcb77535ca5966944e0492739866e2
 Status changed from new to needs_review
New commits:
3a89fb2  update cryptominisat to 5.6.8

comment:5 Changed 3 years ago by
Here is a branch.
comment:6 Changed 3 years ago by
 Reviewers set to Thierry Monteil
comment:7 followup: ↓ 8 Changed 3 years ago by
by the way, any idea on the following failure of the arando patchbot ?
sage t long src/sage/sat/boolean_polynomials.py ********************************************************************** File "src/sage/sat/boolean_polynomials.py", line 146, in sage.sat.boolean_polynomials.solve Failed example: len(sls_aes) # optional  cryptominisat, long time Expected: 256 Got: 18 ********************************************************************** 1 item had failures: 1 of 41 in sage.sat.boolean_polynomials.solve [46 tests, 1 failure, 186.16 s]  sage t long src/sage/sat/boolean_polynomials.py # 1 doctest failed
comment:8 in reply to: ↑ 7 Changed 3 years ago by
 Status changed from needs_review to needs_work
Replying to chapoton:
by the way, any idea on the following failure of the arando patchbot ?
sage t long src/sage/sat/boolean_polynomials.py ********************************************************************** File "src/sage/sat/boolean_polynomials.py", line 146, in sage.sat.boolean_polynomials.solve Failed example: len(sls_aes) # optional  cryptominisat, long time Expected: 256 Got: 18 ********************************************************************** 1 item had failures: 1 of 41 in sage.sat.boolean_polynomials.solve [46 tests, 1 failure, 186.16 s]  sage t long src/sage/sat/boolean_polynomials.py # 1 doctest failed
I have a similar issue on a 32bit VM. We should inspect further.
comment:9 Changed 3 years ago by
I rechecked: the problem was already here on 5.6.6, but not on 5.0.1.
comment:10 Changed 3 years ago by
 Commit changed from 3a89fb243abcb77535ca5966944e0492739866e2 to d219646cd4dec96a1b4e53cce1f14aa9905377c3
Branch pushed to git repo; I updated commit sha1. This was a forced push. New commits:
d219646  update cryptominisat to 5.6.8

comment:11 Changed 3 years ago by
I have made the necessary changes for python3compatible doctests (because one cannot compare dicts in python3)
I have also replaced eqs = map(R, eqs)
by list comprehension in the line before the failing doctest in src/sage/sat/boolean_polynomials.py
.
comment:12 Changed 3 years ago by
 Milestone changed from sage8.8 to sage8.9
Tickets still needing working or clarification should be moved to the next release milestone at the soonest (please feel free to revert if you think the ticket is close to being resolved).
comment:13 Changed 3 years ago by
The result of the failing doctest on arando seems to be random, varying from 16 to 25.
comment:14 Changed 3 years ago by
 Status changed from needs_work to needs_review
Thierry, or somebody else, please have a look. This contains some changes that are required for py3compatibility !
Maybe we can still update, even if this does not fix the 32bit doctest. But maybe it does ?
comment:15 Changed 3 years ago by
Damn, now i have an issue building cryptominisat on 64 standard machine:
[ 94%] Linking CXX executable ../cryptominisat5 cd /opt/sagemath/sagesource/local/var/tmp/sage/build/cryptominisat5.6.8/src/cmsat5src && /opt/sagemath/sagesource/local/bin/cmake E cmake_link_script CMakeFiles/cryptominisat5bin.dir/link.txt verbose=ON /usr/bin/g++ std=gnu++11 mtune=native Wall Wextra Wunused Wsigncompare fnoomitframepointer Wtypelimits Wuninitialized Wnodeprecated Wstrictaliasing Wpointerarith Wpointerarith Wformatnonliteral Winitself Wparentheses Wunreachablecode ggdb3 Wlogicalop Wnulldereference Wdoublepromotion Wshadow Wformat=2 pedantic L/opt/sagemath/sagesource/local/lib Wl,rpath,/opt/sagemath/sagesource/local/lib O2 Wl,discardall Wl,buildid=sha1 rdynamic CMakeFiles/cryptominisat5bin.dir/main.cpp.o CMakeFiles/cryptominisat5bin.dir/main_exe.cpp.o CMakeFiles/cryptominisat5bin.dir/signalcode.cpp.o o ../cryptominisat5 Wl,rpath,/opt/sagemath/sagesource/local/var/tmp/sage/build/cryptominisat5.6.8/src/lib: ../lib/libcryptominisat5.so.5.6 /usr/lib/x86_64linuxgnu/libz.so /usr/lib/x86_64linuxgnu/libboost_program_options.so /opt/sagemath/sagesource/local/lib/libm4ri.so pthread /opt/sagemath/sagesource/local/lib/libpng16.so.16: undefined reference to `inflateValidate@ZLIB_1.2.9' collect2: error: ld returned 1 exit status cmsat5src/CMakeFiles/cryptominisat5bin.dir/build.make:117: recipe for target 'cryptominisat5' failed make[4]: *** [cryptominisat5] Error 1 make[4]: Leaving directory '/opt/sagemath/sagesource/local/var/tmp/sage/build/cryptominisat5.6.8/src' CMakeFiles/Makefile2:197: recipe for target 'cmsat5src/CMakeFiles/cryptominisat5bin.dir/all' failed make[3]: *** [cmsat5src/CMakeFiles/cryptominisat5bin.dir/all] Error 2 make[3]: Leaving directory '/opt/sagemath/sagesource/local/var/tmp/sage/build/cryptominisat5.6.8/src' Makefile:129: recipe for target 'all' failed make[2]: *** [all] Error 2 make[2]: Leaving directory '/opt/sagemath/sagesource/local/var/tmp/sage/build/cryptominisat5.6.8/src' ******************************************************************************** Error building cryptominisat5.6.8
Let me rebuild libpng
in case.
comment:16 Changed 3 years ago by
I still have the issue after rebuilding libpng
(and a large part of Sage). Note that i merged with Sage 8.8, could the problem be related to #27186 ?
comment:17 followup: ↓ 19 Changed 3 years ago by
This looks like an attempt to update, rather than a full rebuild after make distclean
.
Now Sage will try using libpng from your system. Blindly doing ./sage f libpng
might actually be breaking your build, if it is not followed by ./configure
.
In any event, this is one of significant changes to configure, and all bets are off whether make distclean
is needed.
Could you try uninstalling libpng
? (make libpngclean
), then ./configure
and see whether libpng
is picked from the system or not?
comment:18 Changed 3 years ago by
the update works for me on the 8.8.bera1, on Gentoo Linux
comment:19 in reply to: ↑ 17 ; followup: ↓ 20 Changed 3 years ago by
Replying to dimpase:
This looks like an attempt to update, rather than a full rebuild after
make distclean
.Now Sage will try using libpng from your system. Blindly doing
./sage f libpng
might actually be breaking your build, if it is not followed by./configure
. In any event, this is one of significant changes to configure, and all bets are off whethermake distclean
is needed.Could you try uninstalling
libpng
? (make libpngclean
), then./configure
and see whetherlibpng
is picked from the system or not?
I will give a try, but it should also work with the libpng
provided by Sage.
comment:20 in reply to: ↑ 19 Changed 3 years ago by
Thierry, I have troubles with the patchbot server. Could you please phone me ?
Replying to tmonteil:
Replying to dimpase:
This looks like an attempt to update, rather than a full rebuild after
make distclean
.Now Sage will try using libpng from your system. Blindly doing
./sage f libpng
might actually be breaking your build, if it is not followed by./configure
. In any event, this is one of significant changes to configure, and all bets are off whethermake distclean
is needed.Could you try uninstalling
libpng
? (make libpngclean
), then./configure
and see whetherlibpng
is picked from the system or not?I will give a try, but it should also work with the
libpng
provided by Sage.
comment:21 Changed 3 years ago by
well, I can guess what happens with libpng. We have now a check that if system libpng is available then system zlib is used, and it need not be compatible with Sage's libpng.
If you override this and forceinstall libpng in Sage then for some reason a compatible zlib doesn't get installed, and we see this error (which should be fixable by manually installing Sage's zlib)
comment:22 Changed 3 years ago by
 Cc mjo added
As I noted over in #27186, libpng won't even use inflateValidate
unless the zlib headers are new enough to have it. Note that Sage's zlib does have inflateValidate
. If I had to guess, this error,
/opt/sagemath/sagesource/local/lib/libpng16.so.16: undefined reference to `inflateValidate@ZLIB_1.2.9'
suggests to me that (Sage's) libpng was built against new headers that do have inflateValidate
, and then linked against an older (system) copy of zlib that doesn't have inflateValidate
.
We'll need the gory details of your libpng build, including the header/library search path used during the build. (If I knew how to get those off the top of my head I'd be telling you how to do it; I'll need to come back to this when I have some free time.)
comment:23 Changed 3 years ago by
 Status changed from needs_review to positive_review
comment:24 Changed 3 years ago by
 Branch changed from u/chapoton/27319 to d219646cd4dec96a1b4e53cce1f14aa9905377c3
 Resolution set to fixed
 Status changed from positive_review to closed
Ticket retargeted after milestone closed (if you don't believe this ticket is appropriate for the Sage 8.8 release please retarget manually)