Opened 6 months ago

Closed 2 months ago

#26361 closed enhancement (fixed)

Glucose SAT solver

Reported by: tmonteil Owned by:
Priority: major Milestone: sage-8.7
Component: packages: optional Keywords: thursdaysbdx
Cc: Merged in:
Authors: Thierry Monteil, Sébastien Labbé Reviewers: Vincent Delecroix
Report Upstream: N/A Work issues:
Branch: 66d1983 (Commits) Commit: 66d1983180e02a9be6da548524f9de397089dbce
Dependencies: Stopgaps:

Description (last modified by slabbe)

This ticket adds a glucose experimental or optional package, and fixes the old glucose interface.

Tarball: http://www.labri.fr/perso/lsimon/downloads/softwares/glucose-syrup-4.1.tgz

Change History (39)

comment:1 Changed 6 months ago by tmonteil

I did not notice that before packaging: the parallel version (which is the interesting one) uses a modified MIT license, and adds:

  • The parallel version of Glucose (all files modified since Glucose 3.0 releases, 2013) cannot be used in any competitive event (sat competitions/evaluations) without the express permission of the authors (Gilles Audemard / Laurent Simon). This is also the case for any competitive event using Glucose Parallel as an embedded SAT engine (single core or not).

Shall we distribute that ? Shall we add a warning during the install procedure ?

comment:2 Changed 6 months ago by tmonteil

  • Branch set to u/tmonteil/glucose_sat_solver

comment:3 Changed 6 months ago by git

  • Commit set to 1159e0318dba6c3c3e667e6ecdc305b1eb6f98a6

Branch pushed to git repo; I updated commit sha1. New commits:

1159e03#26361 : glucose depends on zlib

comment:4 Changed 6 months ago by git

  • Commit changed from 1159e0318dba6c3c3e667e6ecdc305b1eb6f98a6 to 38d09ebc35e5b1ee4a00e689c54af225144943ea

Branch pushed to git repo; I updated commit sha1. New commits:

38d09eb#26361 : fix glucose interface + doctests

comment:5 Changed 6 months ago by tmonteil

  • Description modified (diff)

comment:6 Changed 6 months ago by git

  • Commit changed from 38d09ebc35e5b1ee4a00e689c54af225144943ea to 878769da0e26094712866eea15da5a4de91b043a

Branch pushed to git repo; I updated commit sha1. New commits:

878769d#26361 : add a warning about the license of glucose-syrup

comment:7 Changed 6 months ago by tmonteil

  • Status changed from new to needs_review

comment:8 Changed 5 months ago by slabbe

  • Branch changed from u/tmonteil/glucose_sat_solver to u/slabbe/glucose_sat_solver
  • Commit changed from 878769da0e26094712866eea15da5a4de91b043a to 887989a29439ab49328d4943c3a5324d5f6c3385

Porting the modif I did in #26552 that were not here.


New commits:

19ac7ecMerge branch 'u/tmonteil/glucose_sat_solver' into 8.5.beta0
521f59526361 adding doctests, adding glucose as an option to `SAT`
887989a26361: adding an interface to glucose-syrup

comment:9 Changed 5 months ago by git

  • Commit changed from 887989a29439ab49328d4943c3a5324d5f6c3385 to 41fa426773d934d8d141fe5748482f2300d562f6

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

41fa42626361: adding optional tags

comment:10 Changed 5 months ago by slabbe

I removed the commit 887989a from this ticket because glucose-syrup does not work: it writes an empty output file. I will move that commit to my other ticket #26552 and I will update its goal.

comment:11 Changed 5 months ago by slabbe

  • Reviewers set to Sébastien Labbé

I give a positive review to your commits. Do you agree with my changes? If so, you may set this to positive review.

comment:12 Changed 5 months ago by slabbe

  • Keywords thursdaysbdx added

Salut Thierry, est-ce que mes commits te conviennent? Je vais faire du sage jeudi matin si tu veux que je change des choses dans mes commits.

comment:13 Changed 4 months ago by vdelecroix

  • Status changed from needs_review to needs_info

Where is spkg-check?

comment:14 Changed 4 months ago by vdelecroix

  • Status changed from needs_info to needs_work

In spkg-install the following is not needed

if [ "$SAGE_LOCAL" = "" ]; then
   echo "SAGE_LOCAL undefined ... exiting";
   echo "Maybe run 'sage -sh'?"
   exit 1
