Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

create an optional package for kissat SAT solver #34909

Closed
seblabbe opened this issue Jan 12, 2023 · 33 comments
Closed

create an optional package for kissat SAT solver #34909

seblabbe opened this issue Jan 12, 2023 · 33 comments
Labels
c: packages: optional p: major / 3 t: enhancement
Milestone
sage-9.8

Comments

@seblabbe
Copy link
Contributor

http://fmv.jku.at/kissat/

More precisely, version 3.0.0 available at https://github.com/arminbiere/kissat/archive/refs/tags/rel-3.0.0.tar.gz

Component: packages: optional

Author: Sébastien Labbé, Matthias Koeppe

Branch/Commit: c02693d

Reviewer: Matthias Koeppe, Sébastien Labbé

Issue created by migration from https://trac.sagemath.org/ticket/34909
@seblabbe seblabbe added this to the sage-9.8 milestone Jan 12, 2023
@seblabbe
Copy link
Contributor Author

comment:1

Initial version

New commits:

d52caacKISSAT 3.0.0: initial version for this optional package

@seblabbe
Copy link
Contributor Author

Commit: d52caac

@seblabbe
Copy link
Contributor Author

Branch: u/slabbe/34909

@sagetrac-git
Copy link
Mannequin

sagetrac-git mannequin commented Jan 12, 2023

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

852c151KISSAT 3.0.0: initial version for this optional package

@sagetrac-git
Copy link
Mannequin

sagetrac-git mannequin commented Jan 12, 2023

Changed commit from d52caac to 852c151

@sagetrac-git
Copy link
Mannequin

sagetrac-git mannequin commented Jan 12, 2023

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

bbb6d28KISSAT 3.0.0: initial version for this optional package

@sagetrac-git
Copy link
Mannequin

sagetrac-git mannequin commented Jan 12, 2023

Changed commit from 852c151 to bbb6d28

@seblabbe
Copy link
Contributor Author

comment:4

using helper function sdh_configure cause the following error:

[kissat-3.0.0] Configuring kissat-3.0.0
[kissat-3.0.0] configure: error: invalid option '--prefix=/home/slabbe/GitBox/sage/local' (try '-h')
[kissat-3.0.0] configure: error: invalid option '--prefix=/home/slabbe/GitBox/sage/local' (try '-h')
[kissat-3.0.0] *****************************************************************************************************
[kissat-3.0.0] Error configuring kissat-3.0.0
[kissat-3.0.0] *****************************************************************************************************

@sagetrac-git
Copy link
Mannequin

sagetrac-git mannequin commented Jan 12, 2023

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

665a48cusing ./configure instead of sdh_configure

@sagetrac-git
Copy link
Mannequin

sagetrac-git mannequin commented Jan 12, 2023

Changed commit from bbb6d28 to 665a48c

@sagetrac-git
Copy link
Mannequin

sagetrac-git mannequin commented Jan 12, 2023

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

bba0024using just a spkg-install.in with no spkg-build.in

@sagetrac-git
Copy link
Mannequin

sagetrac-git mannequin commented Jan 12, 2023

Changed commit from 665a48c to bba0024

@seblabbe
Copy link
Contributor Author

comment:7

With the current state, installation works:

Copying package files from temporary location /home/slabbe/GitBox/sage/local/var/tmp/sage/build/kissat-3.0.0/inst to /home/slabbe/GitBox/sage/local
Successfully installed kissat-3.0.0
Deleting temporary build directory
/home/slabbe/GitBox/sage/local/var/tmp/sage/build/kissat-3.0.0
Finished installing kissat-3.0.0

But, then I don't find the command:

 $ sage -sh
...
(sage-sh) slabbe@miami:sage$ kissat
bash: kissat : commande introuvable

@mkoeppe
Copy link
Contributor

mkoeppe commented Jan 13, 2023

comment:8

The upstream package has a hand-written configure script that does not understand the standard option --prefix, and the generated Makefile has no target make install.

@mkoeppe
Copy link
Contributor

mkoeppe commented Jan 13, 2023

Changed branch from u/slabbe/34909 to u/mkoeppe/34909

@mkoeppe
Copy link
Contributor

