From unknown Sat Jun 21 12:35:30 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#78246] [PATCH 0/3] gnu: Add bitwuzla. Resent-From: soeren@soeren-tempel.net Original-Sender: "Debbugs-submit" Resent-CC: andreas@enge.fr, bavier@posteo.net, sharlatanus@gmail.com, guix-patches@gnu.org Resent-Date: Sun, 04 May 2025 17:38:05 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 78246 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 78246@debbugs.gnu.org Cc: liliana.prikler@gmail.com, Andreas Enge , Eric Bavier , Sharlatan Hellseher X-Debbugs-Original-To: guix-patches@gnu.org X-Debbugs-Original-Xcc: Andreas Enge , Eric Bavier , Sharlatan Hellseher Received: via spool by submit@debbugs.gnu.org id=B.174638028411088 (code B ref -1); Sun, 04 May 2025 17:38:05 +0000 Received: (at submit) by debbugs.gnu.org; 4 May 2025 17:38:04 +0000 Received: from localhost ([127.0.0.1]:59082 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1uBdHs-0002s0-1o for submit@debbugs.gnu.org; Sun, 04 May 2025 13:38:02 -0400 Received: from lists.gnu.org ([2001:470:142::17]:52130) by debbugs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.84_2) (envelope-from ) id 1uBdHn-0002qx-Hf for submit@debbugs.gnu.org; Sun, 04 May 2025 13:37:56 -0400 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 1uBdHf-0005T3-Rt for guix-patches@gnu.org; Sun, 04 May 2025 13:37:48 -0400 Received: from magnesium.8pit.net ([45.76.88.171]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1uBdHd-0002KO-NR; Sun, 04 May 2025 13:37:47 -0400 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; s=opensmtpd; bh=1c84fXON Wz3jindO7qBjHtzfDm2+ay9HShSy07rdQ0U=; h=date:subject:cc:to:from; d=soeren-tempel.net; b=wUvnWvtbHWfnLn0mZeEWKG36/MlgysDo4gvHQe2LUf1Coiu RqT82Uwb1jer4X+38KGlmNcqCMYg3fTdd66XksM0OErciBGeQ/MMyjN5hK3D2pLI0Zo+9l T+h3LmjCRvGllTX2KMsF9xyoSrxisnsAWnzMl+HgRxeBqhtH4pli1U= Received: from localhost ( [2a02:560:4d21:3f00:4392:0:6418:52]) by magnesium.8pit.net (OpenSMTPD) with ESMTPSA id 6bffdadd (TLSv1.3:TLS_AES_256_GCM_SHA384:256:YES); Sun, 4 May 2025 19:37:40 +0200 (CEST) From: soeren@soeren-tempel.net Date: Sun, 4 May 2025 19:34:41 +0200 Message-ID: X-Mailer: git-send-email 2.49.0 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Received-SPF: pass client-ip=45.76.88.171; envelope-from=soeren@soeren-tempel.net; helo=magnesium.8pit.net X-Spam_score_int: -20 X-Spam_score: -2.1 X-Spam_bar: -- X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, RCVD_IN_VALIDITY_RPBL_BLOCKED=0.001, RCVD_IN_VALIDITY_SAFE_BLOCKED=0.001, SPF_HELO_NONE=0.001, SPF_PASS=-0.001 autolearn=ham autolearn_force=no X-Spam_action: no action X-Spam-Score: 0.9 (/) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.1 (/) From: Sören Tempel This patchsets adds bitwuzla an SMT solver which is especially efficent for bitvector theory and can be used with the already packaged BINSEC symbolic executor. While packaging bitwuzla, I also noticed and fixed a bug regarding the installed header files for cadical (CC: liliana.prikler@) and added a package for symfpu, which is a dependency of bitwuzla. Sören Tempel (3): gnu: cadical: also install C++ header file to /usr/include gnu: Add symfpu. gnu: Add bitwuzla. gnu/packages/maths.scm | 96 +++++++++++++++++++++++++++++++++++++++++- 1 file changed, 95 insertions(+), 1 deletion(-) base-commit: 415e3d98d6faf5fd3d1b7b3daa2f20636e4ff822 From unknown Sat Jun 21 12:35:30 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#78246] [PATCH 1/3] gnu: cadical: also install C++ header file to /usr/include Resent-From: soeren@soeren-tempel.net Original-Sender: "Debbugs-submit" Resent-CC: andreas@enge.fr, bavier@posteo.net, sharlatanus@gmail.com, guix-patches@gnu.org Resent-Date: Sun, 04 May 2025 17:41:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 78246 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 78246@debbugs.gnu.org Cc: Andreas Enge , Eric Bavier , Sharlatan Hellseher X-Debbugs-Original-Xcc: Andreas Enge , Eric Bavier , Sharlatan Hellseher Received: via spool by 78246-submit@debbugs.gnu.org id=B78246.174638044612748 (code B ref 78246); Sun, 04 May 2025 17:41:02 +0000 Received: (at 78246) by debbugs.gnu.org; 4 May 2025 17:40:46 +0000 Received: from localhost ([127.0.0.1]:59124 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1uBdKU-0003J1-2p for submit@debbugs.gnu.org; Sun, 04 May 2025 13:40:45 -0400 Received: from magnesium.8pit.net ([45.76.88.171]:38949) by debbugs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.84_2) (envelope-from ) id 1uBdKP-0003Hg-A1; Sun, 04 May 2025 13:40:39 -0400 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; s=opensmtpd; bh=EtoJsTLC 6GcizYOtYy31am5beHGZ1Z/WnskFyGznmSU=; h=references:in-reply-to:date: subject:to:from; d=soeren-tempel.net; b=scRihYjcF4se6o3/V0CIqKRlUshs7g m6dVf6EqcatIlNAFyOIrTZUdYcGx0YIKIllvDTXUBKxYFEc+8VG6D4NHSfhdSQRoe1nzfg BC323w6gFZ81B1OQnOERVeQFgK6tlrsP7RNy93yhSHajbTs1FdQUuRVSW+XS0YUNLrJNWl o= Received: from localhost ( [2a02:560:4d21:3f00:4392:0:6418:52]) by magnesium.8pit.net (OpenSMTPD) with ESMTPSA id 40fc4e1c (TLSv1.3:TLS_AES_256_GCM_SHA384:256:YES); Sun, 4 May 2025 19:40:35 +0200 (CEST) From: soeren@soeren-tempel.net Date: Sun, 4 May 2025 19:40:26 +0200 Message-ID: <69e8ea179aa197f93452e94c402db520264a796a.1746379841.git.soeren@soeren-tempel.net> X-Mailer: git-send-email 2.49.0 In-Reply-To: References: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-Spam-Score: 0.0 (/) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) From: Sören Tempel * gnu/packages/maths.scm (cadical)[arguments]: Install cadical.hpp. --- gnu/packages/maths.scm | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index eb23a375b4..53f726f620 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -9840,7 +9840,7 @@ (define-public cadical #:install-plan `(("build" "bin" #:include ("cadical" "mobical")) ("build" "lib" #:include-regexp ("libcadical\\.(a|so)$")) - ("src" "include" #:include ("cadical.h")) + ("src" "include" #:include ("cadical.h" "cadical.hpp")) ;; Internal headers used by cadiback. ("src" "include/cadical" #:include-regexp ("\\.hpp$"))) args)))))) From unknown Sat Jun 21 12:35:30 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#78246] [PATCH 2/3] gnu: Add symfpu. Resent-From: soeren@soeren-tempel.net Original-Sender: "Debbugs-submit" Resent-CC: andreas@enge.fr, bavier@posteo.net, sharlatanus@gmail.com, guix-patches@gnu.org Resent-Date: Sun, 04 May 2025 17:41:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 78246 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 78246@debbugs.gnu.org Cc: Andreas Enge , Eric Bavier , Sharlatan Hellseher X-Debbugs-Original-Xcc: Andreas Enge , Eric Bavier , Sharlatan Hellseher Received: via spool by 78246-submit@debbugs.gnu.org id=B78246.174638044812767 (code B ref 78246); Sun, 04 May 2025 17:41:02 +0000 Received: (at 78246) by debbugs.gnu.org; 4 May 2025 17:40:48 +0000 Received: from localhost ([127.0.0.1]:59126 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1uBdKZ-0003Jp-Pn for submit@debbugs.gnu.org; Sun, 04 May 2025 13:40:48 -0400 Received: from magnesium.8pit.net ([2001:19f0:6c01:4ae:5400:ff:fe66:af9d]:11503) by debbugs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.84_2) (envelope-from ) id 1uBdKQ-0003Hx-I5; Sun, 04 May 2025 13:40:41 -0400 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; s=opensmtpd; bh=OgyfYjBF c6Lgbew717kUzKNokZ9mR4GxlRMO8KzFmqU=; h=references:in-reply-to:date: subject:to:from; d=soeren-tempel.net; b=O++jzQQMgFsmoA3ZbubYhwltG5Y19n ojHLq/gC8cGkDdVRmrCZKzGDsl/ImrV90KpviUe9bTzcfN8bLhDHh77XWR7BQykyFV4gpj i4unXxJZpNJ0gkDxoEO9VcvbAxuRE9VW7kpURkufaiQCgUZ1KLExxWeTlx59SuyM0y7TdM A= Received: from localhost ( [2a02:560:4d21:3f00:4392:0:6418:52]) by magnesium.8pit.net (OpenSMTPD) with ESMTPSA id a0b878a4 (TLSv1.3:TLS_AES_256_GCM_SHA384:256:YES); Sun, 4 May 2025 19:40:36 +0200 (CEST) From: soeren@soeren-tempel.net Date: Sun, 4 May 2025 19:40:27 +0200 Message-ID: <75016ee93ed5132c6c3cff0d078e84fdf301b246.1746379841.git.soeren@soeren-tempel.net> X-Mailer: git-send-email 2.49.0 In-Reply-To: References: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-Spam-Score: 0.0 (/) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) From: Sören Tempel * gnu/packages/maths.scm (symfpu): New variable. --- gnu/packages/maths.scm | 56 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 56 insertions(+) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 53f726f620..572912ca82 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -8218,6 +8218,62 @@ (define-public yices s-expression-based format.") (license license:gpl3+))) +(define-public symfpu + (let ((commit "22d993d880f66b2e470c3928e0e61bdf61419702")) + (package + (name "symfpu") + (version (git-version "20220910" "0" commit)) + (source + (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/martin-cs/symfpu") + (commit commit))) + (file-name (git-file-name name version)) + (sha256 + (base32 "1h20zzkyi225290kc6mzg8i4dwkj0p1vlwfgc9ycs61snlyd8gr8")))) + (build-system copy-build-system) + (arguments + (list + #:phases + #~(modify-phases %standard-phases + (delete 'configure) + (replace 'install + (lambda* (#:key outputs #:allow-other-keys) + (let* ((outdir (assoc-ref outputs "out")) + (incdir (string-append outdir "/include/symfpu")) + (libdir (string-append outdir "/lib")) + + (coredir (string-append incdir "/core")) + (utilsdir (string-append incdir "/utils"))) + (mkdir-p coredir) + (mkdir-p utilsdir) + (copy-recursively "core" coredir) + (copy-recursively "utils" utilsdir) + (mkdir-p (string-append libdir "/pkgconfig")) + (with-output-to-file (string-append libdir + "/pkgconfig/symfpu.pc") + (lambda _ + (format #t + "prefix=~a~@ + exec_prefix=${prefix}~@ + includedir=${prefix}/include~@ + ~@ + ~@ + Name: symfpu~@ + Version: ~a~@ + Description: library for IEEE-754 floats~@ + Cflags: -I${includedir}~%" + outdir + #$version))))))))) + (synopsis + "Concrete and symbolic implementation of IEEE-754 floating-point numbers") + (description + "This library provides a C++ implementation of concrete and symbolic semantics +for floating point numbers as defined in IEEE Standard for Floating-Point Arithmetic.") + (home-page "https://github.com/martin-cs/symfpu") + (license license:gpl3)))) + (define-public z3 (package (name "z3") From unknown Sat Jun 21 12:35:30 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#78246] [PATCH 3/3] gnu: Add bitwuzla. Resent-From: soeren@soeren-tempel.net Original-Sender: "Debbugs-submit" Resent-CC: andreas@enge.fr, bavier@posteo.net, sharlatanus@gmail.com, guix-patches@gnu.org Resent-Date: Sun, 04 May 2025 17:41:03 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 78246 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 78246@debbugs.gnu.org Cc: Andreas Enge , Eric Bavier , Sharlatan Hellseher X-Debbugs-Original-Xcc: Andreas Enge , Eric Bavier , Sharlatan Hellseher Received: via spool by 78246-submit@debbugs.gnu.org id=B78246.174638044812773 (code B ref 78246); Sun, 04 May 2025 17:41:03 +0000 Received: (at 78246) by debbugs.gnu.org; 4 May 2025 17:40:48 +0000 Received: from localhost ([127.0.0.1]:59128 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1uBdKa-0003Js-75 for submit@debbugs.gnu.org; Sun, 04 May 2025 13:40:48 -0400 Received: from magnesium.8pit.net ([45.76.88.171]:38949) by debbugs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.84_2) (envelope-from ) id 1uBdKR-0003Hg-LZ; Sun, 04 May 2025 13:40:43 -0400 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; s=opensmtpd; bh=zKHOPBCR 18JsX67oT2R2IL8ES1HuClCMxC9kG9yU0P0=; h=references:in-reply-to:date: subject:to:from; d=soeren-tempel.net; b=DyYrnN0nx38HxkXi2Iysq9u54NrcVB Q4qq2c0gi1zDu5SwYKJgyaMlC2xBQa7xpk547tA5mR1jiu+o7yW28GmgZKG1pXWa5t2uHH 1YodFrSDlpljxiQMBRWMam9mzw+rwBVvvKyo15dS6hKXlpgkn3sY9f5qsircCa268pYpS3 A= Received: from localhost ( [2a02:560:4d21:3f00:4392:0:6418:52]) by magnesium.8pit.net (OpenSMTPD) with ESMTPSA id 5606f103 (TLSv1.3:TLS_AES_256_GCM_SHA384:256:YES); Sun, 4 May 2025 19:40:36 +0200 (CEST) From: soeren@soeren-tempel.net Date: Sun, 4 May 2025 19:40:28 +0200 Message-ID: <67a4e964dce6af0c08c7d2cf22b2de697d2aec77.1746379841.git.soeren@soeren-tempel.net> X-Mailer: git-send-email 2.49.0 In-Reply-To: References: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-Spam-Score: 0.0 (/) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) From: Sören Tempel * gnu/packages/maths.scm (bitwuzla): New variable. --- gnu/packages/maths.scm | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 572912ca82..09ce6bcb7c 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -8274,6 +8274,44 @@ (define-public symfpu (home-page "https://github.com/martin-cs/symfpu") (license license:gpl3)))) +(define-public bitwuzla + (package + (name "bitwuzla") + (version "0.7.0") + (source + (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/bitwuzla/bitwuzla") + (commit version))) + (file-name (git-file-name name version)) + (sha256 + (base32 "1fpd1kgb5xdbcjiqbbc6j0b8g2ly9bp9m3la78fiayl4qlmsvh2b")))) + (build-system meson-build-system) + (arguments + `(#:configure-flags '("-Dtesting=enabled" "-Ddefault_library=shared" + "-Dkissat=true") + #:phases (modify-phases %standard-phases + (add-after 'unpack 'make-git-optional + (lambda _ + (substitute* "src/meson.build" + (("run_command\\('git',") + "run_command('sh', '-c', 'git',"))))))) + (native-inputs (list pkg-config + googletest + python + gmp + cadical + symfpu + kissat)) + (synopsis "SMT solver optimized for the theory of bit-vectors") + (description + "@acronym{SMT, Satisfiability Modulo Theories} solver for the +theories of fixed-size bit-vectors, floating-point arithmetic, arrays, +uninterpreted functions and their combinations.") + (home-page "https://bitwuzla.github.io/") + (license license:expat))) + (define-public z3 (package (name "z3") From unknown Sat Jun 21 12:35:30 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#78246] [PATCH 2/3] gnu: Add symfpu. Resent-From: Liliana Marie Prikler Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 05 May 2025 07:34:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 78246 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: soeren@soeren-tempel.net, 78246@debbugs.gnu.org Received: via spool by 78246-submit@debbugs.gnu.org id=B78246.174643039227360 (code B ref 78246); Mon, 05 May 2025 07:34:01 +0000 Received: (at 78246) by debbugs.gnu.org; 5 May 2025 07:33:12 +0000 Received: from localhost ([127.0.0.1]:38161 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1uBqK7-00077E-Do for submit@debbugs.gnu.org; Mon, 05 May 2025 03:33:11 -0400 Received: from mail-wm1-x344.google.com ([2a00:1450:4864:20::344]:42326) by debbugs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.84_2) (envelope-from ) id 1uBqK4-00076f-NS for 78246@debbugs.gnu.org; Mon, 05 May 2025 03:33:09 -0400 Received: by mail-wm1-x344.google.com with SMTP id 5b1f17b1804b1-43cfa7e7f54so23554295e9.1 for <78246@debbugs.gnu.org>; Mon, 05 May 2025 00:33:08 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1746430381; x=1747035181; darn=debbugs.gnu.org; h=mime-version:user-agent:content-transfer-encoding:references :in-reply-to:date:to:from:subject:message-id:from:to:cc:subject:date :message-id:reply-to; bh=JnpvWQyvaZWmGNB0hh3qoo1ZE4+1nNIvWFL5Iakad1w=; b=meBKJchIbhDQvBUIwzXF0YJL+dkuvrR/lxsJ9e1Azgb6v69U64v2vFtKTzrA4+I2A7 roBs9LARpz4JO+ZXdrCyWNImo0g3lrAVa5YcwffDTBe+DsAVDjbZGbmIkUK+K0GK25vv xtTEaDfUfknww/47ueVmPU+lE425rRHKfAQx857+Gq9yXu9tT47V3VYKlUoNzIn6hPrO lvmkrTV6shq4OP0e0MNvHsaxvWx6iPlxOwe8S5GHHWfDdvcO9Ct10SUyrQyZ/V6kTGQ1 yCsOCtU2h1IRWBoGoGD2A7KaB6lOTX0U6BVp0EiK0hh8CPMDpNBebJfmsVxcCtYQnDcE q5PA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1746430381; x=1747035181; h=mime-version:user-agent:content-transfer-encoding:references :in-reply-to:date:to:from:subject:message-id:x-gm-message-state:from :to:cc:subject:date:message-id:reply-to; bh=JnpvWQyvaZWmGNB0hh3qoo1ZE4+1nNIvWFL5Iakad1w=; b=YD6n0NT3Km3OLlX+dn87JRc6JbIPhbmPkvzIf3X7qoJy7dpGxL1mZI0lER8cLc0gDT tzK1KgAwCjqLt5awTxVbDb3dmU1xTQ8lxF2xAqZ4ECEBK1bRbjdMnr/yfhrKEGacxCrA D8+YPvw5ilFhmro2gsWD0abu8OmeEkwLwx0xNuyBeg6FpMeaS5ZJ0RoBAEW4M0oED6ek mCm2Tuv6gqoycaDwkrHrlckh6n+v5vwX4QZJ5bNR7xLPIkDw2fvGM2R0pPbOGdcLnMIJ dGWiVLfNMvgNffHi0HTAIqfiGxl3GOL6KWvRUIJMI5Qi2fkeb80OMrNfi3N9QZb6ot1z mI8g== X-Forwarded-Encrypted: i=1; AJvYcCWOKia/pXCVEoqNSX8lRwpcEO9vLzHKJf01maBUBiaRvWmKLSPtdEBSat1m/y3EPa13t3pXeg==@debbugs.gnu.org X-Gm-Message-State: AOJu0Yy/enbJGTOTQRySLJTY19vhwGBw2UOMYmo/qmQxdWmfCpwJmeCv zxDt+WgK40wz7hP4JUUGLO0zIXwJC4TO30pH4U479gOCpl1cf9LZOj1qNwqj X-Gm-Gg: ASbGncuxwE/Ua0nrUVLD2Ty3kAc6B10nSeHaHzHv4ENQgVUJF0omKMLId/9NkLrQziD W7zFt+L71Y6pD+4IXCz0ywaYcvIbWPm7h77eTxVPrvItvHPHzl2tpGhrwBm7sJ5/IYFDkiPMyiP vPEZcmZTSY13pS5s+5cmtqVLMBL6yPxmKZ7346QIGFFtxYWxH4A6A7vFI439hkFk+jgvRnOdsPN yN80RRCIsNVnXu4d0RQfEw9iarLygrW1LK17XhOLuoWX8+awhb+sMkL38sEnSKFA92AP/thrsiT sabVW/8VekfRN12O85FXekB10RlVam8DYYed7UDxCilvDhVev5ABoGjrAHDekD26cmCi/eFehQX 5+l9UvGKDgjG0/PID X-Google-Smtp-Source: AGHT+IFKg2mCUIBT+xAYMZzPycOpwNSdTDYX5UiBAd5++6VAHM7b6Xrqq+eTCZCNJhxivVqSZ0rs6w== X-Received: by 2002:a05:600c:528f:b0:43b:c857:e9d7 with SMTP id 5b1f17b1804b1-441bb852744mr92220295e9.5.1746430381054; Mon, 05 May 2025 00:33:01 -0700 (PDT) Received: from lumine.fritz.box (85-127-114-32.dsl.dynamic.surfer.at. [85.127.114.32]) by smtp.gmail.com with ESMTPSA id 5b1f17b1804b1-441b8a3113csm122875375e9.33.2025.05.05.00.32.59 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 05 May 2025 00:32:59 -0700 (PDT) Message-ID: From: Liliana Marie Prikler Date: Mon, 05 May 2025 09:32:58 +0200 In-Reply-To: <75016ee93ed5132c6c3cff0d078e84fdf301b246.1746379841.git.soeren@soeren-tempel.net> References: <75016ee93ed5132c6c3cff0d078e84fdf301b246.1746379841.git.soeren@soeren-tempel.net> Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: base64 User-Agent: Evolution 3.54.3 MIME-Version: 1.0 X-Spam-Score: 0.0 (/) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) QW0gU29ubnRhZywgZGVtIDA0LjA1LjIwMjUgdW0gMTk6NDAgKzAyMDAgc2NocmllYgpzb2VyZW5A c29lcmVuLXRlbXBlbC5uZXQ6Cj4gRnJvbTogU8O2cmVuIFRlbXBlbCA8c29lcmVuQHNvZXJlbi10 ZW1wZWwubmV0Pgo+IAo+ICogZ251L3BhY2thZ2VzL21hdGhzLnNjbSAoc3ltZnB1KTogTmV3IHZh cmlhYmxlLgo+IC0tLQo+IMKgZ251L3BhY2thZ2VzL21hdGhzLnNjbSB8IDU2Cj4gKysrKysrKysr KysrKysrKysrKysrKysrKysrKysrKysrKysrKysrKysrCj4gwqAxIGZpbGUgY2hhbmdlZCwgNTYg aW5zZXJ0aW9ucygrKQo+IAo+IGRpZmYgLS1naXQgYS9nbnUvcGFja2FnZXMvbWF0aHMuc2NtIGIv Z251L3BhY2thZ2VzL21hdGhzLnNjbQo+IGluZGV4IDUzZjcyNmY2MjAuLjU3MjkxMmNhODIgMTAw NjQ0Cj4gLS0tIGEvZ251L3BhY2thZ2VzL21hdGhzLnNjbQo+ICsrKyBiL2dudS9wYWNrYWdlcy9t YXRocy5zY20KPiBAQCAtODIxOCw2ICs4MjE4LDYyIEBAIChkZWZpbmUtcHVibGljIHlpY2VzCj4g wqBzLWV4cHJlc3Npb24tYmFzZWQgZm9ybWF0LiIpCj4gwqDCoMKgIChsaWNlbnNlIGxpY2Vuc2U6 Z3BsMyspKSkKPiDCoAo+ICsoZGVmaW5lLXB1YmxpYyBzeW1mcHUKPiArwqAgKGxldCAoKGNvbW1p dCAiMjJkOTkzZDg4MGY2NmIyZTQ3MGMzOTI4ZTBlNjFiZGY2MTQxOTcwMiIpKQpDb21taXQgYW5k IHJldmlzaW9uIHNob3VsZCBib3RoIGJlIGxldC1ib3VuZC4KPiArwqDCoMKgIChwYWNrYWdlCj4g K8KgwqDCoMKgwqAgKG5hbWUgInN5bWZwdSIpCj4gK8KgwqDCoMKgwqAgKHZlcnNpb24gKGdpdC12 ZXJzaW9uICIyMDIyMDkxMCIgIjAiIGNvbW1pdCkpCldoZW5jZSBjb21ldGggdGhlIGJhc2UgdmVy c2lvbj8KPiArwqDCoMKgwqDCoCAoc291cmNlCj4gK8KgwqDCoMKgwqDCoCAob3JpZ2luCj4gK8Kg wqDCoMKgwqDCoMKgwqAgKG1ldGhvZCBnaXQtZmV0Y2gpCj4gK8KgwqDCoMKgwqDCoMKgwqAgKHVy aSAoZ2l0LXJlZmVyZW5jZQo+ICvCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgICh1cmwgImh0 dHBzOi8vZ2l0aHViLmNvbS9tYXJ0aW4tY3Mvc3ltZnB1IikKPiArwqDCoMKgwqDCoMKgwqDCoMKg wqDCoMKgwqDCoCAoY29tbWl0IGNvbW1pdCkpKQo+ICvCoMKgwqDCoMKgwqDCoMKgIChmaWxlLW5h bWUgKGdpdC1maWxlLW5hbWUgbmFtZSB2ZXJzaW9uKSkKPiArwqDCoMKgwqDCoMKgwqDCoCAoc2hh MjU2Cj4gK8KgwqDCoMKgwqDCoMKgwqDCoCAoYmFzZTMyCj4gIjFoMjB6emt5aTIyNTI5MGtjNm16 ZzhpNGR3a2owcDF2bHdmZ2M5eWNzNjFzbmx5ZDhncjgiKSkpKQo+ICvCoMKgwqDCoMKgIChidWls ZC1zeXN0ZW0gY29weS1idWlsZC1zeXN0ZW0pCj4gK8KgwqDCoMKgwqAgKGFyZ3VtZW50cwo+ICvC oMKgwqDCoMKgwqAgKGxpc3QKPiArwqDCoMKgwqDCoMKgwqAgIzpwaGFzZXMKPiArwqDCoMKgwqDC oMKgwqAgI34obW9kaWZ5LXBoYXNlcyAlc3RhbmRhcmQtcGhhc2VzCj4gK8KgwqDCoMKgwqDCoMKg wqDCoMKgwqAgKGRlbGV0ZSAnY29uZmlndXJlKQo+ICvCoMKgwqDCoMKgwqDCoMKgwqDCoMKgIChy ZXBsYWNlICdpbnN0YWxsCj4gK8KgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgIChsYW1iZGEqICgj OmtleSBvdXRwdXRzICM6YWxsb3ctb3RoZXIta2V5cykKPiArwqDCoMKgwqDCoMKgwqDCoMKgwqDC oMKgwqDCoMKgIChsZXQqICgob3V0ZGlyIChhc3NvYy1yZWYgb3V0cHV0cyAib3V0IikpCj4gK8Kg wqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgIChpbmNkaXIgKHN0cmlu Zy1hcHBlbmQgb3V0ZGlyCj4gIi9pbmNsdWRlL3N5bWZwdSIpKQo+ICvCoMKgwqDCoMKgwqDCoMKg wqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoCAobGliZGlyIChzdHJpbmctYXBwZW5kIG91dGRp ciAiL2xpYiIpKQo+ICsKPiArwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDC oMKgwqAgKGNvcmVkaXIgKHN0cmluZy1hcHBlbmQgaW5jZGlyICIvY29yZSIpKQo+ICvCoMKgwqDC oMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoCAodXRpbHNkaXIgKHN0cmluZy1h cHBlbmQgaW5jZGlyICIvdXRpbHMiKSkpCj4gK8KgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDC oMKgwqAgKG1rZGlyLXAgY29yZWRpcikKPiArwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKg wqDCoCAobWtkaXItcCB1dGlsc2RpcikKPiArwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKg wqDCoCAoY29weS1yZWN1cnNpdmVseSAiY29yZSIgY29yZWRpcikKPiArwqDCoMKgwqDCoMKgwqDC oMKgwqDCoMKgwqDCoMKgwqDCoCAoY29weS1yZWN1cnNpdmVseSAidXRpbHMiIHV0aWxzZGlyKQpU aGlzIHNob3VsZCBiZSBhbiBpbnN0YWxsIHBsYW4uCj4gK8KgwqDCoMKgwqDCoMKgwqDCoMKgwqDC oMKgwqDCoMKgwqAgKG1rZGlyLXAgKHN0cmluZy1hcHBlbmQgbGliZGlyICIvcGtnY29uZmlnIikp Cj4gK8KgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqAgKHdpdGgtb3V0cHV0LXRvLWZp bGUgKHN0cmluZy1hcHBlbmQgbGliZGlyCj4gK8KgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDC oMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKg wqDCoMKgwqDCoMKgwqDCoMKgwqAKPiAiL3BrZ2NvbmZpZy9zeW1mcHUucGMiKQo+ICvCoMKgwqDC oMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoCAobGFtYmRhIF8KPiArwqDCoMKgwqDCoMKg wqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgIChmb3JtYXQgI3QKPiArwqDCoMKgwqDCoMKg wqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqAgInByZWZpeD1+YX5ACj4gK8KgwqDCoMKg wqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqAgZXhlY19wcmVmaXg9JHtwcmVm aXh9fkAKPiArwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoCBp bmNsdWRlZGlyPSR7cHJlZml4fS9pbmNsdWRlfkAKPiArwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKg wqDCoMKgwqDCoMKgwqDCoMKgwqDCoCB+QAo+ICvCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKg wqDCoMKgwqDCoMKgwqDCoMKgIH5ACj4gK8KgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKg wqDCoMKgwqDCoMKgwqAgTmFtZTogc3ltZnB1fkAKPiArwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKg wqDCoMKgwqDCoMKgwqDCoMKgwqDCoCBWZXJzaW9uOiB+YX5ACj4gK8KgwqDCoMKgwqDCoMKgwqDC oMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqAgRGVzY3JpcHRpb246IGxpYnJhcnkgZm9yIElF RUUtNzU0IGZsb2F0c35ACj4gK8KgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKg wqDCoMKgwqAgQ2ZsYWdzOiAtSSR7aW5jbHVkZWRpcn1+JSIKPiArwqDCoMKgwqDCoMKgwqDCoMKg wqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqAgb3V0ZGlyCj4gK8KgwqDCoMKgwqDCoMKgwqDCoMKg wqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgICMkdmVyc2lvbikpKSkpKSkpKQpDb25zaWRlciB3cml0 aW5nIHRoaXMgdG8gdGhlIGN1cnJlbnQgZGlyZWN0b3J5IGFuZCByZWZlcmluZyB0byBpdCBpbgp0 aGUgaW5zdGFsbCBwbGFuLgo+ICvCoMKgwqDCoMKgIChzeW5vcHNpcwo+ICvCoMKgwqDCoMKgwqAg IkNvbmNyZXRlIGFuZCBzeW1ib2xpYyBpbXBsZW1lbnRhdGlvbiBvZiBJRUVFLTc1NCBmbG9hdGlu Zy0KPiBwb2ludCBudW1iZXJzIikKPiArwqDCoMKgwqDCoCAoZGVzY3JpcHRpb24KPiArwqDCoMKg wqDCoMKgICJUaGlzIGxpYnJhcnkgcHJvdmlkZXMgYSBDKysgaW1wbGVtZW50YXRpb24gb2YgY29u Y3JldGUgYW5kCj4gc3ltYm9saWMgc2VtYW50aWNzCj4gK2ZvciBmbG9hdGluZyBwb2ludCBudW1i ZXJzIGFzIGRlZmluZWQgaW4gSUVFRSBTdGFuZGFyZCBmb3IgRmxvYXRpbmctCj4gUG9pbnQgQXJp dGhtZXRpYy4iKQo+ICvCoMKgwqDCoMKgIChob21lLXBhZ2UgImh0dHBzOi8vZ2l0aHViLmNvbS9t YXJ0aW4tY3Mvc3ltZnB1IikKPiArwqDCoMKgwqDCoCAobGljZW5zZSBsaWNlbnNlOmdwbDMpKSkp Cj4gKwpTaG91bGQgcHJvYmFibHkgYmUgZ3BsMysKCgpDaGVlcnMK From unknown Sat Jun 21 12:35:30 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#78246] [PATCH v2] gnu: Add symfpu. Resent-From: soeren@soeren-tempel.net Original-Sender: "Debbugs-submit" Resent-CC: andreas@enge.fr, bavier@posteo.net, sharlatanus@gmail.com, guix-patches@gnu.org Resent-Date: Mon, 05 May 2025 16:41:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 78246 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 78246@debbugs.gnu.org Cc: liliana.prikler@gmail.com, Andreas Enge , Eric Bavier , Sharlatan Hellseher X-Debbugs-Original-Xcc: Andreas Enge , Eric Bavier , Sharlatan Hellseher Received: via spool by 78246-submit@debbugs.gnu.org id=B78246.174646322715675 (code B ref 78246); Mon, 05 May 2025 16:41:02 +0000 Received: (at 78246) by debbugs.gnu.org; 5 May 2025 16:40:27 +0000 Received: from localhost ([127.0.0.1]:42218 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1uByri-00044k-Rs for submit@debbugs.gnu.org; Mon, 05 May 2025 12:40:27 -0400 Received: from magnesium.8pit.net ([45.76.88.171]:14735) by debbugs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.84_2) (envelope-from ) id 1uByrf-00044Q-Kq; Mon, 05 May 2025 12:40:24 -0400 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; s=opensmtpd; bh=ExDgy8zm d9eNoZRGDDrhFSgxR7tHOMnpXNr26jTW07g=; h=references:in-reply-to:date: subject:cc:to:from; d=soeren-tempel.net; b=EzQSyvXCty9YqExuBPibzqnm4Ak x2hiCybFSQ79GJP7PZ0WWj1B693kNcS2GA7Fs/eN41aGF9vJMicY4L9iUpVyWldrvDEXPU GCVGe2vxWnsRsZ3HJLY0xtQqKGZsX8aYwi/CfYSvd/vnYC1RNOOiQWeZGUOhR8yRhyN3ml Q5X8= Received: from localhost ( [2a02:560:4d42:c00:fadc:7b3f:a434:6cdf]) by magnesium.8pit.net (OpenSMTPD) with ESMTPSA id dd61212a (TLSv1.3:TLS_AES_256_GCM_SHA384:256:YES); Mon, 5 May 2025 18:40:21 +0200 (CEST) From: soeren@soeren-tempel.net Date: Mon, 5 May 2025 18:39:30 +0200 Message-ID: X-Mailer: git-send-email 2.49.0 In-Reply-To: References: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-Spam-Score: 0.0 (/) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) From: Sören Tempel * gnu/packages/maths.scm (symfpu): New variable. --- Change since v2: * Make revision let-bound * Fix git-version * Use an install-plan * Change license to gpl3+ gnu/packages/maths.scm | 48 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index eb23a375b4..c139d46fee 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -8218,6 +8218,54 @@ (define-public yices s-expression-based format.") (license license:gpl3+))) +(define-public symfpu + (let ((commit "22d993d880f66b2e470c3928e0e61bdf61419702") + (revision "0")) + (package + (name "symfpu") + (version (git-version "0" revision commit)) + (source + (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/martin-cs/symfpu") + (commit commit))) + (file-name (git-file-name name version)) + (sha256 + (base32 "1h20zzkyi225290kc6mzg8i4dwkj0p1vlwfgc9ycs61snlyd8gr8")))) + (build-system copy-build-system) + (arguments + (list + #:install-plan + #~`(("symfpu.pc" "lib/pkgconfig/symfpu.pc") + ("core" "include/symfpu/core") + ("utils" "include/symfpu/utils")) + #:phases + #~(modify-phases %standard-phases + (add-before 'install 'build-pkgconfig + (lambda* (#:key outputs #:allow-other-keys) + (with-output-to-file "symfpu.pc" + (lambda _ + (format #t + "prefix=~a~@ + exec_prefix=${prefix}~@ + includedir=${prefix}/include~@ + ~@ + ~@ + Name: symfpu~@ + Version: ~a~@ + Description: library for IEEE-754 floats~@ + Cflags: -I${includedir}~%" + (assoc-ref outputs "out") + #$version)))))))) + (synopsis + "Concrete and symbolic implementation of IEEE-754 floating-point numbers") + (description + "This library provides a C++ implementation of concrete and symbolic semantics +for floating point numbers as defined in IEEE Standard for Floating-Point Arithmetic.") + (home-page "https://github.com/martin-cs/symfpu") + (license license:gpl3+)))) + (define-public z3 (package (name "z3") base-commit: 415e3d98d6faf5fd3d1b7b3daa2f20636e4ff822 From unknown Sat Jun 21 12:35:30 2025 MIME-Version: 1.0 X-Mailer: MIME-tools 5.505 (Entity 5.505) X-Loop: help-debbugs@gnu.org From: help-debbugs@gnu.org (GNU bug Tracking System) To: soeren@soeren-tempel.net Subject: bug#78246: closed (Re: [PATCH v2] gnu: Add symfpu.) Message-ID: References: X-Gnu-PR-Message: they-closed 78246 X-Gnu-PR-Package: guix-patches X-Gnu-PR-Keywords: patch Reply-To: 78246@debbugs.gnu.org Date: Wed, 14 May 2025 12:57:07 +0000 Content-Type: multipart/mixed; boundary="----------=_1747227427-1615-1" This is a multi-part message in MIME format... ------------=_1747227427-1615-1 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" Your bug report #78246: [PATCH 0/3] gnu: Add bitwuzla. which was filed against the guix-patches package, has been closed. The explanation is attached below, along with your original report. If you require more details, please reply to 78246@debbugs.gnu.org. --=20 78246: https://debbugs.gnu.org/cgi/bugreport.cgi?bug=3D78246 GNU Bug Tracking System Contact help-debbugs@gnu.org with problems ------------=_1747227427-1615-1 Content-Type: message/rfc822 Content-Disposition: inline Content-Transfer-Encoding: 7bit Received: (at 78246-done) by debbugs.gnu.org; 14 May 2025 12:56:59 +0000 Received: from localhost ([127.0.0.1]:41307 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1uFBfM-0000Oc-Cf for submit@debbugs.gnu.org; Wed, 14 May 2025 08:56:58 -0400 Received: from hera.aquilenet.fr ([185.233.100.1]:48728) by debbugs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.84_2) (envelope-from ) id 1uFBfG-0000N4-OV for 78246-done@debbugs.gnu.org; Wed, 14 May 2025 08:56:51 -0400 Received: from localhost (localhost [127.0.0.1]) by hera.aquilenet.fr (Postfix) with ESMTP id A858C828; Wed, 14 May 2025 14:56:43 +0200 (CEST) X-Virus-Scanned: Debian amavis at hera.aquilenet.fr Received: from hera.aquilenet.fr ([127.0.0.1]) by localhost (hera.aquilenet.fr [127.0.0.1]) (amavis, port 10024) with ESMTP id 4n5YER4pl8z1; Wed, 14 May 2025 14:56:42 +0200 (CEST) Received: from jurong (176-179-191-150.abo.bbox.fr [176.179.191.150]) by hera.aquilenet.fr (Postfix) with ESMTPSA id C9C316E9; Wed, 14 May 2025 14:56:41 +0200 (CEST) Date: Wed, 14 May 2025 14:56:40 +0200 From: Andreas Enge To: soeren@soeren-tempel.net Subject: Re: [PATCH v2] gnu: Add symfpu. Message-ID: References: MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-15 Content-Disposition: inline Content-Transfer-Encoding: 8bit In-Reply-To: X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 78246-done Cc: 78246-done@debbugs.gnu.org, liliana.prikler@gmail.com X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) Hello Sören, thanks a lot for your patch, which I have modified a little bit and pushed. Next time when you send a v2, could you send the complete patch set, even those which have (seemingly) not changed? Here for instance the bitwuzla patch did not apply any more as such, since the context had changed (the previous line from symfpu ended in "gpl3+))))" instead of "gpl3))))"). And I think this will also help QA to apply all patches of the v2. I have also expanded a bit the descriptions and in particular made them full sentences. And added a copyright line for you. For bitwuzla, many of the native-inputs should instead be just regular inputs (rule of thumb: everything that is just needed during the build, such as pkg-config for configuring or googletest for the tests, should be native; when cross-compiling, it is run on the build machine; whereas libraries against which the project is linked should be regular, they will be used during, well, the use of the package). (To be honest, I am not totally sure my split between native and normal inputs is correct; maybe the header only library symfpu should be a native input? I have also removed python as an input; the build works without, and I did not see python related in the output.) I am closing this issue; please feel free to reopen it if something does not work as expected. Andreas ------------=_1747227427-1615-1 Content-Type: message/rfc822 Content-Disposition: inline Content-Transfer-Encoding: 7bit Received: (at submit) by debbugs.gnu.org; 4 May 2025 17:38:04 +0000 Received: from localhost ([127.0.0.1]:59082 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1uBdHs-0002s0-1o for submit@debbugs.gnu.org; Sun, 04 May 2025 13:38:02 -0400 Received: from lists.gnu.org ([2001:470:142::17]:52130) by debbugs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.84_2) (envelope-from ) id 1uBdHn-0002qx-Hf for submit@debbugs.gnu.org; Sun, 04 May 2025 13:37:56 -0400 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 1uBdHf-0005T3-Rt for guix-patches@gnu.org; Sun, 04 May 2025 13:37:48 -0400 Received: from magnesium.8pit.net ([45.76.88.171]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1uBdHd-0002KO-NR; Sun, 04 May 2025 13:37:47 -0400 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; s=opensmtpd; bh=1c84fXON Wz3jindO7qBjHtzfDm2+ay9HShSy07rdQ0U=; h=date:subject:cc:to:from; d=soeren-tempel.net; b=wUvnWvtbHWfnLn0mZeEWKG36/MlgysDo4gvHQe2LUf1Coiu RqT82Uwb1jer4X+38KGlmNcqCMYg3fTdd66XksM0OErciBGeQ/MMyjN5hK3D2pLI0Zo+9l T+h3LmjCRvGllTX2KMsF9xyoSrxisnsAWnzMl+HgRxeBqhtH4pli1U= Received: from localhost ( [2a02:560:4d21:3f00:4392:0:6418:52]) by magnesium.8pit.net (OpenSMTPD) with ESMTPSA id 6bffdadd (TLSv1.3:TLS_AES_256_GCM_SHA384:256:YES); Sun, 4 May 2025 19:37:40 +0200 (CEST) From: soeren@soeren-tempel.net To: guix-patches@gnu.org Subject: [PATCH 0/3] gnu: Add bitwuzla. Date: Sun, 4 May 2025 19:34:41 +0200 Message-ID: X-Mailer: git-send-email 2.49.0 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 X-Debbugs-Cc: Andreas Enge , Eric Bavier , Sharlatan Hellseher Content-Transfer-Encoding: 8bit Received-SPF: pass client-ip=45.76.88.171; envelope-from=soeren@soeren-tempel.net; helo=magnesium.8pit.net X-Spam_score_int: -20 X-Spam_score: -2.1 X-Spam_bar: -- X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, RCVD_IN_VALIDITY_RPBL_BLOCKED=0.001, RCVD_IN_VALIDITY_SAFE_BLOCKED=0.001, SPF_HELO_NONE=0.001, SPF_PASS=-0.001 autolearn=ham autolearn_force=no X-Spam_action: no action X-Spam-Score: 0.9 (/) X-Debbugs-Envelope-To: submit Cc: liliana.prikler@gmail.com X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.1 (/) From: Sören Tempel This patchsets adds bitwuzla an SMT solver which is especially efficent for bitvector theory and can be used with the already packaged BINSEC symbolic executor. While packaging bitwuzla, I also noticed and fixed a bug regarding the installed header files for cadical (CC: liliana.prikler@) and added a package for symfpu, which is a dependency of bitwuzla. Sören Tempel (3): gnu: cadical: also install C++ header file to /usr/include gnu: Add symfpu. gnu: Add bitwuzla. gnu/packages/maths.scm | 96 +++++++++++++++++++++++++++++++++++++++++- 1 file changed, 95 insertions(+), 1 deletion(-) base-commit: 415e3d98d6faf5fd3d1b7b3daa2f20636e4ff822 ------------=_1747227427-1615-1--