Opened 2 years ago

Closed 22 months 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:

Status badges

Description (last modified by slelievre)

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 2 years ago by embray

  • Component changed from PLEASE CHANGE to packages: optional
  • Type changed from PLEASE CHANGE to task

comment:2 Changed 2 years ago by slelievre

  • Description modified (diff)
  • Summary changed from Upgrade to cryptominisat 5.6.7 to Upgrade to Cryptominisat 5.6.8

comment:3 Changed 2 years ago by embray

  • Milestone changed from sage-8.7 to sage-8.8

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

comment:4 Changed 2 years ago by chapoton

  • Authors set to Frédéric Chapoton
  • Branch set to u/chapoton/27319
  • Commit set to 3a89fb243abcb77535ca5966944e0492739866e2
  • Status changed from new to needs_review

New commits:

3a89fb2update cryptominisat to 5.6.8

comment:5 Changed 2 years ago by chapoton

Here is a branch.

comment:6 Changed 2 years ago by tmonteil

  • Reviewers set to Thierry Monteil

comment:7 follow-up: Changed 2 years ago by 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

comment:8 in reply to: ↑ 7 Changed 2 years ago by tmonteil

  • 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 2 years ago by tmonteil

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

comment:10 Changed 2 years ago by git

  • Commit changed from 3a89fb243abcb77535ca5966944e0492739866e2 to d219646cd4dec96a1b4e53cce1f14aa9905377c3

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

d219646update cryptominisat to 5.6.8

comment:11 Changed 2 years ago by 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.

comment:12 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:13 Changed 2 years ago by chapoton

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

comment:14 Changed 23 months ago by chapoton

  • 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 23 months ago by 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.

comment:16 Changed 23 months ago by 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 ?

comment:17 follow-up: Changed 23 months ago by 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?

comment:18 Changed 23 months ago by dimpase

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

comment:19 in reply to: ↑ 17 ; follow-up: Changed 23 months ago by 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.

comment:20 in reply to: ↑ 19 Changed 23 months ago by 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.

comment:21 Changed 23 months ago by 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)

comment:22 Changed 23 months ago by mjo

  • 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 22 months ago by tmonteil

  • Status changed from needs_review to positive_review

comment:24 Changed 22 months ago by vbraun

  • Branch changed from u/chapoton/27319 to d219646cd4dec96a1b4e53cce1f14aa9905377c3
  • Resolution set to fixed
  • Status changed from positive_review to closed
Note: See TracTickets for help on using tickets.