Package: guix-patches;
Reported by: Liliana Marie Prikler <liliana.prikler <at> gmail.com>
Date: Sun, 29 Sep 2024 09:19:30 UTC
Severity: normal
Tags: patch
Done: Liliana Marie Prikler <liliana.prikler <at> gmail.com>
Bug is archived. No further changes may be made.
To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 73551 in the body.
You can then email your comments to 73551 AT debbugs.gnu.org in the normal way.
Toggle the display of automated, internal messages from the tracker.
View this report as an mbox folder, status mbox, maintainer mbox
guix-patches <at> gnu.org:bug#73551; Package guix-patches.
(Sun, 29 Sep 2024 09:19:38 GMT) Full text and rfc822 format available.Liliana Marie Prikler <liliana.prikler <at> gmail.com>:guix-patches <at> gnu.org.
(Sun, 29 Sep 2024 09:19:41 GMT) Full text and rfc822 format available.Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: guix-patches <at> gnu.org Subject: [PATCH 0/8] Update some SAT/ASP solvers Date: Sun, 29 Sep 2024 11:16:38 +0200
Hi Guix, I noticed that scasp and some other tools where out of date, so I decided to update them. Cheers Liliana Marie Prikler (8): gnu: scasp: Update to 1.1.4. gnu: kissat: Update to 4.0.1. gnu: z3: Update to 4.13.0. gnu: lingeling: Update to 1.0.0. gnu: Add cadical. gnu: Add cadiback. gnu: Add cadiback-for-cryptominisat. gnu: cryptominisat: Update to 5.11.22. gnu/local.mk | 1 + gnu/packages/maths.scm | 362 ++++++++++++------ .../patches/cadical-add-shared-library.patch | 49 +++ 3 files changed, 305 insertions(+), 107 deletions(-) create mode 100644 gnu/packages/patches/cadical-add-shared-library.patch base-commit: 93ceb2d90165fa5e76f983f252f09bf97f3b17d8 -- 2.46.0
guix-patches <at> gnu.org:bug#73551; Package guix-patches.
(Sun, 29 Sep 2024 09:35:01 GMT) Full text and rfc822 format available.Message #8 received at 73551 <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: 73551 <at> debbugs.gnu.org Subject: [PATCH 5/8] gnu: Add cadical. Date: Sun, 29 Sep 2024 11:00:56 +0200
* gnu/packages/patches/cadical-add-shared-library.patch: New file.
* gnu/local.mk (dist_patch_DATA): Register it here.
* gnu/packages/maths.scm (cadical): New variable.
---
gnu/local.mk | 1 +
gnu/packages/maths.scm | 52 +++++++++++++++++++
.../patches/cadical-add-shared-library.patch | 49 +++++++++++++++++
3 files changed, 102 insertions(+)
create mode 100644 gnu/packages/patches/cadical-add-shared-library.patch
diff --git a/gnu/local.mk b/gnu/local.mk
index 49660d4b3e..3d39016609 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -1027,6 +1027,7 @@ dist_patch_DATA = \
%D%/packages/patches/breezy-fix-gio.patch \
%D%/packages/patches/byobu-writable-status.patch \
%D%/packages/patches/bubblewrap-fix-locale-in-tests.patch \
+ %D%/packages/patches/cadical-add-shared-library.patch \
%D%/packages/patches/calibre-no-updates-dialog.patch \
%D%/packages/patches/calibre-remove-test-sqlite.patch \
%D%/packages/patches/calibre-remove-test-unrar.patch \
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index ab989e6af6..23015bc86a 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9290,6 +9290,58 @@ (define-public lingeling
also included.")
(license license:expat)))
+(define-public cadical
+ (package
+ (name "cadical")
+ (version "2.0.0")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/arminbiere/cadical")
+ (commit (string-append "rel-" version))))
+ (file-name (git-file-name name version))
+ (patches (search-patches "cadical-add-shared-library.patch"))
+ (sha256
+ (base32 "1dzjah3z34v89ka48hncwqkxrwl4xqn9947p0ipf39lxshrq91xa"))))
+ (build-system gnu-build-system)
+ (arguments
+ (list #:test-target "test"
+ #:modules `(((guix build copy-build-system) #:prefix copy:)
+ (guix build gnu-build-system)
+ (guix build utils)
+ (ice-9 regex))
+ #:imported-modules %copy-build-system-modules
+ #:phases
+ #~(modify-phases %standard-phases
+ (replace 'configure
+ (lambda* (#:key configure-flags #:allow-other-keys)
+ (setenv "CXXFLAGS" "-DPIC -fPIC")
+ (apply invoke "./configure" configure-flags)))
+ (replace 'check
+ (lambda args
+ ;; Tests are incorrectly linked upstream.
+ ;; Since we don't install them, just work around this in the
+ ;; check phase.
+ (setenv "LD_LIBRARY_PATH" (string-append (getcwd) "/build"))
+ (apply (assoc-ref %standard-phases 'check) args)
+ (unsetenv "LD_LIBRARY_PATH")))
+ (replace 'install
+ (lambda args
+ (apply
+ (assoc-ref copy:%standard-phases 'install)
+ #:install-plan
+ `(("build" "bin" #:include ("cadical" "mobical"))
+ ("build" "lib" #:include-regexp ("libcadical\\.(a|so)$"))
+ ("src" "include" #:include ("cadical.h"))
+ ;; Internal headers used by cadiback.
+ ("src" "include/cadical" #:include-regexp ("\\.hpp$")))
+ args))))))
+ (home-page "https://github.com/arminbiere/cadical")
+ (synopsis "SAT solver")
+ (description "This package provides a SAT solver based on conflict-driven
+clause learning.")
+ (license license:expat)))
+
(define-public louvain-community
(let ((commit "8cc5382d4844af127b1c1257373740d7e6b76f1e")
(revision "1"))
diff --git a/gnu/packages/patches/cadical-add-shared-library.patch b/gnu/packages/patches/cadical-add-shared-library.patch
new file mode 100644
index 0000000000..a1ae786d13
--- /dev/null
+++ b/gnu/packages/patches/cadical-add-shared-library.patch
@@ -0,0 +1,49 @@
+From fcb865786b524917aa9d3df8745aca66716794bf Mon Sep 17 00:00:00 2001
+From: Mate Soos <soos.mate <at> gmail.com>
+Date: Sun, 2 Jun 2024 21:50:06 -0400
+Subject: [PATCH] Also add a dynamic library
+
+---
+Liliana Marie Prikler <liliana.prikler <at> gmail.com>:
+ Added -L.
+ Squashed fix for cadical and mobical.
+
+ makefile.in | 5 ++++-
+ 1 file changed, 4 insertions(+), 1 deletion(-)
+
+diff --git a/makefile.in b/makefile.in
+index 291cb3e3..d179f591 100644
+--- a/makefile.in
++++ b/makefile.in
+@@ -34,7 +34,7 @@ COMPILE=$(CXX) $(CXXFLAGS) -I$(DIR) -I$(ROOT)/src
+
+ #--------------------------------------------------------------------------#
+
+-all: libcadical.a cadical mobical
++all: libcadical.so libcadical.a cadical mobical
+
+ #--------------------------------------------------------------------------#
+
+@@ -54,10 +54,10 @@ contrib/%.o: $(ROOT)/contrib/%.cpp $(ROOT)/contrib/%.hpp $(ROOT)/src/*.hpp makef
+ # tester 'mobical') and the library are the main build targets.
+
+ cadical: src/cadical.o libcadical.a makefile
+- $(COMPILE) -o $@ $< -L. -lcadical $(LIBS)
++ $(COMPILE) -static -o $@ $< -L. -lcadical $(LIBS)
+
+ mobical: src/mobical.o libcadical.a makefile $(LIBS)
+- $(COMPILE) -o $@ $< -L. -lcadical
++ $(COMPILE) -static -o $@ $< -L. -lcadical
+
+ libcadical.a: $(OBJ_SOLVER) $(OBJ_CONTRIB) makefile
+ ar rc $@ $(OBJ_SOLVER) $(OBJ_CONTRIB)
+@@ -62,5 +62,8 @@ mobical: src/mobical.o libcadical.a makefile $(LIBS)
+ libcadical.a: $(OBJ_SOLVER) $(OBJ_CONTRIB) makefile
+ ar rc $@ $(OBJ_SOLVER) $(OBJ_CONTRIB)
+
++libcadical.so: $(OBJ_SOLVER) $(OBJ_CONTRIB) $(LIBS) makefile
++ $(COMPILE) -shared -o $@ $(OBJ_SOLVER) $(OBJ_CONTRIB) $(LIBS)
++
+ #--------------------------------------------------------------------------#
+
+ # Note that 'build.hpp' is generated and resides in the build directory.
\ No newline at end of file
--
2.46.0
guix-patches <at> gnu.org:bug#73551; Package guix-patches.
(Sun, 29 Sep 2024 09:36:02 GMT) Full text and rfc822 format available.Message #11 received at 73551 <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: 73551 <at> debbugs.gnu.org Subject: [PATCH 8/8] gnu: cryptominisat: Update to 5.11.22. Date: Sun, 29 Sep 2024 11:08:20 +0200
* gnu/packages/maths.scm (cryptominisat): Update to 5.11.22.
[source]: Patch include for cadiback.
[inputs]: Add cadical, cadiback-for-cryptominisat and gmp.
---
gnu/packages/maths.scm | 19 ++++++++++++++++---
1 file changed, 16 insertions(+), 3 deletions(-)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index e84a87db97..e809c62e18 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9463,7 +9463,7 @@ (define-public louvain-community
(define-public cryptominisat
(package
(name "cryptominisat")
- (version "5.11.4")
+ (version "5.11.22")
(source
(origin
(method git-fetch)
@@ -9473,7 +9473,12 @@ (define-public cryptominisat
(file-name (git-file-name name version))
(sha256
(base32
- "1izjn44phjp9670s7bxrdx4p0r59idqwv3bm6sr0qnlqlha5z4zc"))))
+ "1c85gfqvy90yhh9jwmiiz2bz4i86prgpfyx1gbzl42hn2ixkcjgm"))
+ (modules '((guix build utils)))
+ (snippet
+ #~(begin
+ (substitute* "src/backbone.cpp"
+ (("\"\\.\\./cadiback/cadiback\\.h\"") "<cadiback.h>"))))))
(build-system cmake-build-system)
(arguments
(list
@@ -9497,7 +9502,15 @@ (define-public cryptominisat
"find_package(GTest REQUIRED)")
(("add_subdirectory\\(\\$\\{PROJECT_SOURCE_DIR\\}/utils/.*\\)")
"")))))))
- (inputs (list boost louvain-community python python-numpy sqlite zlib))
+ (inputs (list boost
+ cadical
+ cadiback-for-cryptominisat
+ gmp
+ louvain-community
+ python
+ python-numpy
+ sqlite
+ zlib))
(native-inputs (list googletest lingeling python python-wrapper python-lit))
(synopsis "Incremental SAT solver")
(description
--
2.46.0
guix-patches <at> gnu.org:bug#73551; Package guix-patches.
(Sun, 29 Sep 2024 09:37:02 GMT) Full text and rfc822 format available.Message #14 received at 73551 <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: 73551 <at> debbugs.gnu.org Subject: [PATCH 7/8] gnu: Add cadiback-for-cryptominisat. Date: Sun, 29 Sep 2024 11:04:20 +0200
* gnu/packages/maths.scm (cadiback-for-cryptominisat): New variable.
---
gnu/packages/maths.scm | 29 +++++++++++++++++++++++++++++
1 file changed, 29 insertions(+)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index a8ae1c73a0..e84a87db97 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9400,6 +9400,35 @@ (define-public cadiback
true in all models.")
(license license:expat))))
+(define cadiback-for-cryptominisat
+ (let ((commit "ea65a9442fc2604ee5f4ffd0f0fdd0bf481d5b42")
+ (revision "1"))
+ (package
+ (inherit cadiback)
+ (name "cadiback-for-cryptominisat")
+ (version (git-version "0.2.1" revision commit))
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/meelgroup/cadiback")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "1zznrlj4zp1mc7s4pfw11aq773q2lr9yl6pph630zg5mqijaim5g"))))
+ (arguments
+ (substitute-keyword-arguments (package-arguments cadiback)
+ ((#:phases phases)
+ #~(modify-phases #$phases
+ (add-after 'patch-build-files 'fix-prefix
+ (lambda _
+ (substitute* "makefile.in"
+ (("/usr") #$output))))
+ (replace 'install
+ (lambda args
+ (mkdir-p (string-append #$output "/include"))
+ (mkdir-p (string-append #$output "/lib"))
+ (apply (assoc-ref %standard-phases 'install) args))))))))))
+
(define-public louvain-community
(let ((commit "8cc5382d4844af127b1c1257373740d7e6b76f1e")
(revision "1"))
--
2.46.0
guix-patches <at> gnu.org:bug#73551; Package guix-patches.
(Sun, 29 Sep 2024 09:38:02 GMT) Full text and rfc822 format available.Message #17 received at 73551 <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: 73551 <at> debbugs.gnu.org Subject: [PATCH 6/8] gnu: Add cadiback. Date: Sun, 29 Sep 2024 11:04:12 +0200
* gnu/packages/maths.scm (cadiback): New variable.
---
gnu/packages/maths.scm | 58 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 58 insertions(+)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 23015bc86a..a8ae1c73a0 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9342,6 +9342,64 @@ (define-public cadical
clause learning.")
(license license:expat)))
+(define-public cadiback
+ (let ((commit "789329d8fcda851085ed72f1b07d8c3f46243b8a")
+ (revision "1"))
+ (package
+ (name "cadiback")
+ ;; Note: version taken from VERSION file
+ (version (git-version "0.2.1" revision commit))
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/arminbiere/cadiback")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "137jxf9g7c1979pcgcqgfff1mqk5hs41a84780px8gpcrh469cks"))))
+ (build-system gnu-build-system)
+ (arguments
+ (list #:test-target "test"
+ #:modules `(((guix build copy-build-system) #:prefix copy:)
+ (guix build gnu-build-system)
+ (guix build utils)
+ (ice-9 regex))
+ #:imported-modules %copy-build-system-modules
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'unpack 'patch-build-files
+ (lambda* (#:key inputs #:allow-other-keys)
+ (substitute* "configure"
+ (("\\$CADICAL/src") "$CADICAL/include/cadical")
+ (("\\$CADICAL/build") "$CADICAL/lib"))
+ (substitute* "generate"
+ (("\\[ -d .git \\]" all) (string-append ": " all))
+ (("GITID=.*") (string-append "GITID=\"" #$commit "\"")))
+ (substitute* "makefile.in"
+ (("\\.\\./cadical/build")
+ (dirname
+ (search-input-file inputs "lib/libcadical.a")))
+ (("\\.\\./cadical/src")
+ (search-input-directory inputs "include/cadical")))))
+ (replace 'configure
+ (lambda* (#:key configure-flags #:allow-other-keys)
+ (setenv "CADICAL" #$(this-package-input "cadical"))
+ (apply invoke "./configure" configure-flags)))
+ (replace 'install
+ (lambda args
+ (apply
+ (assoc-ref copy:%standard-phases 'install)
+ #:install-plan
+ `(("." "bin" #:include ("cadiback")))
+ args))))))
+ (inputs (list cadical))
+ (home-page "https://github.com/arminbiere/cadiback")
+ (synopsis "Backbone extractor for cadical")
+ (description "This package provides a tool to determine the backbone of
+a satisfiable formula. The backbone is the set of literals that are set to
+true in all models.")
+ (license license:expat))))
+
(define-public louvain-community
(let ((commit "8cc5382d4844af127b1c1257373740d7e6b76f1e")
(revision "1"))
--
2.46.0
guix-patches <at> gnu.org:bug#73551; Package guix-patches.
(Sun, 29 Sep 2024 09:41:02 GMT) Full text and rfc822 format available.Message #20 received at 73551 <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: 73551 <at> debbugs.gnu.org Subject: [PATCH 2/8] gnu: kissat: Update to 4.0.1. Date: Wed, 25 Sep 2024 21:03:25 +0200
* gnu/packages/maths.scm (kissat): Update to 4.0.1.
[#:phases]<patch-source>: Relax regexp to fix test.
---
gnu/packages/maths.scm | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 581608d94d..6163148366 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9023,7 +9023,7 @@ (define-public minisat
(define-public kissat
(package
(name "kissat")
- (version "3.0.0")
+ (version "4.0.1")
(source
(origin
(method git-fetch)
@@ -9033,7 +9033,7 @@ (define-public kissat
(file-name (git-file-name name version))
(sha256
(base32
- "04x4w760srbdi4zci0s747qxk717x5d2x59ixraxh5104s9nyn8b"))))
+ "0acg61cfcjg13if2i375cyl4xvwmabhfhi9z8pnw971046am6bzv"))))
(build-system gnu-build-system)
(inputs (list xz gzip lzip bzip2 p7zip))
(arguments
@@ -9058,7 +9058,7 @@ (define-public kissat
"bool found = true;"))
(substitute* "test/testmain.c"
;; SIGINT is ignored inside invoke.
- (("^SIGNAL\\(SIGINT\\)") ""))))
+ (("^[ \t]*SIGNAL[ \t]*\\(SIGINT\\)") ""))))
(replace 'configure
(lambda* (#:key configure-flags #:allow-other-keys)
;; The configure script does not support standard GNU options.
--
2.46.0
guix-patches <at> gnu.org:bug#73551; Package guix-patches.
(Sun, 29 Sep 2024 09:41:02 GMT) Full text and rfc822 format available.Message #23 received at 73551 <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: 73551 <at> debbugs.gnu.org Subject: [PATCH 1/8] gnu: scasp: Update to 1.1.4. Date: Wed, 25 Sep 2024 21:03:03 +0200
* gnu/packages/maths.scm (scasp): Update to 1.1.4.
---
gnu/packages/maths.scm | 62 ++++++++++++++++++++----------------------
1 file changed, 30 insertions(+), 32 deletions(-)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 5f47d5e390..581608d94d 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -2912,39 +2912,37 @@ (define-public libflame
(license license:bsd-3))))
(define-public scasp
- (let ((commit "89a427aa04ec6346425a40111c99b310901ffe51")
- (revision "1"))
- (package
- (name "scasp")
- (version (git-version "0.21.11.26" revision commit))
- (source (origin
- (method git-fetch)
- (uri (git-reference
- (url "https://github.com/SWI-Prolog/sCASP")
- (commit commit)))
- (file-name (git-file-name name version))
- (sha256
- (base32
- "1ijqv9xr3imrdmz6nq7zqwsmmaxn638icig19m8900m7mjfpizs4"))))
- (build-system copy-build-system)
- (arguments
- (list
- #:install-plan #~`(("scasp" "bin/")
- ("prolog" "lib/swipl/library"))
- #:modules `((guix build copy-build-system)
- ((guix build gnu-build-system) #:prefix gnu:)
- (guix build utils)
- (ice-9 regex))
- #:phases
- #~(modify-phases %standard-phases
- (add-before 'install 'build (assoc-ref gnu:%standard-phases 'build))
- (add-after 'build 'check (assoc-ref gnu:%standard-phases 'check)))))
- (native-inputs (list swi-prolog))
- (home-page "https://github.com/SWI-Prolog/sCASP")
- (synopsis "Interpreter for ASP programs with constraints")
- (description "@code{s(CASP)} is a top-down interpreter for ASP programs
+ (package
+ (name "scasp")
+ (version "1.1.4")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/SWI-Prolog/sCASP")
+ (commit (string-append "V" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "1m4fs1ywich9cwj55miqp5zxs7c1fw9wvy7lcj5rkrgcanks5qk4"))))
+ (build-system copy-build-system)
+ (arguments
+ (list
+ #:install-plan #~`(("scasp" "bin/")
+ ("prolog" "lib/swipl/library"))
+ #:modules `((guix build copy-build-system)
+ ((guix build gnu-build-system) #:prefix gnu:)
+ (guix build utils)
+ (ice-9 regex))
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-before 'install 'build (assoc-ref gnu:%standard-phases 'build))
+ (add-after 'build 'check (assoc-ref gnu:%standard-phases 'check)))))
+ (native-inputs (list swi-prolog))
+ (home-page "https://github.com/SWI-Prolog/sCASP")
+ (synopsis "Interpreter for ASP programs with constraints")
+ (description "@code{s(CASP)} is a top-down interpreter for ASP programs
with constraints.")
- (license license:asl2.0))))
+ (license license:asl2.0)))
(define-public ceres
(package
--
2.46.0
guix-patches <at> gnu.org:bug#73551; Package guix-patches.
(Sun, 29 Sep 2024 09:41:03 GMT) Full text and rfc822 format available.Message #26 received at 73551 <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: 73551 <at> debbugs.gnu.org Subject: [PATCH 3/8] gnu: z3: Update to 4.13.0. Date: Wed, 25 Sep 2024 21:55:10 +0200
* gnu/packages/maths.scm (z3): Update to 4.13.0.
---
gnu/packages/maths.scm | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 6163148366..b6dae2a721 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -7666,7 +7666,7 @@ (define-public yices
(define-public z3
(package
(name "z3")
- (version "4.8.17")
+ (version "4.13.0")
(home-page "https://github.com/Z3Prover/z3")
(source (origin
(method git-fetch)
@@ -7675,7 +7675,7 @@ (define-public z3
(file-name (git-file-name name version))
(sha256
(base32
- "1vvb09q7w7zd29qc4qjysrrhyylszm1wf6azkff004ixwn026b05"))))
+ "0j46lckf3zgx2xjay7z6nvlgh47gisbbl4s3m5zn280a13fwz1ih"))))
(build-system cmake-build-system)
(arguments
(list
--
2.46.0
guix-patches <at> gnu.org:bug#73551; Package guix-patches.
(Sun, 29 Sep 2024 09:41:04 GMT) Full text and rfc822 format available.Message #29 received at 73551 <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: 73551 <at> debbugs.gnu.org Subject: [PATCH 4/8] gnu: lingeling: Update to 1.0.0. Date: Wed, 25 Sep 2024 22:02:49 +0200
* gnu/packages/maths.scm (lingeling): Update to 1.0.0.
[#:phases]<hard-code-commit>: Adjust accordingly.
---
gnu/packages/maths.scm | 132 ++++++++++++++++++++---------------------
1 file changed, 65 insertions(+), 67 deletions(-)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index b6dae2a721..ab989e6af6 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9211,86 +9211,84 @@ (define-public libpoly
(license license:lgpl3+)))
(define-public lingeling
- (let ((commit "72d2b13eea5fbd95557a3d0d199cd98dfbdc76ee")
- (revision "1"))
- (package
- (name "lingeling")
- (version (git-version "sc2022" revision commit))
- (source (origin
+ (package
+ (name "lingeling")
+ (version "1.0.0")
+ (source (origin
(method git-fetch)
(uri (git-reference
(url "https://github.com/arminbiere/lingeling")
- (commit commit)))
+ (commit (string-append "rel-" version))))
(file-name (git-file-name name version))
(sha256
(base32
- "16s30x8s2cw6icchwm65zj56ph4qwz6i07g3hwkknvajisvjq85c"))))
- (build-system gnu-build-system)
- (arguments
- (list #:test-target "test"
- #:modules `((ice-9 match)
- ,@%default-gnu-modules)
- #:configure-flags #~(list "--aiger=.")
- #:phases
- #~(modify-phases %standard-phases
- (add-after 'unpack 'unpack-aiger
- (lambda* (#:key inputs #:allow-other-keys)
- (invoke #$(ar-for-target) "x"
- (search-input-file inputs "lib/libaiger.a")
- "aiger.o")
- (copy-file
- (search-input-file inputs "include/aiger/aiger.h")
- "aiger.h")))
- (add-after 'unpack 'hard-code-commit
- (lambda _
- (substitute* "mkconfig.sh"
- (("`\\./getgitid`") #$commit))))
- (add-after 'unpack 'patch-source
- (lambda* (#:key inputs #:allow-other-keys)
- (substitute* (list "treengeling.c" "lgldimacs.c")
- (("\"(gunzip|xz|bzcat|7z)" all cmd)
- (string-append
- "\""
- (search-input-file inputs (string-append "bin/" cmd)))))))
- (replace 'configure
- (lambda* (#:key configure-flags #:allow-other-keys)
- (apply invoke "./configure.sh" configure-flags)))
- (replace 'install
- (lambda* (#:key outputs #:allow-other-keys)
- (let ((bin (string-append (assoc-ref outputs "out")
- "/bin")))
- (mkdir-p bin)
- (for-each
- (lambda (file)
- (install-file file bin))
- '("blimc" "ilingeling" "lglddtrace" "lglmbt"
- "lgluntrace" "lingeling" "plingeling"
- "treengeling")))))
- (add-after 'install 'wrap-path
- (lambda* (#:key outputs #:allow-other-keys)
- (with-directory-excursion (string-append
- (assoc-ref outputs "out")
- "/bin")
- (for-each
- (lambda (file)
- (wrap-program
- file
+ "0hszkhyni7jcw580f41rrrnwz42x56sqvd8zpcjdagvdiag76lc1"))))
+ (build-system gnu-build-system)
+ (arguments
+ (list #:test-target "test"
+ #:modules `((ice-9 match)
+ ,@%default-gnu-modules)
+ #:configure-flags #~(list "--aiger=.")
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'unpack 'unpack-aiger
+ (lambda* (#:key inputs #:allow-other-keys)
+ (invoke #$(ar-for-target) "x"
+ (search-input-file inputs "lib/libaiger.a")
+ "aiger.o")
+ (copy-file
+ (search-input-file inputs "include/aiger/aiger.h")
+ "aiger.h")))
+ (add-after 'unpack 'hard-code-commit
+ (lambda _
+ (substitute* "mkconfig.sh"
+ (("`\\./getgitid`") ""))))
+ (add-after 'unpack 'patch-source
+ (lambda* (#:key inputs #:allow-other-keys)
+ (substitute* (list "treengeling.c" "lgldimacs.c")
+ (("\"(gunzip|xz|bzcat|7z)" all cmd)
+ (string-append
+ "\""
+ (search-input-file inputs (string-append "bin/" cmd)))))))
+ (replace 'configure
+ (lambda* (#:key configure-flags #:allow-other-keys)
+ (apply invoke "./configure.sh" configure-flags)))
+ (replace 'install
+ (lambda* (#:key outputs #:allow-other-keys)
+ (let ((bin (string-append (assoc-ref outputs "out")
+ "/bin")))
+ (mkdir-p bin)
+ (for-each
+ (lambda (file)
+ (install-file file bin))
+ '("blimc" "ilingeling" "lglddtrace" "lglmbt"
+ "lgluntrace" "lingeling" "plingeling"
+ "treengeling")))))
+ (add-after 'install 'wrap-path
+ (lambda* (#:key outputs #:allow-other-keys)
+ (with-directory-excursion (string-append
+ (assoc-ref outputs "out")
+ "/bin")
+ (for-each
+ (lambda (file)
+ (wrap-program
+ file
'("PATH" suffix
#$(map (lambda (input)
(file-append (this-package-input input) "/bin"))
'("gzip" "bzip2" "xz" "p7zip")))))
- ;; These programs use sprintf on buffers with magic
- ;; values to construct commands (yes, eww), so we
- ;; can't easily substitute* them.
- '("lglddtrace" "lgluntrace" "lingeling" "plingeling"))))))))
- (inputs (list `(,aiger "static") bash-minimal gzip bzip2 xz p7zip))
- (home-page "http://fmv.jku.at/lingeling")
- (synopsis "SAT solver")
- (description "This package provides a range of SAT solvers, including
+ ;; These programs use sprintf on buffers with magic
+ ;; values to construct commands (yes, eww), so we
+ ;; can't easily substitute* them.
+ '("lglddtrace" "lgluntrace" "lingeling" "plingeling"))))))))
+ (inputs (list `(,aiger "static") bash-minimal gzip bzip2 xz p7zip))
+ (home-page "http://fmv.jku.at/lingeling")
+ (synopsis "SAT solver")
+ (description "This package provides a range of SAT solvers, including
the sequential @command{lingeling} and its parallel variants
@command{plingeling} and @command{treengeling}. A bounded model checker is
also included.")
- (license license:expat))))
+ (license license:expat)))
(define-public louvain-community
(let ((commit "8cc5382d4844af127b1c1257373740d7e6b76f1e")
--
2.46.0
Liliana Marie Prikler <liliana.prikler <at> gmail.com>:Liliana Marie Prikler <liliana.prikler <at> gmail.com>:Message #34 received at 73551-done <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: 73551-done <at> debbugs.gnu.org Subject: Re: [PATCH 0/8] Update some SAT/ASP solvers Date: Sun, 06 Oct 2024 16:19:14 +0200
Am Sonntag, dem 29.09.2024 um 11:16 +0200 schrieb Liliana Marie Prikler: > Liliana Marie Prikler (8): > gnu: scasp: Update to 1.1.4. > gnu: kissat: Update to 4.0.1. > gnu: z3: Update to 4.13.0. > gnu: lingeling: Update to 1.0.0. > gnu: Add cadical. > gnu: Add cadiback. > gnu: Add cadiback-for-cryptominisat. > gnu: cryptominisat: Update to 5.11.22. Done and pushed.
Debbugs Internal Request <help-debbugs <at> gnu.org>
to internal_control <at> debbugs.gnu.org.
(Mon, 04 Nov 2024 12:24:14 GMT) Full text and rfc822 format available.
GNU bug tracking system
Copyright (C) 1999 Darren O. Benham,
1997,2003 nCipher Corporation Ltd,
1994-97 Ian Jackson.