From patchwork Tue Jan 9 13:41:01 2024 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Max Heisinger X-Patchwork-Id: 58701 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id A372A27BBEA; Tue, 9 Jan 2024 15:26:17 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-2.9 required=5.0 tests=BAYES_00,MAILING_LIST_MULTI, SPF_HELO_PASS,URIBL_BLOCKED autolearn=ham autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id 73B1927BBE2 for ; Tue, 9 Jan 2024 15:26:16 +0000 (GMT) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1rNDzR-0000ml-Pf; Tue, 09 Jan 2024 10:26:06 -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 ) id 1rNDex-00086P-Gm for guix-patches@gnu.org; Tue, 09 Jan 2024 10:04:55 -0500 Received: from debbugs.gnu.org ([2001:470:142:5::43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1rNDex-0001Od-7v for guix-patches@gnu.org; Tue, 09 Jan 2024 10:04:55 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1rNDf3-0002Dv-Qq for guix-patches@gnu.org; Tue, 09 Jan 2024 10:05:01 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#68347] [PATCH] gnu: Add cadical Resent-From: Max Heisinger Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Tue, 09 Jan 2024 15:05:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 68347 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 68347@debbugs.gnu.org X-Debbugs-Original-To: guix-patches@gnu.org Received: via spool by submit@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 ) id 1rNDe2-0002CA-O9 for submit@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 ) id 1rNCMK-0000rQ-A9 for submit@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 ) id 1rNCM7-0006nN-5p for guix-patches@gnu.org; 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 ) id 1rNCM4-00049e-TR for guix-patches@gnu.org; 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 ; Tue, 9 Jan 2024 14:41:01 +0100 (CET) Message-ID: Date: Tue, 9 Jan 2024 14:41:01 +0100 MIME-Version: 1.0 User-Agent: Mozilla Thunderbird From: Max Heisinger Content-Language: en-US Received-SPF: pass client-ip=140.78.3.66; envelope-from=maximilian.heisinger@jku.at; 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-Mailman-Approved-At: Tue, 09 Jan 2024 10:03:57 -0500 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-Mailman-Approved-At: Tue, 09 Jan 2024 10:26:03 -0500 X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org X-getmail-retrieved-from-mailbox: Patches From 89b262587c67bb2761f7bf62f3d2f5dfc065c669 Mon Sep 17 00:00:00 2001 Message-ID: <89b262587c67bb2761f7bf62f3d2f5dfc065c669.1704807579.git.maximilian.heisinger@jku.at> From: Max Heisinger 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(+) base-commit: 8920cf302c5a2fd457a2629afe24cf4768f1fed7 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 = \"\"") + (("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") + "")) + ;; 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")