Opened 3 years ago
Closed 2 years ago
#26361 closed enhancement (fixed)
Glucose SAT solver
Reported by:  tmonteil  Owned by:  

Priority:  major  Milestone:  sage8.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, GitHub, GitLab)  Commit:  66d1983180e02a9be6da548524f9de397089dbce 
Dependencies:  Stopgaps: 
Description (last modified by )
This ticket adds a glucose experimental or optional package, and fixes the old glucose interface.
Tarball: http://www.labri.fr/perso/lsimon/downloads/softwares/glucosesyrup4.1.tgz
Change History (39)
comment:1 Changed 3 years ago by
comment:2 Changed 3 years ago by
 Branch set to u/tmonteil/glucose_sat_solver
comment:3 Changed 3 years ago by
 Commit set to 1159e0318dba6c3c3e667e6ecdc305b1eb6f98a6
Branch pushed to git repo; I updated commit sha1. New commits:
1159e03  #26361 : glucose depends on zlib

comment:4 Changed 3 years ago by
 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 3 years ago by
 Description modified (diff)
comment:6 Changed 3 years ago by
 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 glucosesyrup

comment:7 Changed 3 years ago by
 Status changed from new to needs_review
comment:8 Changed 3 years ago by
 Branch changed from u/tmonteil/glucose_sat_solver to u/slabbe/glucose_sat_solver
 Commit changed from 878769da0e26094712866eea15da5a4de91b043a to 887989a29439ab49328d4943c3a5324d5f6c3385
comment:9 Changed 3 years ago by
 Commit changed from 887989a29439ab49328d4943c3a5324d5f6c3385 to 41fa426773d934d8d141fe5748482f2300d562f6
Branch pushed to git repo; I updated commit sha1. This was a forced push. New commits:
41fa426  26361: adding optional tags

comment:10 Changed 3 years ago by
I removed the commit 887989a
from this ticket because glucosesyrup 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 3 years ago by
 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 3 years ago by
 Keywords thursdaysbdx added
Salut Thierry, estce 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 3 years ago by
 Status changed from needs_review to needs_info
Where is spkgcheck
?
comment:14 Changed 3 years ago by
 Status changed from needs_info to needs_work
In spkginstall
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 3 years ago by
And what is LFLAGS
!?
comment:16 Changed 3 years ago by
 Commit changed from 41fa426773d934d8d141fe5748482f2300d562f6 to a72792933d996513479d5bd5450ec266c9c38627
comment:17 Changed 3 years ago by
 Commit changed from a72792933d996513479d5bd5450ec266c9c38627 to e213768f6976a33869a474f5ef9f49c679b378b5
Branch pushed to git repo; I updated commit sha1. This was a forced push. New commits:
e213768  26361: simplification of spkginstall

comment:18 Changed 3 years ago by
Ok, I removed the SAGE_LOCAL
check part from the spkginstall
.
I keep the LFLAGS since the template makefile glucosesyrup4.1/mtl/template.mk
contains a line
LFLAGS ?= Wall lpthread
so I guess Thierry wrote that in the spkginstall
for some good reason.
What should be the content of the spkgcheck
? There does seem to be any check
target in the makefile of glucose...
comment:19 Changed 3 years ago by
 Status changed from needs_work to needs_review
comment:20 Changed 3 years ago by
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 3 years ago by
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 years ago by
 Commit changed from e213768f6976a33869a474f5ef9f49c679b378b5 to f8b52d8b68c365fd921e270d44a87ac0ec8904c8
Branch pushed to git repo; I updated commit sha1. New commits:
f8b52d8  26361: fixing description paragraph

comment:23 Changed 3 years ago by
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 years ago by
 Milestone changed from sage8.4 to sage8.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 years ago by
 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 glucosesyrup

2834b53  26361 adding doctests, adding glucose as an option to `SAT`

5ab84e2  26361: adding optional tags

52f09fc  26361: simplification of spkginstall

66d1983  26361: fixing description paragraph

19226b9  26361: define glucose as experimental instead of optional

comment:26 Changed 3 years ago by
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 years ago by
 Reviewers Sébastien Labbé deleted
I consider myself now more of a author for this ticket than a reviewer.
comment:28 Changed 3 years ago by
 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 years ago by
 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 years ago by
 Component changed from packages: optional to packages: experimental
 Milestone changed from sage8.5 to sage8.6
 Status changed from needs_review to positive_review
comment:31 Changed 3 years ago by
 Status changed from positive_review to needs_work
Reviewer name is missing...
comment:32 Changed 3 years ago by
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 followup: ↓ 34 Changed 3 years ago by
The reasons are explained above
 no tests provided
 tarball contains a lot of spurious files
comment:34 in reply to: ↑ 33 Changed 3 years ago by
Does are, imho, not good reasons.
Replying to vdelecroix:
The reasons are explained above
 no tests provided
The existence of spkgcheck
is conditioned to the existence of selftests, see https://doc.sagemath.org/html/en/developer/packaging.html#selftests. Many standard/optional packages do not provide self tests, and some selftests of standard packages are broken in various officially supported platforms (starting with python which is never selftested, see https://doc.sagemath.org/html/en/installation/source.html#index28). On Sage 8.4, only 82 over a total of 286 packages do have a spkgcheck
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 spkgsrc
with something like:
find name '._*' exec rm {} \;
See https://doc.sagemath.org/html/en/developer/packaging.html#modifiedtarballs 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 2 years ago by
 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 2 years ago by
 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 2 years ago by
 Component changed from packages: experimental to packages: optional
comment:38 Changed 2 years ago by
 Milestone changed from sage8.6 to sage8.7
 Status changed from needs_review to positive_review
comment:39 Changed 2 years ago by
 Branch changed from u/slabbe/glucose_sat_solver to 66d1983180e02a9be6da548524f9de397089dbce
 Resolution set to fixed
 Status changed from positive_review to closed
I did not notice that before packaging: the parallel version (which is the interesting one) uses a modified MIT license, and adds:
Shall we distribute that ? Shall we add a warning during the install procedure ?