Opened 3 years ago
Last modified 3 months ago
#25374 needs_work defect
Upgrade cryptominisat to fix cryptominisat build on Cygwin
Reported by:  embray  Owned by:  embray 

Priority:  minor  Milestone:  sage9.4 
Component:  porting: Cygwin  Keywords:  upgrade, cryptominisat 
Cc:  slelievre, tscrim, jmantysalo, embray, jdemeyer, saraedum, tmonteil, vdelecroix, mjo, novoselt, fbissey  Merged in:  
Authors:  Erik Bray  Reviewers:  Julian Rüth 
Report Upstream:  Fixed upstream, in a later stable release.  Work issues:  
Branch:  public/25374cryptominisat5.8.0 (Commits, GitHub, GitLab)  Commit:  5603e11e1a6bd62ef6f3e9a092de22a8433d05cc 
Dependencies:  #25372  Stopgaps: 
Description (last modified by )
This is to upgrade to CryptoMiniSat 5.8.0, released 20200706.
Release notes for the versions since 5.6.8 (current in Sage):
5.8.0
Massive new release! Manymany improvements:
 GaussJordan elimination is enabled by default
 Target Phases ("Stable Polarities") are used
 CCAnr SLS solver is enabled and is set to work by default
 Hybrid variable branching heuristics
 Manymany speed improvements
 Better DIMACS parsing to work for other systems
 Made to work with new ApproxMC and UniGen
5.7.1
 Removing LSIDS, as it was interfering with performance.
5.7.0
 Improved parameters
 Hybrid branching strategies
 and much more
Previous upgrade:
 #27319: Upgrade to Cryptominisat 5.6.8  merged in Sage 8.9.beta2
Change History (40)
comment:1 Changed 3 years ago by
 Branch set to u/embray/cygwin/build/cryptominisat
 Cc slelievre added
 Commit set to e2b30c09c02eb249a04a8d78d3bdbcce994247dc
 Dependencies set to #25372
 Report Upstream changed from N/A to Not yet reported upstream; Will do shortly.
 Status changed from new to needs_review
comment:2 Changed 3 years ago by
 Report Upstream changed from Not yet reported upstream; Will do shortly. to Fixed upstream, but not in a stable release.
Turns out there's nothing to report upstream, because the problems with Cygwin are already fixed there. However, the Cygwin fixes are kind of incidental to other changes. Until/unless we upgrade this package in Sage, these specifically targeted fixes are simpler to patch in than the larger changes in upstream.
comment:3 Changed 3 years ago by
 Reviewers set to Julian Rüth
I'm confused. Doesn't this add g
twice?
comment:4 Changed 3 years ago by
 Status changed from needs_review to needs_info
comment:5 Changed 3 years ago by
 Status changed from needs_info to needs_review
Yes, I had intended to remove the g
from those earlier lines.
comment:6 Changed 3 years ago by
 Commit changed from e2b30c09c02eb249a04a8d78d3bdbcce994247dc to e98cb15313749d32965823f126dc609e4aebc6e1
Branch pushed to git repo; I updated commit sha1. This was a forced push. New commits:
e98cb15  adds patch for cryptominisat to build and install correctly on Cygwin

comment:7 Changed 3 years ago by
Please see how it looks like with the new release #25480. Do you want to put this ticket as a dependency?
comment:8 Changed 3 years ago by
This might be mostly superseded by #25480, except maybe for the spkginstall
updates.
I'll test and see...
comment:9 Changed 3 years ago by
Any update on this?
comment:10 Changed 3 years ago by
 Milestone changed from sage8.3 to sage8.4
I believe this issue can reasonably be addressed for Sage 8.4.
comment:11 Changed 3 years ago by
 Milestone changed from sage8.4 to sage8.5
comment:12 Changed 2 years ago by
 Milestone changed from sage8.5 to sage8.7
Retargeting some of my tickets (somewhat optimistically for now).
comment:13 Changed 2 years ago by
What's the status of this now after #25480?
comment:14 Changed 2 years ago by
 Status changed from needs_review to needs_work
I'll have to give it another try. Maybe this is fixed by #25480? I haven't checked.
comment:15 Changed 2 years ago by
 Owner changed from (none) to embray
comment:16 Changed 2 years ago by
 Milestone changed from sage8.7 to sage8.8