fi

comment:15 Changed 4 months ago by vdelecroix

And what is LFLAGS!?

comment:16 Changed 4 months ago by git

  • Commit changed from 41fa426773d934d8d141fe5748482f2300d562f6 to a72792933d996513479d5bd5450ec266c9c38627

Branch pushed to git repo; I updated commit sha1. New commits:

bec05bbMerge branch 'u/slabbe/glucose_sat_solver' into 8.5.beta4
a72792926361: simplification of spkg-install

comment:17 Changed 4 months ago by git

  • Commit changed from a72792933d996513479d5bd5450ec266c9c38627 to e213768f6976a33869a474f5ef9f49c679b378b5

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

e21376826361: simplification of spkg-install

comment:18 Changed 4 months ago by slabbe

Ok, I removed the SAGE_LOCAL check part from the spkg-install.

I keep the LFLAGS since the template makefile glucose-syrup-4.1/mtl/template.mk contains a line

LFLAGS    ?= -Wall -lpthread 

so I guess Thierry wrote that in the spkg-install for some good reason.

What should be the content of the spkg-check ? There does seem to be any check target in the makefile of glucose...

Last edited 4 months ago by slabbe (previous) (diff)

comment:19 Changed 4 months ago by slabbe

  • Status changed from needs_work to needs_review

comment:20 Changed 4 months ago by vdelecroix

The copy paste in the description is not so nice.

This page summarizes the techniques embedded in all the versions of
glucose. 

comment:21 Changed 4 months ago by vdelecroix

The tarball is full of junk (from mac OSX)

./utils/._System.h
./utils/._System.cc
./utils/._ParseUtils.h
./utils/._Options.h
./utils/._Options.cc
./utils/._Makefile
./._utils
./simp/._SimpSolver.h
./simp/._SimpSolver.cc
./simp/._Makefile
./simp/._Main.cc
./._simp
./._README
./parallel/._SolverConfiguration.h
./parallel/._SolverConfiguration.cc
./parallel/._SolverCompanion.h
./parallel/._SolverCompanion.cc
./parallel/._SharedCompanion.h
./parallel/._SharedCompanion.cc
./parallel/._ParallelSolver.h
./parallel/._ParallelSolver.cc
./parallel/._MultiSolvers.h
./parallel/._MultiSolvers.cc
./parallel/._Makefile
./parallel/._Main.cc
./parallel/._ClausesBuffer.h
./parallel/._ClausesBuffer.cc
./._parallel
./mtl/._XAlloc.h
./mtl/._VecThreads.h
./mtl/._Vec.h
./mtl/._template.mk
./mtl/._Sort.h
./mtl/._Queue.h
./mtl/._Map.h
./mtl/._IntTypes.h
./mtl/._Heap.h
./mtl/._config.mk
./mtl/._Clone.h
./mtl/._Alloc.h
./mtl/._Alg.h
./._mtl
./._LICENCE
./core/._SolverTypes.h
./core/._SolverStats.h
./core/._Solver.h
./core/._Solver.cc
./core/._Makefile
./core/._Dimacs.h
./core/._Constants.h
./core/._BoundedQueue.h
./._core
./._Changelog

comment:22 Changed 3 months ago by git

  • Commit changed from e213768f6976a33869a474f5ef9f49c679b378b5 to f8b52d8b68c365fd921e270d44a87ac0ec8904c8

Branch pushed to git repo; I updated commit sha1. New commits:

f8b52d826361: fixing description paragraph

comment:23 Changed 3 months ago by slabbe

I fixed the description.

I asked Laurent to redo a new tarball with no junk files. I do not know how long it will take. Vincent: do you want to wait for the new tarball or are you okay with some junk files for now? This issue of junk files shall be fixed in a later version of glucose.

For now, the goal of this ticket is to make version 4.1 of glucose an optional package of sage. Later versions of glucose will be dealt in another ticket.

Needs review!

comment:24 Changed 3 months ago by vdelecroix

  • Milestone changed from sage-8.4 to sage-8.5

glucose is really terrible in terms of packaging. For the time being I would rather propose to make it an experimental package.

comment:25 Changed 3 months ago by git

  • Commit changed from f8b52d8b68c365fd921e270d44a87ac0ec8904c8 to 19226b98a599e878ea27411750ccafd57f072ec0

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

