Upgrade to Cryptominisat 5.6.8

[slelievre]

This ticket is to upgrade to Cryptominisat 5.6.8.

Tarball (to be renamed cryptominisat-5.6.8.tar.gz):

• ​​https://github.com/msoos/cryptominisat/archive/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

[embray]

Ticket retargeted after milestone closed (if you don't believe this ticket is appropriate for the Sage 8.8 release please retarget manually)

[chapoton]

New commits:

​3a89fb2

update cryptominisat to 5.6.8

[chapoton]

Here is a branch.

[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

[tmonteil]

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.

[tmonteil]

I re-checked: the problem was already here on 5.6.6, but not on 5.0.1.

[git]

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

​d219646

update cryptominisat to 5.6.8

[chapoton]

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.

[embray]

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

[chapoton]

The result of the failing doctest on arando seems to be random, varying from 16 to 25.

[chapoton]

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 ?

[tmonteil]

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.

[tmonteil]

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 ?

[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 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?

[dimpase]

the update works for me on the 8.8.bera1, on Gentoo Linux

[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 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?

I will give a try, but it should also work with the libpng provided by Sage.

[chapoton]

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 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?

I will give a try, but it should also work with the libpng provided by Sage.

[dimpase]

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)

[mjo]

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