GNU bug report logs - #68347
[PATCH] gnu: Add cadical

Previous Next

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 68347 in the body.
You can then email your comments to 68347 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Max Heisinger <maximilian.heisinger <at> jku.at>
To: guix-patches <at> gnu.org
Subject: [PATCH] gnu: Add cadical
Date: Tue, 9 Jan 2024 14:41:01 +0100

From 89b262587c67bb2761f7bf62f3d2f5dfc065c669 Mon Sep 17 00:00:00 2001
Message-ID: <89b262587c67bb2761f7bf62f3d2f5dfc065c669.1704807579.git.maximilian.heisinger <at> jku.at>
From: Max Heisinger <maximilian.heisinger <at> jku.at>
Date: Tue, 9 Jan 2024 14:26:56 +0100
Subject: [PATCH] gnu: Add CaDiCaL.

* gnu/packages/maths.scm (cadical): Add package.

Change-Id: I300d454ce79623c737b9208623bcce0dde798f14
---
 gnu/packages/maths.scm | 91 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 91 insertions(+)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index adc7beb655..2b21ce3db2 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -8925,6 +8925,97 @@ (define-public kissat
 optimized algorithms and implementation.")
     (license license:expat)))
 
+(define-public cadical
+  (package
+    (name "cadical")
+    (version "1.9.4")
+    (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))
+       (sha256
+        (base32 "1sd3r1czgm6h36fa5if2npnjpfnxjnzlnc2srkbwi2ywvsysyavi"))))
+    (build-system gnu-build-system)
+    (inputs (list xz gzip lzip bzip2 p7zip))
+    (arguments
+     (list
+      #:test-target "test"
+      #:phases #~(modify-phases %standard-phases
+                   (add-after 'unpack 'patch-source
+                     (lambda* (#:key inputs outputs source #:allow-other-keys)
+                       (substitute* "src/file.cpp"
+                         (("(bzip2|gzip|lzma|xz) -c" all cmd)
+                          (string-append (search-input-file inputs
+                                                            (string-append
+                                                             "bin/" cmd))
+                                         " -c"))
+                         (("7z ([ax])" all mode)
+                          (string-append (search-input-file inputs "bin/7z")
+                                         " " mode))
+                         ;; Since we hard-coded the paths, we no longer need to find
+                         ;; them.
+                         (("char \\*found = find\\_program \\(prg\\)")
+                          "const char* found = \"<configured-at-build-time>\"")
+                         (("delete\\[\\] found;")
+                          ""))
+                       (substitute* "scripts/make-build-header.sh"
+                         ;; The identifier in Guix is the source, as the input may be
+                         ;; replaced while building.
+                         (("`../scripts/get-git-id.sh`")
+                          source)
+                         ;; Remove non-determinism by removing the date from the
+                         ;; binary.
+                         (("\\$DATE")
+                          "<no non-deterministic timestamp in the binary>"))
+                       ;; Convert the static library to a shared one.
+                       (substitute* "makefile.in"
+                         (("libcadical\\.a")
+                          "libcadical.so")
+                         (("\\$\\(COMPILE\\) -o")
+                          (string-append "$(COMPILE) -Wl,-rpath="
+                                         (assoc-ref outputs "out") "/lib -o"))
+                         (("ar rc")
+                          "$(COMPILE) -shared -o"))
+                       (substitute* "test/api/run.sh"
+                         (("libcadical\\.a")
+                          "libcadical.so"))
+                       (substitute* "configure"
+                         (("-static")
+                          "-shared")
+                         ;; Tests are not written with a shared libcadical.so in
+                         ;; mind, so the LD_LIBRARY_PATH has to be set to the
+                         ;; libcadical.so in the build directory while running
+                         ;; tests. The rpath points to the installed directory and is
+                         ;; only available after installation.
+                         (("\\\\\\$\\(MAKE\\)")
+                          (string-append "export LD_LIBRARY_PATH="
+                                         (getcwd) "/build/ ; \\\\\\$(MAKE)"))
+                         (("CXXFLAGS=\"\\$CXXFLAGS\\$options\"")
+                          "CXXFLAGS=\"$CXXFLAGS$options -fPIC\""))))
+                   (replace 'configure
+                     (lambda* (#:key configure-flags #:allow-other-keys)
+                       ;; The configure script does not support standard GNU options.
+                       (apply invoke "./configure" configure-flags)))
+                   (replace 'install
+                     (lambda* (#:key inputs outputs #:allow-other-keys)
+                       (let ((out (assoc-ref outputs "out")))
+                         (install-file "build/cadical"
+                                       (string-append out "/bin"))
+                         (install-file "build/libcadical.so"
+                                       (string-append out "/lib"))
+                         (install-file "src/cadical.hpp"
+                                       (string-append out "/include"))))))))
+    (home-page "https://github.com/arminbiere/cadical")
+    (synopsis "CaDiCaL Simplified Satisfiability (SAT) Solver")
+    (description
+     "CaDiCaL is a hackable CDCL SAT solver written in C++. It offers an incremental
+API and a library for solving SAT problems given in CNF in the standard DIMACS
+format.")
+    (license license:expat)))
+
 (define-public aiger
   (package
     (name "aiger")

base-commit: 8920cf302c5a2fd457a2629afe24cf4768f1fed7
-- 
2.41.0

Message #8 received at 68347 <at> debbugs.gnu.org (full text, mbox):

From: Sören Tempel <soeren <at> soeren-tempel.net>
To: 68347 <at> debbugs.gnu.org
Cc: andreas <at> enge.fr, bavier <at> posteo.net, sharlatanus <at> gmail.com,
 maximilian.heisinger <at> jku.at
Subject: Re: [PATCH] gnu: Add cadical
Date: Sat, 18 May 2024 22:48:09 +0200

Hi,

I also started working on a CaDiCaL package for a channel of mine [1].
My version is very similar but uses a Fedora-based patch to build a
shared library instead of substitutions. However, the approach chosen
here is also fine with me.

Is there a chance that this could get merged so that we can join forces
and maintain a single CaDiCaL package in the main Guix repository? :)

Best,
Sören

[1]: https://github.com/agra-uni-bremen/guix-symex/commit/236b84c15bd7cc51bb935c7d85d2fbb270b30499

Message #11 received at 68347 <at> debbugs.gnu.org (full text, mbox):

From: Max Heisinger <maximilian.heisinger <at> jku.at>
To: 68347 <at> debbugs.gnu.org
Subject: Re: [PATCH] gnu: Add cadical
Date: Wed, 22 May 2024 16:22:28 +0200

Hi,

thank you for your patch-based approach Sören! I think yours is more readable
for the Makefile changes.

We could add the substitutions for 7z, xz, etc. and the changes to
scripts/make-build-header.sh in order to make the build reproducible and not
rely on runtime $PATH searches, then we'd have combined the best from both
patches - however I'd also be fine to start with my original version and add
the patch in a later revision.

I would also be happy if we could maintain a single CaDiCaL package in the main
Guix repository :)

Best,
Max

Message #16 received at 68347-submitter <at> debbugs.gnu.org (full text, mbox):

From: Steve George <steve <at> futurile.net>
To: control <at> debbugs.gnu.org
Cc: 68347-submitter <at> debbugs.gnu.org
Subject: closing 68347
Date: Wed, 13 Nov 2024 17:01:22 +0000

# hi both - looks like cadical is at 2.0.0 in the archive.
# thanks for sending this contribution in.
close 68347 
quit

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.