8449a95#26361: package glucose SAT solver
cf69c54#26361 : glucose depends on zlib
da88cbc#26361 : fix glucose interface + doctests
de2c83e#26361 : add a warning about the license of glucose-syrup
2834b5326361 adding doctests, adding glucose as an option to `SAT`
5ab84e226361: adding optional tags
52f09fc26361: simplification of spkg-install
66d198326361: fixing description paragraph
19226b926361: define glucose as experimental instead of optional

comment:26 Changed 3 months ago by slabbe

Fine for me. I changed it to experimental.

I also rebased the branch on top of 8.5.rc0 to avoid 3 merge commits inside a single ticket.

Needs review!

comment:27 Changed 3 months ago by slabbe

  • Authors changed from Thierry Monteil to Thierry Monteil, Sébastien Labbé
  • Reviewers Sébastien Labbé deleted

I consider myself now more of a author for this ticket than a reviewer.

comment:28 Changed 3 months ago by slabbe

  • Status changed from needs_review to needs_info

Laurent might provide me with a new tarbal with no junk file by tomorrow... So I put the review on hold for now.

comment:29 Changed 3 months ago by slabbe

  • Description modified (diff)
  • Status changed from needs_info to needs_review

No tarball received by today. Let's move forward with an experimental package for now.

comment:30 Changed 3 months ago by vdelecroix

  • Component changed from packages: optional to packages: experimental
  • Milestone changed from sage-8.5 to sage-8.6
  • Status changed from needs_review to positive_review

comment:31 Changed 3 months ago by vbraun

  • Status changed from positive_review to needs_work

Reviewer name is missing...

comment:32 Changed 3 months ago by tmonteil

Sorry for not being active during the past month. I really do not understand why the package has to be experimental. Does someone have problem to compile it ? Does someone experience wrong results with it ? Note that having a package set to experimental makes it less tested (one have to manualy add it to the --optional test option).

comment:33 follow-up: Changed 3 months ago by vdelecroix

The reasons are explained above

  • no tests provided
  • tarball contains a lot of spurious files

comment:34 in reply to: ↑ 33 Changed 3 months ago by tmonteil

Does are, imho, not good reasons.

Replying to vdelecroix:

The reasons are explained above

  • no tests provided

The existence of spkg-check is conditioned to the existence of self-tests, see https://doc.sagemath.org/html/en/developer/packaging.html#self-tests. Many standard/optional packages do not provide self tests, and some self-tests of standard packages are broken in various officially supported platforms (starting with python which is never self-tested, see https://doc.sagemath.org/html/en/installation/source.html#index-28). On Sage 8.4, only 82 over a total of 286 packages do have a spkg-check file.

Note that, setting a package type to experimental implies that classical sage tests tagged with that package are not run with a usual sage --test --all --long command, the package must be explicitly added by hand (and then only the explicitly added packages will be tested). This implies that actually, the package behaviour in sage will be even less tested than if it was optional.

  • tarball contains a lot of spurious files

This is an aesthetical judgment. They do not interfere with the compilation. Note that even with those files, the tarball size is pretty small.

If this was a real concern (it is not), the appropriate fix would have been to provide a spkg-src with something like:

find -name '._*' -exec rm {} \;

See https://doc.sagemath.org/html/en/developer/packaging.html#modified-tarballs note that i am not in favor of this option either as is breaks upstream integrity (everyone can check that the hashes correspond) for no real benefit.

comment:35 Changed 3 months ago by git

  • Commit changed from 19226b98a599e878ea27411750ccafd57f072ec0 to 66d1983180e02a9be6da548524f9de397089dbce

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

comment:36 Changed 3 months ago by slabbe

  • Reviewers set to Vincent Delecroix
  • Status changed from needs_work to needs_review

Personally, I agree to set it to optional.

I just forced pushed the penultimate commit ​66d1983.

I added the name of Vincent in the reviewer field since he was involved in the review up to now and to avoid forgeting it a second time.

Needs review.

comment:37 Changed 3 months ago by slabbe

  • Component changed from packages: experimental to packages: optional

comment:38 Changed 3 months ago by vdelecroix

  • Milestone changed from sage-8.6 to sage-8.7
  • Status changed from needs_review to positive_review

comment:39 Changed 2 months ago by vbraun

  • Branch changed from u/slabbe/glucose_sat_solver to 66d1983180e02a9be6da548524f9de397089dbce
  • Resolution set to fixed
  • Status changed from positive_review to closed
Note: See TracTickets for help on using tickets.