Glucose SAT solver

[tmonteil]

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

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

[git]

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

​1159e03

#26361 : glucose depends on zlib

[git]

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

​38d09eb

#26361 : fix glucose interface + doctests

[git]

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

​878769d

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

[slabbe]

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

---

New commits:

​19ac7ec	Merge branch 'u/tmonteil/glucose_sat_solver' into 8.5.beta0
​521f595	26361 adding doctests, adding glucose as an option to `SAT`
​887989a	26361: adding an interface to glucose-syrup

[git]

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

​41fa426

26361: adding optional tags

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

[slabbe]

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

[slabbe]

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.

[vdelecroix]

Where is spkg-check?

[vdelecroix]

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

[vdelecroix]

And what is LFLAGS!?

[git]

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

​bec05bb	Merge branch 'u/slabbe/glucose_sat_solver' into 8.5.beta4
​a727929	26361: simplification of spkg-install

[git]

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

​e213768

26361: simplification of spkg-install

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

[vdelecroix]

The copy paste in the description is not so nice.

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

[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

[git]

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

​f8b52d8

26361: fixing description paragraph

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

[vdelecroix]

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

[git]

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
​2834b53	26361 adding doctests, adding glucose as an option to `SAT`
​5ab84e2	26361: adding optional tags
​52f09fc	26361: simplification of spkg-install
​66d1983	26361: fixing description paragraph
​19226b9	26361: define glucose as experimental instead of optional

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

[slabbe]

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

[slabbe]

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

[slabbe]

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

[vbraun]

Reviewer name is missing...

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

[vdelecroix]

The reasons are explained above

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

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

[git]

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

[slabbe]

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.