X-Loop: help-debbugs@HIDDEN
Subject: [bug#68347] [PATCH] gnu: Add cadical
Resent-From: Max Heisinger <maximilian.heisinger@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Tue, 09 Jan 2024 15:05:01 +0000
Resent-Message-ID: <handler.68347.B.17048126458469 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
X-GNU-PR-Message: report 68347
X-GNU-PR-Package: guix-patches
X-GNU-PR-Keywords: patch
To: 68347 <at> debbugs.gnu.org
X-Debbugs-Original-To: guix-patches@HIDDEN
Received: via spool by submit <at> debbugs.gnu.org id=B.17048126458469
(code B ref -1); Tue, 09 Jan 2024 15:05:01 +0000
Received: (at submit) by debbugs.gnu.org; 9 Jan 2024 15:04:05 +0000
Received: from localhost ([127.0.0.1]:40681 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1rNDe2-0002CA-O9
for submit <at> debbugs.gnu.org; Tue, 09 Jan 2024 10:04:04 -0500
Received: from lists.gnu.org ([2001:470:142::17]:58366)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <maximilian.heisinger@HIDDEN>) id 1rNCMK-0000rQ-A9
for submit <at> debbugs.gnu.org; Tue, 09 Jan 2024 08:41:37 -0500
Received: from eggs.gnu.org ([2001:470:142:3::10])
by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from <maximilian.heisinger@HIDDEN>)
id 1rNCM7-0006nN-5p
for guix-patches@HIDDEN; Tue, 09 Jan 2024 08:41:23 -0500
Received: from emailsecure.uni-linz.ac.at ([140.78.3.66])
by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from <maximilian.heisinger@HIDDEN>)
id 1rNCM4-00049e-TR
for guix-patches@HIDDEN; Tue, 09 Jan 2024 08:41:22 -0500
Received: from [140.78.11.12] (unknown [140.78.11.12])
(using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits))
(No client certificate requested)
by emailsecure.uni-linz.ac.at (Postfix) with ESMTPSA id 4T8XBj28Lrz2PRX
for <guix-patches@HIDDEN>; Tue, 9 Jan 2024 14:41:01 +0100 (CET)
Message-ID: <cb61e44b-4ae5-4a78-a90c-8e07baa4c693@HIDDEN>
Date: Tue, 9 Jan 2024 14:41:01 +0100
MIME-Version: 1.0
User-Agent: Mozilla Thunderbird
From: Max Heisinger <maximilian.heisinger@HIDDEN>
Content-Language: en-US
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Received-SPF: pass client-ip=140.78.3.66;
envelope-from=maximilian.heisinger@HIDDEN; helo=emailsecure.uni-linz.ac.at
X-Spam_score_int: -41
X-Spam_score: -4.2
X-Spam_bar: ----
X-Spam_report: (-4.2 / 5.0 requ) BAYES_00=-1.9, RCVD_IN_DNSWL_MED=-2.3,
RCVD_IN_MSPIKE_H3=0.001, RCVD_IN_MSPIKE_WL=0.001, SPF_HELO_NONE=0.001,
SPF_PASS=-0.001, T_SCC_BODY_TEXT_LINE=-0.01 autolearn=ham autolearn_force=no
X-Spam_action: no action
X-Spam-Score: 1.7 (+)
X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org",
has NOT identified this incoming email as spam. The original
message has been attached to this so you can view it or label
similar future email. If you have any questions, see
the administrator of that system for details.
Content preview: From 89b262587c67bb2761f7bf62f3d2f5dfc065c669 Mon Sep 17
00:00:00 2001 Message-ID:
<89b262587c67bb2761f7bf62f3d2f5dfc065c669.1704807579.git.maximilian.heisinger@HIDDEN>
From: Max Heisinger <maximilia [...]
Content analysis details: (1.7 points, 10.0 required)
pts rule name description
---- ---------------------- --------------------------------------------------
1.7 URIBL_BLACK Contains an URL listed in the URIBL blacklist
[URIs: run.sh]
0.0 T_SPF_PERMERROR SPF: test of record failed (permerror)
-0.0 SPF_HELO_PASS SPF: HELO matches SPF record
-0.0 T_SCC_BODY_TEXT_LINE No description available.
X-Mailman-Approved-At: Tue, 09 Jan 2024 10:03:57 -0500
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: 0.7 (/)
From 89b262587c67bb2761f7bf62f3d2f5dfc065c669 Mon Sep 17 00:00:00 2001
Message-ID: <89b262587c67bb2761f7bf62f3d2f5dfc065c669.1704807579.git.maximilian.heisinger@HIDDEN>
From: Max Heisinger <maximilian.heisinger@HIDDEN>
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
Content-Disposition: inline Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-Mailer: MIME-tools 5.505 (Entity 5.505) Content-Type: text/plain; charset=utf-8 X-Loop: help-debbugs@HIDDEN From: help-debbugs@HIDDEN (GNU bug Tracking System) To: Max Heisinger <maximilian.heisinger@HIDDEN> Subject: bug#68347: Acknowledgement ([PATCH] gnu: Add cadical) Message-ID: <handler.68347.B.17048126458469.ack <at> debbugs.gnu.org> References: <cb61e44b-4ae5-4a78-a90c-8e07baa4c693@HIDDEN> X-Gnu-PR-Message: ack 68347 X-Gnu-PR-Package: guix-patches X-Gnu-PR-Keywords: patch Reply-To: 68347 <at> debbugs.gnu.org Date: Tue, 09 Jan 2024 15:05:01 +0000 Thank you for filing a new bug report with debbugs.gnu.org. This is an automatically generated reply to let you know your message has been received. Your message is being forwarded to the package maintainers and other interested parties for their attention; they will reply in due course. Your message has been sent to the package maintainer(s): guix-patches@HIDDEN If you wish to submit further information on this problem, please send it to 68347 <at> debbugs.gnu.org. Please do not send mail to help-debbugs@HIDDEN unless you wish to report a problem with the Bug-tracking system. --=20 68347: https://debbugs.gnu.org/cgi/bugreport.cgi?bug=3D68347 GNU Bug Tracking System Contact help-debbugs@HIDDEN with problems
GNU bug tracking system
Copyright (C) 1999 Darren O. Benham,
1997 nCipher Corporation Ltd,
1994-97 Ian Jackson.