Moving all my inprogress tickets to 8.8 milestone.
comment:17 Changed 2 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:18 Changed 17 months ago by
 Milestone changed from sage8.9 to sage9.1
Ticket retargeted after milestone closed
comment:19 Changed 13 months ago by
Building cryptominisat is still broken with 9.1.rc2 (https://github.com/mkoeppe/sage/runs/641394520)
 Found python interpreter, libs and header files  Building python interface CMake Error at python/CMakeLists.txt:44 (string): string subcommand REPLACE requires at least four arguments.  Python CFLAGS: 'Wnounusedresult Wsigncompare DNDEBUG g fwrapv O3 Wall ggdb O2 pipe Wall Werror=formatsecurity Wp,D_FORTIFY_SOURCE=2 fstackprotectorstrong param=sspbuffersize=4 fdebugprefixmap=/cygdrive/d/cyg_pub/devel/python/python37/python373.7.71.x86_64/build=/usr/src/debug/python373.7.71 fdebugprefixmap=/cygdrive/d/cyg_pub/devel/python/python37/python373.7.71.x86_64/src/Python3.7.7=/usr/src/debug/python373.7.71 ggdb O2 pipe Wall Werror=formatsecurity Wp,D_FORTIFY_SOURCE=2 fstackprotectorstrong param=sspbuffersize=4 fdebugprefixmap=/cygdrive/d/cyg_pub/devel/python/python37/python373.7.71.x86_64/build=/usr/src/debug/python373.7.71 fdebugprefixmap=/cygdrive/d/cyg_pub/devel/python/python37/python373.7.71.x86_64/src/Python3.7.7=/usr/src/debug/python373.7.71'  Python LDFLAGS: 'lcrypt lintl ldl'  Python LINKFORSHARED flags: ''  Python module will be installed to : '/cygdrive/d/a/sage/sage/local'  Configuring incomplete, errors occurred! See also "/cygdrive/d/a/sage/sage/local/var/tmp/sage/build/cryptominisat5.6.8/src/CMakeFiles/CMakeOutput.log". See also "/cygdrive/d/a/sage/sage/local/var/tmp/sage/build/cryptominisat5.6.8/src/CMakeFiles/CMakeError.log". ******************************************************************************** Error configuring cryptominisat5.6.8 with cmake See the file /cygdrive/d/a/sage/sage/local/var/tmp/sage/build/cryptominisat5.6.8/src/CMakeFiles/CMakeOutput.log for details. ********************************************************************************
comment:20 Changed 13 months ago by
 Milestone changed from sage9.1 to sage9.2
comment:21 followup: ↓ 23 Changed 13 months ago by
There's a new release of CryptoMiniSat. The issue here was said to be fixed upstream so it might be enough to upgrade to CryptoMiniSat 5.7.1.
comment:22 Changed 13 months ago by
 Cc tscrim jmantysalo embray jdemeyer saraedum tmonteil vdelecroix mjo added
 Summary changed from Fix cryptominisat build on Cygwin to Upgrade cryptominisat to fix cryptominisat build on Cygwin
comment:23 in reply to: ↑ 21 Changed 13 months ago by
Replying to slelievre:
There's a new release of CryptoMiniSat. The issue here was said to be fixed upstream so it might be enough to upgrade to CryptoMiniSat 5.7.1.
OK who wants to work on it?
comment:24 Changed 10 months ago by
 Cc novoselt added
comment:25 Changed 10 months ago by
 Description modified (diff)
comment:26 Changed 10 months ago by
CryptoMiniSat 5.8.0 was released on 20200706.
comment:27 Changed 10 months ago by
Instructions for doing the upgrade:
1) Add upstream_url
field to checksums.ini
https://wiki.sagemath.org/ReleaseTours/sage9.1#For_developers1
2) Run ./sage package update cryptominisat 5.8.0
3) Remove patches
4) Try build on local machine
5) Push to the ticket
comment:28 Changed 10 months ago by
The needed URL is
upstream_url=https://github.com/msoos/cryptominisat/archive/VERSION.tar.gz
comment:29 Changed 10 months ago by
Forgot about this and opened #30264. I'm setting it to duplicate.
comment:30 Changed 9 months ago by
 Description modified (diff)
