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: sage-9.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/25374-cryptominisat-5.8.0 (Commits, GitHub, GitLab) Commit: 5603e11e1a6bd62ef6f3e9a092de22a8433d05cc
Dependencies: #25372 Stopgaps:

Status badges

Description (last modified by slelievre)

This is to upgrade to CryptoMiniSat 5.8.0, released 2020-07-06.

Release notes for the versions since 5.6.8 (current in Sage):

5.8.0

Massive new release! Many-many improvements:

  • Gauss-Jordan 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
  • Many-many 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 embray

  • Authors set to Erik Bray
  • 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

New commits:

48159c7Use sage-dist-helpers to add DESTDIR support in cryptominisat
312f1ebadd a patch to cryptominisat so that when it installs its Python package that also respects DESTDIR
e2b30c0adds patch for cryptominisat to build and install correctly on Cygwin

comment:2 Changed 3 years ago by embray

  • 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 saraedum

  • Reviewers set to Julian Rüth

I'm confused. Doesn't this add -g twice?

comment:4 Changed 3 years ago by saraedum

  • Status changed from needs_review to needs_info

comment:5 Changed 3 years ago by embray

  • 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 git

  • Commit changed from e2b30c09c02eb249a04a8d78d3bdbcce994247dc to e98cb15313749d32965823f126dc609e4aebc6e1

Branch pushed to git repo; I updated commit sha1. This was a forced push. New commits:

e98cb15adds patch for cryptominisat to build and install correctly on Cygwin

comment:7 Changed 3 years ago by vdelecroix

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 embray

This might be mostly superseded by #25480, except maybe for the spkg-install updates. I'll test and see...

comment:9 Changed 3 years ago by saraedum

Any update on this?

comment:10 Changed 3 years ago by embray

  • Milestone changed from sage-8.3 to sage-8.4

I believe this issue can reasonably be addressed for Sage 8.4.

comment:11 Changed 3 years ago by embray

  • Milestone changed from sage-8.4 to sage-8.5

comment:12 Changed 2 years ago by embray

  • Milestone changed from sage-8.5 to sage-8.7

Retargeting some of my tickets (somewhat optimistically for now).

comment:13 Changed 2 years ago by jdemeyer

What's the status of this now after #25480?

comment:14 Changed 2 years ago by embray

  • 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 embray

  • Owner changed from (none) to embray

comment:16 Changed 2 years ago by embray

  • Milestone changed from sage-8.7 to sage-8.8

Moving all my in-progress tickets to 8.8 milestone.

comment:17 Changed 2 years ago by embray

  • 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:18 Changed 17 months ago by embray

  • Milestone changed from sage-8.9 to sage-9.1

Ticket retargeted after milestone closed

comment:19 Changed 13 months ago by mkoeppe

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 sub-command REPLACE requires at least four arguments.


-- Python CFLAGS:  '-Wno-unused-result -Wsign-compare -DNDEBUG -g -fwrapv -O3 -Wall -ggdb -O2 -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fstack-protector-strong --param=ssp-buffer-size=4 -fdebug-prefix-map=/cygdrive/d/cyg_pub/devel/python/python37/python37-3.7.7-1.x86_64/build=/usr/src/debug/python37-3.7.7-1 -fdebug-prefix-map=/cygdrive/d/cyg_pub/devel/python/python37/python37-3.7.7-1.x86_64/src/Python-3.7.7=/usr/src/debug/python37-3.7.7-1 -ggdb -O2 -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fstack-protector-strong --param=ssp-buffer-size=4 -fdebug-prefix-map=/cygdrive/d/cyg_pub/devel/python/python37/python37-3.7.7-1.x86_64/build=/usr/src/debug/python37-3.7.7-1 -fdebug-prefix-map=/cygdrive/d/cyg_pub/devel/python/python37/python37-3.7.7-1.x86_64/src/Python-3.7.7=/usr/src/debug/python37-3.7.7-1'
-- 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/cryptominisat-5.6.8/src/CMakeFiles/CMakeOutput.log".
See also "/cygdrive/d/a/sage/sage/local/var/tmp/sage/build/cryptominisat-5.6.8/src/CMakeFiles/CMakeError.log".
********************************************************************************
Error configuring cryptominisat-5.6.8 with cmake
See the file
    /cygdrive/d/a/sage/sage/local/var/tmp/sage/build/cryptominisat-5.6.8/src/CMakeFiles/CMakeOutput.log
for details.
********************************************************************************

comment:20 Changed 13 months ago by mkoeppe

  • Milestone changed from sage-9.1 to sage-9.2

comment:21 follow-up: Changed 13 months ago by 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.

Last edited 13 months ago by slelievre (previous) (diff)

comment:22 Changed 13 months ago by mkoeppe

  • 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 mkoeppe

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 mkoeppe

  • Cc novoselt added

comment:25 Changed 10 months ago by mkoeppe

  • Description modified (diff)

comment:26 Changed 10 months ago by slelievre

CryptoMiniSat 5.8.0 was released on 2020-07-06.

Last edited 10 months ago by slelievre (previous) (diff)

comment:27 Changed 10 months ago by mkoeppe

Instructions for doing the upgrade:

1) Add upstream_url field to checksums.ini https://wiki.sagemath.org/ReleaseTours/sage-9.1#For_developers-1

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 novoselt

The needed URL is

upstream_url=https://github.com/msoos/cryptominisat/archive/VERSION.tar.gz

comment:29 Changed 10 months ago by slelievre

Forgot about this and opened #30264. I'm setting it to duplicate.

comment:30 Changed 9 months ago by mkoeppe

  • Description modified (diff)

Would someone like to update the branch please?

comment:31 Changed 9 months ago by slelievre

  • Branch changed from u/embray/cygwin/build/cryptominisat to public/25374-cryptominisat-5.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 --random-seed=0 src/sage/sat/boolean_polynomials.py
too many failed tests, not using stored timings
Running doctests with ID 2020-08-13-14-39-55-b4ff37bc.
Git branch: develop
Using --optional=build,cryptominisat,dochtml,memlimit,sage
Doctesting 1 file.
sage -t --long --random-seed=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] truth-find 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] truth-find 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 --random-seed=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 mkoeppe

  • Cc fbissey added

comment:33 Changed 9 months ago by mkoeppe

For broader testing, push a tag to github...

comment:34 Changed 9 months ago by slelievre

  • Description modified (diff)

The extra verbosity needs fixing before wider testing. Help needed.

comment:35 Changed 9 months ago by slelievre

  • 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 tmonteil

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 tmonteil

  • Status changed from needs_review to needs_work

So, i expect the doctest to fail.

comment:38 Changed 7 months ago by mkoeppe

  • Milestone changed from sage-9.2 to sage-9.3

comment:39 Changed 6 months ago by mkoeppe

Currently we build cryptominisat including its Python bindings (pycryptosat). This is slightly problematic for the plan to separate non-Python 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 mkoeppe

  • Milestone changed from sage-9.3 to sage-9.4

Setting new milestone based on a cursory review of ticket status, priority, and last modification date.

Note: See TracTickets for help on using tickets.