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: | sage-8.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 cryptominisat-5.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 sage-8.7 to sage-8.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 follow-up: ↓ 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 32-bit VM. We should inspect further.
comment:9 Changed 3 years ago by
I re-checked: 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 python3-compatible 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 sage-8.8 to sage-8.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 py3-compatibility !
Maybe we can still update, even if this does not fix the 32-bit 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/sage-source/local/var/tmp/sage/build/cryptominisat-5.6.8/src/cmsat5-src && /opt/sagemath/sage-source/local/bin/cmake -E cmake_link_script CMakeFiles/cryptominisat5-bin.dir/link.txt --verbose=ON /usr/bin/g++ -std=gnu++11 -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 -Wunreachable-code -ggdb3 -Wlogical-op -Wnull-dereference -Wdouble-promotion -Wshadow -Wformat=2 -pedantic -L/opt/sagemath/sage-source/local/lib -Wl,-rpath,/opt/sagemath/sage-source/local/lib -O2 -Wl,--discard-all -Wl,--build-id=sha1 -rdynamic CMakeFiles/cryptominisat5-bin.dir/main.cpp.o CMakeFiles/cryptominisat5-bin.dir/main_exe.cpp.o CMakeFiles/cryptominisat5-bin.dir/signalcode.cpp.o -o ../cryptominisat5 -Wl,-rpath,/opt/sagemath/sage-source/local/var/tmp/sage/build/cryptominisat-5.6.8/src/lib: ../lib/libcryptominisat5.so.5.6 /usr/lib/x86_64-linux-gnu/libz.so /usr/lib/x86_64-linux-gnu/libboost_program_options.so /opt/sagemath/sage-source/local/lib/libm4ri.so -pthread /opt/sagemath/sage-source/local/lib/libpng16.so.16: undefined reference to `inflateValidate@ZLIB_1.2.9' collect2: error: ld returned 1 exit status cmsat5-src/CMakeFiles/cryptominisat5-bin.dir/build.make:117: recipe for target 'cryptominisat5' failed make[4]: *** [cryptominisat5] Error 1 make[4]: Leaving directory '/opt/sagemath/sage-source/local/var/tmp/sage/build/cryptominisat-5.6.8/src' CMakeFiles/Makefile2:197: recipe for target 'cmsat5-src/CMakeFiles/cryptominisat5-bin.dir/all' failed make[3]: *** [cmsat5-src/CMakeFiles/cryptominisat5-bin.dir/all] Error 2 make[3]: Leaving directory '/opt/sagemath/sage-source/local/var/tmp/sage/build/cryptominisat-5.6.8/src' Makefile:129: recipe for target 'all' failed make[2]: *** [all] Error 2 make[2]: Leaving directory '/opt/sagemath/sage-source/local/var/tmp/sage/build/cryptominisat-5.6.8/src' ******************************************************************************** Error building cryptominisat-5.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 follow-up: ↓ 19 Changed 3 years ago by
This looks like an attempt to update, rather than a full re-build 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 libpng-clean
), 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 ; follow-up: ↓ 20 Changed 3 years ago by
Replying to dimpase:
This looks like an attempt to update, rather than a full re-build 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 libpng-clean
), 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 re-build 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 libpng-clean
), 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 force-install 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/sage-source/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)