Would someone like to update the branch please?
comment:31 Changed 9 months ago by
 Branch changed from u/embray/cygwin/build/cryptominisat to public/25374cryptominisat5.8.0
 Commit changed from e98cb15313749d32965823f126dc609e4aebc6e1 to 5603e11e1a6bd62ef6f3e9a092de22a8433d05cc
 Description modified (diff)
 Keywords upgrade cryptominisat added
With this branch, make cryptominisat
and sage i cryptominisat
succeed.
They used to fail with Sage 9.x for the previous version of the package.
Tested on Debian 10 buster and macOS 10.14.6 Mojave. Cygwin testing needed.
New doctest failure (both on Debian and macOS):
$ OPT='optional=build,cryptominisat,dochtml,memlimit,sage' $ ./sage t long $OPT randomseed=0 src/sage/sat/boolean_polynomials.py too many failed tests, not using stored timings Running doctests with ID 20200813143955b4ff37bc. Git branch: develop Using optional=build,cryptominisat,dochtml,memlimit,sage Doctesting 1 file. sage t long randomseed=0 src/sage/sat/boolean_polynomials.py ********************************************************************** File "src/sage/sat/boolean_polynomials.py", line 131, in sage.sat.boolean_polynomials.solve Failed example: sr = sage.crypto.mq.SR(1, 4, 4, 8, allow_zero_inversions = True) # optional  cryptominisat, long time Expected nothing Got: c [g 0] truthfind prop checks : 156 c [g 0] > of which prop : 22.44 % c [g 0] > of which confl : 0.64 % c [g 0] elim called : 54 c [g 0] > which lead to prop : 22.22 % c [g 0] > which lead to confl: 0.00 % c [g 0] size: 12 x 24 c [g 1] truthfind prop checks : 178 c [g 1] > of which prop : 51.12 % c [g 1] > of which confl : 0.00 % c [g 1] elim called : 150 c [g 1] > which lead to prop : 11.33 % c [g 1] > which lead to confl: 0.00 % c [g 1] size: 12 x 24 ********************************************************************** 1 item had failures: 1 of 40 in sage.sat.boolean_polynomials.solve [45 tests, 1 failure, 80.53 s]  sage t long randomseed=0 src/sage/sat/boolean_polynomials.py # 1 doctest failed  Total time for all tests: 80.6 seconds cpu time: 82.1 seconds cumulative wall time: 80.5 seconds
New commits:
5603e11  #25374 Upgrade to CryptoMiniSat 5.8.0

comment:32 Changed 9 months ago by
 Cc fbissey added
comment:33 Changed 9 months ago by
For broader testing, push a tag to github...
comment:34 Changed 9 months ago by
 Description modified (diff)
The extra verbosity needs fixing before wider testing. Help needed.
comment:35 Changed 9 months ago by
 Report Upstream changed from Fixed upstream, but not in a stable release. to Fixed upstream, in a later stable release.
 Status changed from needs_work to needs_review
Or maybe it only happens on my machine?
comment:36 Changed 9 months ago by
I had a look some time ago, i also had such issues, so it is not only on your machine. If i understood correctly (to be checked), it is possible that the verbosity happens when a cryptominisat instance is run while another is still running, as if we got the log of the previous instance (?). You could inspect by adding some sleep between doctests, just to check.
comment:37 Changed 9 months ago by
 Status changed from needs_review to needs_work
So, i expect the doctest to fail.
comment:38 Changed 7 months ago by
 Milestone changed from sage9.2 to sage9.3
comment:39 Changed 6 months ago by
Currently we build cryptominisat including its Python bindings (pycryptosat
).
This is slightly problematic for the plan to separate nonPython packages (SAGE_LOCAL
) from Python packages (SAGE_VENV
), see #29013 (and #30534 for pynac
).
But there is also https://pypi.org/project/pycryptosat/, which can be installed separately. Its release history seems to be out of sync with cryptominisat.
comment:40 Changed 3 months ago by
 Milestone changed from sage9.3 to sage9.4
Setting new milestone based on a cursory review of ticket status, priority, and last modification date.
New commits:
Use sagedisthelpers to add DESTDIR support in cryptominisat
add a patch to cryptominisat so that when it installs its Python package that also respects DESTDIR
adds patch for cryptominisat to build and install correctly on Cygwin