mkoeppe commented Jan 13, 2023

Author: Sébastien Labbé, Matthias Koeppe

@mkoeppe
Copy link
Contributor

mkoeppe commented Jan 13, 2023

Changed commit from bba0024 to cea9e49

@mkoeppe
Copy link
Contributor

mkoeppe commented Jan 13, 2023

New commits:

12a1839KISSAT 3.0.0: initial version for this optional package
279bd4dusing ./configure instead of sdh_configure
8262dcdusing just a spkg-install.in with no spkg-build.in
ae36201build/pkgs/kissat/SPKG.rst: Fix title format, remove empty section
cea9e49build/pkgs/kissat: Fix scripts

@sagetrac-git
Copy link
Mannequin

sagetrac-git mannequin commented Jan 13, 2023

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

a991372build/pkgs/kissat/distros: Add more

@sagetrac-git
Copy link
Mannequin

sagetrac-git mannequin commented Jan 13, 2023

Changed commit from cea9e49 to a991372

@mkoeppe
Copy link
Contributor

mkoeppe commented Jan 13, 2023

comment:12

builds, installs, and tests OK on macOS. Have not tried anything else.

@seblabbe
Copy link
Contributor Author

comment:13

Great! Thanks for fixing the scripts Matthias. I needed help for that. I will test that now, but I first need to update my sage version to the most recent one.

@seblabbe
Copy link
Contributor Author

comment:14

Did you manage to download the tarbal with the given upstream_url?
Because when we click on the link, it downloads a file named kissat-rel-3.0.0.tar.gz and wgetting it downloads rel-3.0.0.tar.gz. I think a file starting with kissat is better because rel I guess means release. Maybe we should just delete the upstream_url line?

@mkoeppe
Copy link
Contributor

mkoeppe commented Jan 13, 2023

comment:15

The checksums.ini already handles this correctly.
That's why both tarball and upstream_url are given.

@seblabbe
Copy link
Contributor Author

comment:16

Installation works, but during installation I notice the following line:

[kissat-3.0.0] mkdir: cannot create directory 'build': File exists

@seblabbe
Copy link
Contributor Author

Changed branch from u/mkoeppe/34909 to u/slabbe/34909

@seblabbe
Copy link
Contributor Author

Changed commit from a991372 to c02693d

@seblabbe
Copy link
Contributor Author

New commits:

c02693d34909: removed line 'mkdir build' in spkg-install

@seblabbe
Copy link
Contributor Author

Reviewer: Sébastien Labbé

@seblabbe
Copy link
Contributor Author

comment:18

The build directory seems to be constructed in the configure script, so I removed the mkdir build line from the spkg-install.

I give positive review to your changes. I let you change the status to positive review if you agree with my changes.

Everything done here seems to work well (see #34911).

@mkoeppe
Copy link
Contributor

mkoeppe commented Jan 13, 2023

Changed reviewer from Sébastien Labbé to Matthias Koeppe, Sébastien Labbé

@mkoeppe
Copy link
Contributor

mkoeppe commented Jan 13, 2023

comment:19

LGTM, thanks.

@vbraun
Copy link
Member

vbraun commented Jan 21, 2023

Changed branch from u/slabbe/34909 to c02693d

@vbraun vbraun closed this as completed in 0aa67a5 Jan 21, 2023
@seblabbe seblabbe mentioned this issue Jan 21, 2023
Closed
kryzar pushed a commit to kryzar/sage that referenced this issue Feb 6, 2023
Trac sagemath#34911: Adding class Kissat in sage/sat/solvers/dimacs.py
54bfa66 
We add a class Kissat in sage/sat/solvers/dimacs.py

We also use the opportunity to improve the dimacs.py file (uniformize
the classes so that they can inherit the same `__call__` method, added
documentation and new doctests).

This is a follow up of sagemath#34909.

URL: https://trac.sagemath.org/34911
Reported by: slabbe
Ticket author(s): Sébastien Labbé
Reviewer(s): Andrey Belgorodski
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
c: packages: optional p: major / 3 t: enhancement
Projects
None yet
Milestone
sage-9.8
Development

No branches or pull requests
3 participants
@vbraun @seblabbe @mkoeppe