Opened 2 years ago
Closed 2 years 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, 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/glucose-syrup-4.1.tgz
Change History (39)
comment:1 Changed 2 years ago by
comment:2 Changed 2 years ago by
- Branch set to u/tmonteil/glucose_sat_solver
comment:3 Changed 2 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 2 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 2 years ago by
- Description modified (diff)
comment:6 Changed 2 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 glucose-syrup
|
comment:7 Changed 2 years ago by
- Status changed from new to needs_review
comment:8 Changed 2 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 2 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 2 years ago by
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 2 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 2 years ago by
- 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 2 years ago by
- Status changed from needs_review to needs_info
Where is spkg-check
?
comment:14 Changed 2 years ago by
- 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 2 years ago by
And what is LFLAGS
!?
comment:16 Changed 2 years ago by
- Commit changed from 41fa426773d934d8d141fe5748482f2300d562f6 to a72792933d996513479d5bd5450ec266c9c38627
comment:17 Changed 2 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 spkg-install
|
comment:18 Changed 2 years ago by
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...
comment:19 Changed 2 years ago by
- Status changed from needs_work to needs_review
comment:20 Changed 2 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 2 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 2 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 2 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 2 years ago by
- 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 2 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 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
|
comment:26 Changed 2 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 2 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 2 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 2 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 2 years ago by
- 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 2 years ago by
- Status changed from positive_review to needs_work
Reviewer name is missing...
comment:32 Changed 2 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 follow-up: ↓ 34 Changed 2 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 2 years ago by
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 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 sage-8.6 to sage-8.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 ?