Upgrade cryptominisat to 5.8.0, fix build on Cygwin

[embray]

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

Tarball at: https://github.com/msoos/cryptominisat/archive/refs/tags/5.8.0.tar.gz

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

Upstream: Fixed upstream, in a later stable release.

CC: @slel @tscrim @jm58660 @embray @jdemeyer @saraedum @sagetrac-tmonteil @videlec @orlitzky @novoselt @kiwifb @dimpase

Component: packages: optional

Keywords: upgrade, cryptominisat

Author: Erik Bray, Thierry Monteil, François Bissey, Matthias Koeppe

Branch: 69033db

Reviewer: Travis Scrimshaw, Julian Rüth, Matthias Koeppe

Issue created by migration from https://trac.sagemath.org/ticket/25374

[embray]

Branch: u/embray/cygwin/build/cryptominisat

[embray]

Upstream: Not yet reported upstream; Will do shortly.

[embray]

Dependencies: #25372

[embray]

Author: Erik Bray

[embray]

Commit: e2b30c0

[embray]

New commits:

48159c7	Use sage-dist-helpers to add DESTDIR support in cryptominisat
312f1eb	add a patch to cryptominisat so that when it installs its Python package that also respects DESTDIR
e2b30c0	adds patch for cryptominisat to build and install correctly on Cygwin

[embray]

Changed upstream from Not yet reported upstream; Will do shortly. to Fixed upstream, but not in a stable release.

[embray]

comment:2

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.

[saraedum]

comment:3

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

[saraedum]

Reviewer: Julian Rüth

[embray]

comment:5

Yes, I had intended to remove the -g from those earlier lines.

[7ed8c4ca-6d56-4ae9-953a-41e42b4ed313]

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

[7ed8c4ca-6d56-4ae9-953a-41e42b4ed313]

Changed commit from e2b30c0 to e98cb15

[videlec]

comment:7

Please see how it looks like with the new release #25480. Do you want to put this ticket as a dependency?

[embray]

comment:8

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

[saraedum]

comment:9

Any update on this?

[embray]

comment:10

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

[embray]

comment:12

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

[jdemeyer]

comment:13

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

[embray]

comment:14

I'll have to give it another try. Maybe this is fixed by #25480? I haven't checked.

[embray]

comment:16

Moving all my in-progress tickets to 8.8 milestone.

[embray]

comment:17

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).

[embray]

comment:18

Ticket retargeted after milestone closed

[mkoeppe]

comment:19

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.
********************************************************************************

[slel]

comment:21

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.

[mkoeppe]

comment:23

Replying to @slel:

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?

[mkoeppe]

Description changed:

--- 
+++ 
@@ -1 +1,3 @@

+
+Previous update: #27319 Cryptominisat 5.6.8

[slel]

comment:26

CryptoMiniSat 5.8.0 was released on 2020-07-06.

[mkoeppe]

comment:27

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

[novoselt]

comment:28

The needed URL is

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

[slel]

comment:29

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

[mkoeppe]

Description changed:

--- 
+++ 
@@ -1,3 +1,22 @@
+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 update: #27319 Cryptominisat 5.6.8

[mkoeppe]

comment:30

Would someone like to update the branch please?

[slel]

Changed keywords from none to upgrade, cryptominisat

[slel]

Description changed:

[slel]

Changed commit from e98cb15 to 5603e11

[slel]

Changed branch from u/embray/cygwin/build/cryptominisat to public/25374-cryptominisat-5.8.0

[slel]

comment:31

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

[mkoeppe]

comment:33

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

[slel]

Description changed:

--- 
+++ 
@@ -2,21 +2,31 @@

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

-5.8.0
-Massive new release! Many-many improvements:
+>
+> == 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

-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 update: #27319 Cryptominisat 5.6.8
+Previous upgrade:
+
+- #27319: Upgrade to Cryptominisat 5.6.8 -- merged in Sage 8.9.beta2
+

[slel]

comment:34

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

[slel]

Changed upstream from Fixed upstream, but not in a stable release. to Fixed upstream, in a later stable release.

[slel]

comment:35

Or maybe it only happens on my machine?

[edd8e884-f507-429a-b577-5d554626c0fe]

comment:36

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.

[edd8e884-f507-429a-b577-5d554626c0fe]

comment:37

So, i expect the doctest to fail.

[mkoeppe]

comment:39

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.

[mkoeppe]

comment:40

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

[mkoeppe]

comment:41

Setting a new milestone for this ticket based on a cursory review.

[edd8e884-f507-429a-b577-5d554626c0fe]

comment:42

I forgot the existence of this ticket and created #32545 to get a faster cryptominisat, here is a branch that fixes the issue: i removed the s_verbosity=1 option of some doctest, since it produces noise to another unrelated doctest that appears later in the same file (which confirms comment:36).

I could not test on Cygwin.

[edd8e884-f507-429a-b577-5d554626c0fe]

Changed commit from 5603e11 to 824a597