all messages for Guix-related lists mirrored at yhetil.org
 help / color / mirror / code / Atom feed
* [bug#73551] [PATCH 1/8] gnu: scasp: Update to 1.1.4.
  2024-09-29  9:16 [bug#73551] [PATCH 0/8] Update some SAT/ASP solvers Liliana Marie Prikler
@ 2024-09-25 19:03 ` Liliana Marie Prikler
  2024-09-25 19:03 ` [bug#73551] [PATCH 2/8] gnu: kissat: Update to 4.0.1 Liliana Marie Prikler
                   ` (7 subsequent siblings)
  8 siblings, 0 replies; 10+ messages in thread
From: Liliana Marie Prikler @ 2024-09-25 19:03 UTC (permalink / raw)
  To: 73551

* 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





^ permalink raw reply related	[flat|nested] 10+ messages in thread

* [bug#73551] [PATCH 2/8] gnu: kissat: Update to 4.0.1.
  2024-09-29  9:16 [bug#73551] [PATCH 0/8] Update some SAT/ASP solvers Liliana Marie Prikler
  2024-09-25 19:03 ` [bug#73551] [PATCH 1/8] gnu: scasp: Update to 1.1.4 Liliana Marie Prikler
@ 2024-09-25 19:03 ` Liliana Marie Prikler
  2024-09-25 19:55 ` [bug#73551] [PATCH 3/8] gnu: z3: Update to 4.13.0 Liliana Marie Prikler
                   ` (6 subsequent siblings)
  8 siblings, 0 replies; 10+ messages in thread
From: Liliana Marie Prikler @ 2024-09-25 19:03 UTC (permalink / raw)
  To: 73551

* 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





^ permalink raw reply related	[flat|nested] 10+ messages in thread

* [bug#73551] [PATCH 3/8] gnu: z3: Update to 4.13.0.
  2024-09-29  9:16 [bug#73551] [PATCH 0/8] Update some SAT/ASP solvers Liliana Marie Prikler
  2024-09-25 19:03 ` [bug#73551] [PATCH 1/8] gnu: scasp: Update to 1.1.4 Liliana Marie Prikler
  2024-09-25 19:03 ` [bug#73551] [PATCH 2/8] gnu: kissat: Update to 4.0.1 Liliana Marie Prikler
@ 2024-09-25 19:55 ` Liliana Marie Prikler
  2024-09-25 20:02 ` [bug#73551] [PATCH 4/8] gnu: lingeling: Update to 1.0.0 Liliana Marie Prikler
                   ` (5 subsequent siblings)
  8 siblings, 0 replies; 10+ messages in thread
From: Liliana Marie Prikler @ 2024-09-25 19:55 UTC (permalink / raw)
  To: 73551

* 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





^ permalink raw reply related	[flat|nested] 10+ messages in thread

* [bug#73551] [PATCH 4/8] gnu: lingeling: Update to 1.0.0.
  2024-09-29  9:16 [bug#73551] [PATCH 0/8] Update some SAT/ASP solvers Liliana Marie Prikler
                   ` (2 preceding siblings ...)
  2024-09-25 19:55 ` [bug#73551] [PATCH 3/8] gnu: z3: Update to 4.13.0 Liliana Marie Prikler
@ 2024-09-25 20:02 ` Liliana Marie Prikler
  2024-09-29  9:00 ` [bug#73551] [PATCH 5/8] gnu: Add cadical Liliana Marie Prikler
                   ` (4 subsequent siblings)
  8 siblings, 0 replies; 10+ messages in thread
From: Liliana Marie Prikler @ 2024-09-25 20:02 UTC (permalink / raw)
  To: 73551

* 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





^ permalink raw reply related	[flat|nested] 10+ messages in thread

* [bug#73551] [PATCH 5/8] gnu: Add cadical.
  2024-09-29  9:16 [bug#73551] [PATCH 0/8] Update some SAT/ASP solvers Liliana Marie Prikler
                   ` (3 preceding siblings ...)
  2024-09-25 20:02 ` [bug#73551] [PATCH 4/8] gnu: lingeling: Update to 1.0.0 Liliana Marie Prikler
@ 2024-09-29  9:00 ` Liliana Marie Prikler
  2024-09-29  9:04 ` [bug#73551] [PATCH 6/8] gnu: Add cadiback Liliana Marie Prikler
                   ` (3 subsequent siblings)
  8 siblings, 0 replies; 10+ messages in thread
From: Liliana Marie Prikler @ 2024-09-29  9:00 UTC (permalink / raw)
  To: 73551

* 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@gmail.com>
+Date: Sun, 2 Jun 2024 21:50:06 -0400
+Subject: [PATCH] Also add a dynamic library
+
+---
+Liliana Marie Prikler <liliana.prikler@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





^ permalink raw reply related	[flat|nested] 10+ messages in thread

* [bug#73551] [PATCH 6/8] gnu: Add cadiback.
  2024-09-29  9:16 [bug#73551] [PATCH 0/8] Update some SAT/ASP solvers Liliana Marie Prikler
                   ` (4 preceding siblings ...)
  2024-09-29  9:00 ` [bug#73551] [PATCH 5/8] gnu: Add cadical Liliana Marie Prikler
@ 2024-09-29  9:04 ` Liliana Marie Prikler
  2024-09-29  9:04 ` [bug#73551] [PATCH 7/8] gnu: Add cadiback-for-cryptominisat Liliana Marie Prikler
                   ` (2 subsequent siblings)
  8 siblings, 0 replies; 10+ messages in thread
From: Liliana Marie Prikler @ 2024-09-29  9:04 UTC (permalink / raw)
  To: 73551

* 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





^ permalink raw reply related	[flat|nested] 10+ messages in thread

* [bug#73551] [PATCH 7/8] gnu: Add cadiback-for-cryptominisat.
  2024-09-29  9:16 [bug#73551] [PATCH 0/8] Update some SAT/ASP solvers Liliana Marie Prikler
                   ` (5 preceding siblings ...)
  2024-09-29  9:04 ` [bug#73551] [PATCH 6/8] gnu: Add cadiback Liliana Marie Prikler
@ 2024-09-29  9:04 ` Liliana Marie Prikler
  2024-09-29  9:08 ` [bug#73551] [PATCH 8/8] gnu: cryptominisat: Update to 5.11.22 Liliana Marie Prikler
  2024-10-06 14:19 ` bug#73551: [PATCH 0/8] Update some SAT/ASP solvers Liliana Marie Prikler
  8 siblings, 0 replies; 10+ messages in thread
From: Liliana Marie Prikler @ 2024-09-29  9:04 UTC (permalink / raw)
  To: 73551

* 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





^ permalink raw reply related	[flat|nested] 10+ messages in thread

* [bug#73551] [PATCH 8/8] gnu: cryptominisat: Update to 5.11.22.
  2024-09-29  9:16 [bug#73551] [PATCH 0/8] Update some SAT/ASP solvers Liliana Marie Prikler
                   ` (6 preceding siblings ...)
  2024-09-29  9:04 ` [bug#73551] [PATCH 7/8] gnu: Add cadiback-for-cryptominisat Liliana Marie Prikler
@ 2024-09-29  9:08 ` Liliana Marie Prikler
  2024-10-06 14:19 ` bug#73551: [PATCH 0/8] Update some SAT/ASP solvers Liliana Marie Prikler
  8 siblings, 0 replies; 10+ messages in thread
From: Liliana Marie Prikler @ 2024-09-29  9:08 UTC (permalink / raw)
  To: 73551

* 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





^ permalink raw reply related	[flat|nested] 10+ messages in thread

* [bug#73551] [PATCH 0/8] Update some SAT/ASP solvers
@ 2024-09-29  9:16 Liliana Marie Prikler
  2024-09-25 19:03 ` [bug#73551] [PATCH 1/8] gnu: scasp: Update to 1.1.4 Liliana Marie Prikler
                   ` (8 more replies)
  0 siblings, 9 replies; 10+ messages in thread
From: Liliana Marie Prikler @ 2024-09-29  9:16 UTC (permalink / raw)
  To: 73551

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





^ permalink raw reply	[flat|nested] 10+ messages in thread

* bug#73551: [PATCH 0/8] Update some SAT/ASP solvers
  2024-09-29  9:16 [bug#73551] [PATCH 0/8] Update some SAT/ASP solvers Liliana Marie Prikler
                   ` (7 preceding siblings ...)
  2024-09-29  9:08 ` [bug#73551] [PATCH 8/8] gnu: cryptominisat: Update to 5.11.22 Liliana Marie Prikler
@ 2024-10-06 14:19 ` Liliana Marie Prikler
  8 siblings, 0 replies; 10+ messages in thread
From: Liliana Marie Prikler @ 2024-10-06 14:19 UTC (permalink / raw)
  To: 73551-done

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.




^ permalink raw reply	[flat|nested] 10+ messages in thread

end of thread, other threads:[~2024-10-06 14:21 UTC | newest]

Thread overview: 10+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2024-09-29  9:16 [bug#73551] [PATCH 0/8] Update some SAT/ASP solvers Liliana Marie Prikler
2024-09-25 19:03 ` [bug#73551] [PATCH 1/8] gnu: scasp: Update to 1.1.4 Liliana Marie Prikler
2024-09-25 19:03 ` [bug#73551] [PATCH 2/8] gnu: kissat: Update to 4.0.1 Liliana Marie Prikler
2024-09-25 19:55 ` [bug#73551] [PATCH 3/8] gnu: z3: Update to 4.13.0 Liliana Marie Prikler
2024-09-25 20:02 ` [bug#73551] [PATCH 4/8] gnu: lingeling: Update to 1.0.0 Liliana Marie Prikler
2024-09-29  9:00 ` [bug#73551] [PATCH 5/8] gnu: Add cadical Liliana Marie Prikler
2024-09-29  9:04 ` [bug#73551] [PATCH 6/8] gnu: Add cadiback Liliana Marie Prikler
2024-09-29  9:04 ` [bug#73551] [PATCH 7/8] gnu: Add cadiback-for-cryptominisat Liliana Marie Prikler
2024-09-29  9:08 ` [bug#73551] [PATCH 8/8] gnu: cryptominisat: Update to 5.11.22 Liliana Marie Prikler
2024-10-06 14:19 ` bug#73551: [PATCH 0/8] Update some SAT/ASP solvers Liliana Marie Prikler

Code repositories for project(s) associated with this external index

	https://git.savannah.gnu.org/cgit/guix.git

This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.