From debbugs-submit-bounces@debbugs.gnu.org Sun Sep 29 05:19:01 2024 Received: (at submit) by debbugs.gnu.org; 29 Sep 2024 09:19:05 +0000 Received: from localhost ([127.0.0.1]:40039 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1suq4d-0005Gv-PA for submit@debbugs.gnu.org; Sun, 29 Sep 2024 05:18:59 -0400 Received: from lists.gnu.org ([209.51.188.17]:51012) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1suq4N-0005D5-87 for submit@debbugs.gnu.org; Sun, 29 Sep 2024 05:18:30 -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 1suq3r-0007ry-Fh for guix-patches@gnu.org; Sun, 29 Sep 2024 05:17:51 -0400 Received: from mail-ej1-x642.google.com ([2a00:1450:4864:20::642]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1suq3p-0002a0-Tl for guix-patches@gnu.org; Sun, 29 Sep 2024 05:17:51 -0400 Received: by mail-ej1-x642.google.com with SMTP id a640c23a62f3a-a8d51a7d6f5so443724266b.2 for ; Sun, 29 Sep 2024 02:17:49 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1727601468; x=1728206268; darn=gnu.org; h=mime-version:to:subject:date:from:message-id:from:to:cc:subject :date:message-id:reply-to; bh=TIF+XV6S25xDqBnIQX99n2Jawai2Y99HpqBgqZY3rVo=; b=MOmlhCZdg7xbD8XuRXiMvV/U9SFf4NOdRTDKdsgEeS6myQ8DJbxKs6ROC027csv85M xlJ4CItvFyUkESz9YP2E8iwLm2ettVpcCHdXBzIl2dszwn9+yWNNeEQppszHDgtnI+F7 tupNWiGsvDI167ARcNDSiCF3XIESDZ6oA2dOaCXQL07F1/gYCOOZy/8B+/LsyGGRhs/q O5N+1UZJxIRvG/Xr6LMkpqa020PrkhuQ/58IE/iIGOjDcoaIb4EKrCUy4Pej7d1ZIma1 aWzlgivKYZkHJpH5Eu5280CGdJFrfZL3dDixDDkfq1coramjjSwiQWwp1wlsjWGfc4qr +95g== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1727601468; x=1728206268; h=mime-version:to:subject:date:from:message-id:x-gm-message-state :from:to:cc:subject:date:message-id:reply-to; bh=TIF+XV6S25xDqBnIQX99n2Jawai2Y99HpqBgqZY3rVo=; b=lHQTbfIM+eu+R+jRBDgxGdJTR+IyWUMjhtfKCqJu40QBIJsWrsRKagNq6Z6sicFcsD c3G3gbUbh0kxd/F2kD6+bKhLK7SfjxL17I6svuTWPIFNQAPD/SAbnwk3D/9lOQTcF5ES kRnOyV/nEwi6DuRtiO6S65R3Z6ajVafsJFPWGITzHQqrP68SqVAGG5tT62x2E43pKsH/ BeX3txBhcunq6Xg+yriSht5dPHZC3l+BLXUkY9dGsqMC76oz4saUZsCBKGPaDmWIOc28 5p17QSI2Pp9tsi0H+z3YMY0LmKWGN76CXVinHaqEO9IOp6g031dsbK6AR9VCllECZGS8 ezpA== X-Gm-Message-State: AOJu0YxfAExkYsF/J2k8tF9ci8NIrR1fHECmcdirfva2fDpnE9Pum1qA kE48TMsmlBJ5euZDVWOJeF973ivNgHWmfW/GpgcOMrS0Aw7YYnlhJR3GIiqq X-Google-Smtp-Source: AGHT+IHQSFCA9heN0r0XF2h9tiMo0ieXUdo1pQFtATUTdyQ5i7qulKaKvVPqdMzKFXPRh0uyeOllPw== X-Received: by 2002:a17:907:1c29:b0:a8e:a578:2b63 with SMTP id a640c23a62f3a-a93c4aeb94cmr835582966b.55.1727601467755; Sun, 29 Sep 2024 02:17:47 -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 a640c23a62f3a-a93c297bceesm349394666b.187.2024.09.29.02.17.46 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sun, 29 Sep 2024 02:17:47 -0700 (PDT) Message-ID: From: Liliana Marie Prikler Date: Sun, 29 Sep 2024 11:16:38 +0200 Subject: [PATCH 0/8] Update some SAT/ASP solvers to: guix-patches@gnu.org MIME-Version: 1.0 Received-SPF: pass client-ip=2a00:1450:4864:20::642; envelope-from=liliana.prikler@gmail.com; helo=mail-ej1-x642.google.com X-Spam_score_int: 2 X-Spam_score: 0.2 X-Spam_bar: / X-Spam_report: (0.2 / 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, FREEMAIL_FROM=0.001, MALFORMED_FREEMAIL=2.279, SPF_HELO_NONE=0.001, SPF_PASS=-0.001 autolearn=no autolearn_force=no X-Spam_action: no action X-Spam-Score: 0.9 (/) X-Debbugs-Envelope-To: submit 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 (/) 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 From debbugs-submit-bounces@debbugs.gnu.org Sun Sep 29 05:34:47 2024 Received: (at 73551) by debbugs.gnu.org; 29 Sep 2024 09:34:47 +0000 Received: from localhost ([127.0.0.1]:40090 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1suqKE-00015y-K1 for submit@debbugs.gnu.org; Sun, 29 Sep 2024 05:34:47 -0400 Received: from mail-lf1-f65.google.com ([209.85.167.65]:54403) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1suqKC-00015Y-EL for 73551@debbugs.gnu.org; Sun, 29 Sep 2024 05:34:45 -0400 Received: by mail-lf1-f65.google.com with SMTP id 2adb3069b0e04-53988c54ec8so2075588e87.0 for <73551@debbugs.gnu.org>; Sun, 29 Sep 2024 02:34:13 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1727602387; x=1728207187; darn=debbugs.gnu.org; h=mime-version:to:subject:date:from:references:in-reply-to:message-id :from:to:cc:subject:date:message-id:reply-to; bh=m+h0a5oiaUVA92u0kakaAKM7XEgHL/dCQALfSYIF5EA=; b=TtK+FS2vqLvi+GLOutkdKyLfuJNHr2B+bqQOUwtpSQzTuSJ4dD7PcLBRj4erVPd69k FXoYU+5OJieNLC2PZF2/p3RmT7s+X0gjKWsgFypL7ZCKTqxywNorvbzOFWh+kuK5DrEl dWNXJYL6nm5dsBgtQ+0tTElPbz8aXo1u7PAZewnhTSFusVnM+b7e5Ts3rn2SQl3GS+6c 6U1QC7U/sDA24YsOUDkXBJzKjltSizWtQjjbpP8XOArVMA7DHULBKGWRoPoM2xiy7WwT FvPpSzv9grMsu11pyp1ItQqVW8ApuVMIte0gUcjaUHavYC/ePPOSl+BNzyArPVVp7ggC mmzQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1727602387; x=1728207187; h=mime-version:to:subject:date:from:references:in-reply-to:message-id :x-gm-message-state:from:to:cc:subject:date:message-id:reply-to; bh=m+h0a5oiaUVA92u0kakaAKM7XEgHL/dCQALfSYIF5EA=; b=EW1bApsVdaz3ijZHHaBDasTJntvhHV0R0XMCmp3nxdYVyII3VxxydhYqmSOSwdCQXq 53IGwz8mASAxxwGaaBmck5n3YOnKiK6rG6GJ5rP3i2m10dPiXbHXNgVXWOY3N/pwSH6u IupHnzVGKg4Dgct9xSn16jpNVk+MYgOyDTkZ331EHmSzGhhtKcYqRCkFbkiAWq2FgeCm Nu8T02phFhVrFNC9ljfmRVrsn23uLN5/d5gAJnebvn2VMz2QCmcAKyG0YbJ/cCJrCLl1 OFCq/IhSNM5A26SEW7hS/GeVdr4BR0kVapbmznMUUhVmQBevPm5A0uuYAiHZfMw6lW3L 9hoQ== X-Gm-Message-State: AOJu0YxOWg3lTECvSbjl+KbivT+SSSe+NP8bhlU95X6Wxcc4Y5pq7AGO BPgkFekaGITbapYbNiBkdrw3QwF+SjnOWvNU88bCOExUnOVNRhB0dHEiAyDP X-Google-Smtp-Source: AGHT+IHGWeaf6lFhkdGKMfqYaIH6WyHGV2iMxpDAGQtOeSW2n18OX4yekB464H/xdsD5wr1vAsHRTA== X-Received: by 2002:a17:907:1c24:b0:a8a:9246:7f57 with SMTP id a640c23a62f3a-a93c48e8e14mr980661266b.4.1727601868338; Sun, 29 Sep 2024 02:24:28 -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 4fb4d7f45d1cf-5c88248af7dsm2997166a12.78.2024.09.29.02.24.27 for <73551@debbugs.gnu.org> (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sun, 29 Sep 2024 02:24:28 -0700 (PDT) Message-ID: <81e078aa4164ee1b92dfdb9f855c025230444d7a.1727601398.git.liliana.prikler@gmail.com> In-Reply-To: References: From: Liliana Marie Prikler Date: Sun, 29 Sep 2024 11:00:56 +0200 Subject: [PATCH 5/8] gnu: Add cadical. to: 73551@debbugs.gnu.org MIME-Version: 1.0 X-Spam-Score: 1.4 (+) 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: * 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/pack [...] Content analysis details: (1.4 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 0.0 SPF_HELO_NONE SPF: HELO does not publish an SPF Record 0.0 FREEMAIL_FROM Sender email is commonly abused enduser mail provider (liliana.prikler[at]gmail.com) -0.0 SPF_PASS SPF: sender matches SPF record 0.0 RCVD_IN_VALIDITY_CERTIFIED_BLOCKED RBL: ADMINISTRATOR NOTICE: The query to Validity was blocked. See https://knowledge.validity.com/hc/en-us/articles/20961730681243 for more information. [209.85.167.65 listed in sa-accredit.habeas.com] 0.0 RCVD_IN_VALIDITY_RPBL_BLOCKED RBL: ADMINISTRATOR NOTICE: The query to Validity was blocked. See https://knowledge.validity.com/hc/en-us/articles/20961730681243 for more information. [209.85.167.65 listed in bl.score.senderscore.com] -0.9 RCVD_IN_MSPIKE_H2 RBL: Average reputation (+2) [209.85.167.65 listed in wl.mailspike.net] 2.3 MALFORMED_FREEMAIL Bad headers on message from free email service X-Debbugs-Envelope-To: 73551 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.4 (/) * 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 +Date: Sun, 2 Jun 2024 21:50:06 -0400 +Subject: [PATCH] Also add a dynamic library + +--- +Liliana Marie Prikler : + 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 From debbugs-submit-bounces@debbugs.gnu.org Sun Sep 29 05:35:07 2024 Received: (at 73551) by debbugs.gnu.org; 29 Sep 2024 09:35:07 +0000 Received: from localhost ([127.0.0.1]:40094 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1suqKZ-000172-7Q for submit@debbugs.gnu.org; Sun, 29 Sep 2024 05:35:07 -0400 Received: from mail-ed1-f65.google.com ([209.85.208.65]:45486) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1suqKX-00016L-Gc for 73551@debbugs.gnu.org; Sun, 29 Sep 2024 05:35:05 -0400 Received: by mail-ed1-f65.google.com with SMTP id 4fb4d7f45d1cf-5c88b5c375fso1376516a12.3 for <73551@debbugs.gnu.org>; Sun, 29 Sep 2024 02:34:34 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1727602409; x=1728207209; darn=debbugs.gnu.org; h=mime-version:to:subject:date:from:references:in-reply-to:message-id :from:to:cc:subject:date:message-id:reply-to; bh=CqpF57WScORd6air2hU/l7hTYqFGxCAOMjXajdSw2E4=; b=PdMeZlVXkcoI1E1qf1k+d4NAnIJE47difew8bEVqRNhyoAqXWZ+7AZHt41Mu6CHFly v9tZ7WmlDYRRbT/2xS+wiutJCDF0iqWn2nTV+ZBPtdFry+ajImZLl5DY+rSPQAl9ien2 VjkrONr8cAB36euSO2lYyTICr7TRMcpAoT5bvR8FU7yKgQqFHhXTohsW9D1sXHiHBvji RHdfi/8i1ZlBlaDOhWljG4DV39jpg3ZT7oz9zGNQLRcwsXUdWl3b1+SmxqIaeySFqXuK wTsLFHtVYb+eWTx/J0jAJ2KAUeERB8ze2VjmuoU069wzIYW0jGhB3pPbVInesFwPK6kF ZRAg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1727602409; x=1728207209; h=mime-version:to:subject:date:from:references:in-reply-to:message-id :x-gm-message-state:from:to:cc:subject:date:message-id:reply-to; bh=CqpF57WScORd6air2hU/l7hTYqFGxCAOMjXajdSw2E4=; b=iEN8Kf+T98PWfySKB5nxHPVjypJeGXK4jej5xBFbM6x4GDZdZ76+nUG+N2yjBZU/Vv zFHNL9v6G883+8h1O95A3QWTKDJ6VEeG+GJDM74NH1kiqOq7DFEs17GMGVEjqiTdaMFj neunh3PV93Yh6mlW7J7uGoJbOD+EtUjudaEkOm1KJkHHAxbHib7AVbGVUmrOh6VogPcK ++bLOLEyuJo6iBkiXyoRxy+lMSWJj2kZXg6K87Z/LgLK4P/hFApVkejlg5NOrFsI/rrW QVryQfgT6ULbV+rkq49qP21RQgZ60kpUMWayv+hs38e27NiwvPmq1NorT/dFOjP94V6c 9YXQ== X-Gm-Message-State: AOJu0YxL0m99dC1vqNIEA8Lqins3QyEuAFDj7w+u0gG4LJOdWvp9EdqO 87/9xFFx+c8KQj/2aFFUsyho77Ku9RcFOPtIzSDB49C3GXhFYun8zsm45Kk2 X-Google-Smtp-Source: AGHT+IGLOHeBABSY1THuu3hw8O3oc0BSxqMzrBPGEXK/Du/FRmMgjpo6AyC69whCXC1QqrJfleA5Rw== X-Received: by 2002:a17:907:ea7:b0:a8a:8c92:1c76 with SMTP id a640c23a62f3a-a93c4961721mr835870566b.36.1727601870394; Sun, 29 Sep 2024 02:24:30 -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 4fb4d7f45d1cf-5c88248af7dsm2997166a12.78.2024.09.29.02.24.29 for <73551@debbugs.gnu.org> (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sun, 29 Sep 2024 02:24:30 -0700 (PDT) Message-ID: In-Reply-To: References: From: Liliana Marie Prikler Date: Sun, 29 Sep 2024 11:08:20 +0200 Subject: [PATCH 8/8] gnu: cryptominisat: Update to 5.11.22. to: 73551@debbugs.gnu.org MIME-Version: 1.0 X-Spam-Score: 1.4 (+) 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: * 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 ++++++++++ [...] Content analysis details: (1.4 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 0.0 RCVD_IN_VALIDITY_RPBL_BLOCKED RBL: ADMINISTRATOR NOTICE: The query to Validity was blocked. See https://knowledge.validity.com/hc/en-us/articles/20961730681243 for more information. [209.85.208.65 listed in bl.score.senderscore.com] 0.0 RCVD_IN_VALIDITY_CERTIFIED_BLOCKED RBL: ADMINISTRATOR NOTICE: The query to Validity was blocked. See https://knowledge.validity.com/hc/en-us/articles/20961730681243 for more information. [209.85.208.65 listed in sa-accredit.habeas.com] 0.0 SPF_HELO_NONE SPF: HELO does not publish an SPF Record 0.0 FREEMAIL_FROM Sender email is commonly abused enduser mail provider (liliana.prikler[at]gmail.com) -0.0 SPF_PASS SPF: sender matches SPF record -0.9 RCVD_IN_MSPIKE_H2 RBL: Average reputation (+2) [209.85.208.65 listed in wl.mailspike.net] 2.3 MALFORMED_FREEMAIL Bad headers on message from free email service X-Debbugs-Envelope-To: 73551 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.4 (/) * 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\"") "")))))) (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 From debbugs-submit-bounces@debbugs.gnu.org Sun Sep 29 05:36:18 2024 Received: (at 73551) by debbugs.gnu.org; 29 Sep 2024 09:36:19 +0000 Received: from localhost ([127.0.0.1]:40098 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1suqLi-0001I3-Jw for submit@debbugs.gnu.org; Sun, 29 Sep 2024 05:36:18 -0400 Received: from mail-lj1-f196.google.com ([209.85.208.196]:47327) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1suqLf-0001Hn-Na for 73551@debbugs.gnu.org; Sun, 29 Sep 2024 05:36:16 -0400 Received: by mail-lj1-f196.google.com with SMTP id 38308e7fff4ca-2fa10e64805so22764271fa.2 for <73551@debbugs.gnu.org>; Sun, 29 Sep 2024 02:35:44 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1727602479; x=1728207279; darn=debbugs.gnu.org; h=mime-version:to:subject:date:from:references:in-reply-to:message-id :from:to:cc:subject:date:message-id:reply-to; bh=jx2qbQydocJq4yBkaxkeqGfyJGxPkffobRSIL2fUoFo=; b=l0b6RwGor7EgB2tzKUtu7vmg8jecz75bYvV3hQUgwZYf/9TarfPX7ujF9SadJaDUUn bIzuqca4bbqiIwp9WG7eSkjdlkyALr7poy9PBjbxDgIxgcOHfAP6tk2VnfI+WXix7zTz M7JF7yJB5vyfNBN1xvf3XGH3CqhN5kSJdOsdOB8+D4QgC2YKJ0vsooK+4T2FdqYu2lPE uR80/DDtjkoStSA9qf2sI1EDO9h7qstto93NVwk4IZeWHixU9JNWvRLrAOeVxxz+CIBB M/Bl+YJtaLc1oIg5JKN5oLf521S0Z5B/evIP394X3KzAo/Vqxnm8VKoH3/H0YXfPP17W EDSg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1727602479; x=1728207279; h=mime-version:to:subject:date:from:references:in-reply-to:message-id :x-gm-message-state:from:to:cc:subject:date:message-id:reply-to; bh=jx2qbQydocJq4yBkaxkeqGfyJGxPkffobRSIL2fUoFo=; b=Vw2VIA/u9erFH40Q5NDHw7FSDygzUTRTb4FoN0wD+aylw+9+jatDE2b51Uar6G7frE pF3n32blQe+K5pqg/77rob0fgxNDE2hjaiBYainM+riqkAvrPNUH34dMVzUULEECJKi5 kkP8Rzu+YL5wP4dJxtGWOVyw4N30swoMBV25GyOqJelkiXJzQHlP5j0KBHp7xka69AyH gNnMEKXY/TSspPnLSK+XXK9DWeT4PXxMN5S5qQPFV3SPdziKv7mry2OZcEV07pg3y/Ll EcGov7N+BcH23WccvDP8bH/iE9NtsIF09K83LNXEHVYbNewlD+zRwGnr8HyaR5XTw2/H BZGg== X-Gm-Message-State: AOJu0Yzyq+awFCS24kR9KQCDmn5MG+zz21kNCn2Yp+PqiCLXfD8N3APi Fsvn3Z3EX9AmY0qjFqCMR+dm46tDIgB04FVsXsbQhY/XdbghAkvbbOQb2TAV X-Google-Smtp-Source: AGHT+IFVRI57Kux0f2bOfoDwlBXXatwYbY8jnDLag60j4e/3ZwuydRuhWFDFRy+Ro0Lm68dFxAyLRg== X-Received: by 2002:a05:6402:5213:b0:5c8:8fe7:73a8 with SMTP id 4fb4d7f45d1cf-5c88fe774bdmr1760820a12.7.1727601869679; Sun, 29 Sep 2024 02:24:29 -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 4fb4d7f45d1cf-5c88248af7dsm2997166a12.78.2024.09.29.02.24.29 for <73551@debbugs.gnu.org> (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sun, 29 Sep 2024 02:24:29 -0700 (PDT) Message-ID: In-Reply-To: References: From: Liliana Marie Prikler Date: Sun, 29 Sep 2024 11:04:20 +0200 Subject: [PATCH 7/8] gnu: Add cadiback-for-cryptominisat. to: 73551@debbugs.gnu.org MIME-Version: 1.0 X-Spam-Score: 1.4 (+) 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: * 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 cadibac [...] Content analysis details: (1.4 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 0.0 RCVD_IN_VALIDITY_RPBL_BLOCKED RBL: ADMINISTRATOR NOTICE: The query to Validity was blocked. See https://knowledge.validity.com/hc/en-us/articles/20961730681243 for more information. [209.85.208.196 listed in bl.score.senderscore.com] 0.0 RCVD_IN_VALIDITY_CERTIFIED_BLOCKED RBL: ADMINISTRATOR NOTICE: The query to Validity was blocked. See https://knowledge.validity.com/hc/en-us/articles/20961730681243 for more information. [209.85.208.196 listed in sa-accredit.habeas.com] 0.0 SPF_HELO_NONE SPF: HELO does not publish an SPF Record 0.0 FREEMAIL_FROM Sender email is commonly abused enduser mail provider (liliana.prikler[at]gmail.com) -0.0 SPF_PASS SPF: sender matches SPF record -0.9 RCVD_IN_MSPIKE_H2 RBL: Average reputation (+2) [209.85.208.196 listed in wl.mailspike.net] 2.3 MALFORMED_FREEMAIL Bad headers on message from free email service X-Debbugs-Envelope-To: 73551 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.4 (/) * 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 From debbugs-submit-bounces@debbugs.gnu.org Sun Sep 29 05:37:11 2024 Received: (at 73551) by debbugs.gnu.org; 29 Sep 2024 09:37:11 +0000 Received: from localhost ([127.0.0.1]:40102 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1suqMZ-0001Jl-1s for submit@debbugs.gnu.org; Sun, 29 Sep 2024 05:37:11 -0400 Received: from mail-ed1-f65.google.com ([209.85.208.65]:59478) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1suqMX-0001JW-Ab for 73551@debbugs.gnu.org; Sun, 29 Sep 2024 05:37:09 -0400 Received: by mail-ed1-f65.google.com with SMTP id 4fb4d7f45d1cf-5c896b9b3e1so230846a12.2 for <73551@debbugs.gnu.org>; Sun, 29 Sep 2024 02:36:38 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1727602532; x=1728207332; darn=debbugs.gnu.org; h=mime-version:to:subject:date:from:references:in-reply-to:message-id :from:to:cc:subject:date:message-id:reply-to; bh=z3DdpWeiDJeXgzvVE53j1vNopNyJe9Gb0YhqyI08F0o=; b=T0UeUTLFLBBj6qg6T0QhQNySQWgL7YB7gj2cxcfTybM4Q5FVqYS+FHhFGriMOKZcq0 42o6azc2rv7ZAHHjGSwF85lcQKKhJf5BRU0rcj6W9rq+qHlcLfzHfjHiSkMaI2Uy6tR6 7YeUKpvM5ohnYGeWsxzI2XVVpIGIx9oNsASNxNotnzOuJuH/TyqVRmz7vsmmmfMyZjEa SLTnGWC7tGhQl2b2nRvHg7oF477VgBZ3WLJjbCHR+0ZbnYYeKMIEJHvqCphrBgcKJBKS gtDTfSoXDmM8VlA14ua8U6L6rBJFyVeVvlCg7OTCTGjuVwpO04Tn4haJNk7VxaBks+Vh Ygvw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1727602532; x=1728207332; h=mime-version:to:subject:date:from:references:in-reply-to:message-id :x-gm-message-state:from:to:cc:subject:date:message-id:reply-to; bh=z3DdpWeiDJeXgzvVE53j1vNopNyJe9Gb0YhqyI08F0o=; b=h8aSFaoK76mNTTDYoz+KhMkrGdpZT+hvpHw9NYGf96ito/f7GuyW9oSN4/uagPUrXN vaQ6ThoxqCy7uXmcL2fIL5Zc5/DcVORD/WSC+rO+4jam66qj3we4bu7ifQOdTcMTwLfM aq6b4Hg2b25U6s1oyq8ZYBxVtMj2xAbveDAP+FlTvm7Kw8xtU7lcccCpulVDRWQB+XkV cBC7wdoCdWvqZOi1/uXR28T8bpTrEKQ9p76b//ARG8LMxxG4Q5fO2onH7IZ8qj0PE0F0 406Xbd82MmKaR3peDGuSRiSJRg2qlNwVcfnomnMgB2zIF7YsWGVVwWSLaTbZJ2oQdaG0 YbHA== X-Gm-Message-State: AOJu0YzjZu6TBW2kd55JIbTMSU4lUgVMdD7SjreDG1Z/e7TnXrzKdgX+ HVYQSaU+XfzxoZ7aSsd38rxPaq5NdpHwyOd1fuQOHxsQ+ti4zFyLyairfW9E X-Google-Smtp-Source: AGHT+IHreKF4XugyvixxgxW2uii/29MNFr5wEkZdzuPKpnGuRShFZrRH0Z4tXGmMJz08gmq1OH0nrA== X-Received: by 2002:a05:6402:3813:b0:5c5:c0ef:282c with SMTP id 4fb4d7f45d1cf-5c8824d5f37mr8488796a12.11.1727601869039; Sun, 29 Sep 2024 02:24:29 -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 4fb4d7f45d1cf-5c88248af7dsm2997166a12.78.2024.09.29.02.24.28 for <73551@debbugs.gnu.org> (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sun, 29 Sep 2024 02:24:28 -0700 (PDT) Message-ID: <9189bcfc8795d725133fb5ca6eedb24a3090ccba.1727601398.git.liliana.prikler@gmail.com> In-Reply-To: References: From: Liliana Marie Prikler Date: Sun, 29 Sep 2024 11:04:12 +0200 Subject: [PATCH 6/8] gnu: Add cadiback. to: 73551@debbugs.gnu.org MIME-Version: 1.0 X-Spam-Score: 1.4 (+) 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: * 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 [...] Content analysis details: (1.4 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 0.0 RCVD_IN_VALIDITY_RPBL_BLOCKED RBL: ADMINISTRATOR NOTICE: The query to Validity was blocked. See https://knowledge.validity.com/hc/en-us/articles/20961730681243 for more information. [209.85.208.65 listed in bl.score.senderscore.com] 0.0 RCVD_IN_VALIDITY_CERTIFIED_BLOCKED RBL: ADMINISTRATOR NOTICE: The query to Validity was blocked. See https://knowledge.validity.com/hc/en-us/articles/20961730681243 for more information. [209.85.208.65 listed in sa-accredit.habeas.com] 0.0 SPF_HELO_NONE SPF: HELO does not publish an SPF Record 0.0 FREEMAIL_FROM Sender email is commonly abused enduser mail provider (liliana.prikler[at]gmail.com) -0.0 SPF_PASS SPF: sender matches SPF record -0.9 RCVD_IN_MSPIKE_H2 RBL: Average reputation (+2) [209.85.208.65 listed in wl.mailspike.net] 2.3 MALFORMED_FREEMAIL Bad headers on message from free email service X-Debbugs-Envelope-To: 73551 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.4 (/) * 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 From debbugs-submit-bounces@debbugs.gnu.org Sun Sep 29 05:40:21 2024 Received: (at 73551) by debbugs.gnu.org; 29 Sep 2024 09:40:21 +0000 Received: from localhost ([127.0.0.1]:40108 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1suqPd-0001ZZ-7t for submit@debbugs.gnu.org; Sun, 29 Sep 2024 05:40:21 -0400 Received: from mail-ed1-f68.google.com ([209.85.208.68]:45157) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1suqBm-0007w1-Mx for 73551@debbugs.gnu.org; Sun, 29 Sep 2024 05:26:37 -0400 Received: by mail-ed1-f68.google.com with SMTP id 4fb4d7f45d1cf-5c42f406e29so4652028a12.2 for <73551@debbugs.gnu.org>; Sun, 29 Sep 2024 02:25:31 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1727601866; x=1728206666; darn=debbugs.gnu.org; h=mime-version:to:subject:date:from:references:in-reply-to:message-id :from:to:cc:subject:date:message-id:reply-to; bh=w+DIRckBnCth68kAjKBZduilsNkYX+P+2gwWR5qJuBE=; b=bN7D/9V4FmiTHVpodSPmV1wnlV7nwwIJBeuYPDP0rvwtdOXk/OPOQzSmvMNZ7KMTBI IjEsnhSdoQRaaTpk44k+XuUnRFrKxFoDgRpmmyVOw1oMXpUgkqml8C6HnCF0fM8NRg95 xKeAYrOiI9Oc1Z0Ld5qAHcw8wrKzqJrp522QjCyO1+MxO/yRkyXH0eMj8+AfZxYmWomV FYERqa7az7ltPy5IebnHLEDEnkEyAD8YhXwHJ1gJGOw+5OOmdxSr6kEdqPOp83xqbfUC /pOXlEp3zGzF0XSnSo5MXrlRiJDKeGFpQJ+swYra4fv9b/DcIUYn7TSMZsiunD0lkpxi AQKg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1727601866; x=1728206666; h=mime-version:to:subject:date:from:references:in-reply-to:message-id :x-gm-message-state:from:to:cc:subject:date:message-id:reply-to; bh=w+DIRckBnCth68kAjKBZduilsNkYX+P+2gwWR5qJuBE=; b=aMKUUeWpJsppx/mIb7czUmnUkxVw4jSF1gL9y3MWvY43CHyrz6ilcxBg67/f8fLk/Z 9MA1uAxg6SfKQuG5rY17C87Iex27xaxv/bWnyObOKCWnYeaLPviMVRcqLnJzKwg5jD69 dqd62sk4Hh7uoem3myQ/Ve2VdYlIgVWtgtP893pCH5IfRXAzrgUdFA81G+B+TyMYy+uu n7aiIdN2MVtL1CShlvPhN/eW4Zczep3F3jm1yFObnntDmYpNB0i5/Z7SDXTPzNOV2RdI J8+X/rTc34ZtFvDWVqHRtk126t2GeGLWVCn1uTACWT74EKEFOoa+2VH9/YofwGNOBrEi P0nA== X-Gm-Message-State: AOJu0YzuxcWjneCnqIJzFC/NrCGds+2/V1ynWcjJWvGW7MbC67LbyULz roiFHjlZfNxWaXEYf5PyPlxJdEQJvn5tpA8Q4TSeaHA7wEwX/mS1JcHe/wJ1 X-Google-Smtp-Source: AGHT+IHLYUI9tkxVi1cAJuChvjSUy8lwXy+zC7v0r3hhFMB/K4PPbHQIzGnkbjqpVjbKvRcCS/wSUg== X-Received: by 2002:a05:6402:371b:b0:5c4:a62:e1f1 with SMTP id 4fb4d7f45d1cf-5c882603c1amr7011433a12.29.1727601865636; Sun, 29 Sep 2024 02:24:25 -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 4fb4d7f45d1cf-5c88248af7dsm2997166a12.78.2024.09.29.02.24.24 for <73551@debbugs.gnu.org> (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sun, 29 Sep 2024 02:24:25 -0700 (PDT) Message-ID: In-Reply-To: References: From: Liliana Marie Prikler Date: Wed, 25 Sep 2024 21:03:25 +0200 Subject: [PATCH 2/8] gnu: kissat: Update to 4.0.1. to: 73551@debbugs.gnu.org MIME-Version: 1.0 X-Spam-Score: 2.2 (++) 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: * gnu/packages/maths.scm (kissat): Update to 4.0.1. [#:phases]: 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 [...] Content analysis details: (2.2 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 0.0 RCVD_IN_VALIDITY_CERTIFIED_BLOCKED RBL: ADMINISTRATOR NOTICE: The query to Validity was blocked. See https://knowledge.validity.com/hc/en-us/articles/20961730681243 for more information. [209.85.208.68 listed in sa-accredit.habeas.com] -0.0 RCVD_IN_MSPIKE_H2 RBL: Average reputation (+2) [209.85.208.68 listed in wl.mailspike.net] 0.0 RCVD_IN_VALIDITY_RPBL_BLOCKED RBL: ADMINISTRATOR NOTICE: The query to Validity was blocked. See https://knowledge.validity.com/hc/en-us/articles/20961730681243 for more information. [209.85.208.68 listed in bl.score.senderscore.com] -0.0 RCVD_IN_DNSWL_NONE RBL: Sender listed at https://www.dnswl.org/, no trust [209.85.208.68 listed in list.dnswl.org] -0.0 SPF_PASS SPF: sender matches SPF record 0.0 SPF_HELO_NONE SPF: HELO does not publish an SPF Record 0.0 FREEMAIL_FROM Sender email is commonly abused enduser mail provider (liliana.prikler[at]gmail.com) 2.2 MALFORMED_FREEMAIL Bad headers on message from free email service -0.0 T_SCC_BODY_TEXT_LINE No description available. X-Debbugs-Envelope-To: 73551 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.4 (/) * gnu/packages/maths.scm (kissat): Update to 4.0.1. [#:phases]: 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 From debbugs-submit-bounces@debbugs.gnu.org Sun Sep 29 05:40:22 2024 Received: (at 73551) by debbugs.gnu.org; 29 Sep 2024 09:40:22 +0000 Received: from localhost ([127.0.0.1]:40110 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1suqPd-0001Zd-MH for submit@debbugs.gnu.org; Sun, 29 Sep 2024 05:40:22 -0400 Received: from mail-ed1-f65.google.com ([209.85.208.65]:50539) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1suqBl-0007vw-EV for 73551@debbugs.gnu.org; Sun, 29 Sep 2024 05:26:39 -0400 Received: by mail-ed1-f65.google.com with SMTP id 4fb4d7f45d1cf-5c721803a89so4344214a12.1 for <73551@debbugs.gnu.org>; Sun, 29 Sep 2024 02:25:30 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1727601864; x=1728206664; darn=debbugs.gnu.org; h=mime-version:to:subject:date:from:references:in-reply-to:message-id :from:to:cc:subject:date:message-id:reply-to; bh=ZLiPBF9Fkp2uBr5gix45AFfbxNjXG4qYT4194ke38kM=; b=GPv+3LNMdqbb1+4PkT5nrunTtxccjRro3dgajuFXm6KgSs6PmkDIu+bDTtrgybflMl vw1VSW8whFSGeMaKWlFLV0itlaq9dEDMdc+a4J8XwSWIWdVxGLeE+L+WlxjAAIwDZ95f FTDSEqPHHhcb/LcxkDEswRufRdUWiNqG/mmMwp9iq+78vYl8EldEZnKlTpaUUZ8lC+yy CmhhJ28b4w8p3CH7t35iSY+ZEQ+ZvpLlS8LWZU4nwliWVH54DDHWkVODUePiYYKFXeT4 wYHbyo0/GjP4CQJx2ttHSA8WLRAmiNvtCXD6ARpd6jIixML3sM5pyfC3nk0ReAuqqeBM zpKg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1727601864; x=1728206664; h=mime-version:to:subject:date:from:references:in-reply-to:message-id :x-gm-message-state:from:to:cc:subject:date:message-id:reply-to; bh=ZLiPBF9Fkp2uBr5gix45AFfbxNjXG4qYT4194ke38kM=; b=aCGGY/b+Tj4ooCgl09cGf51sjomZD/Jd3dvQpyzv7jYtitmZdwusae5c5EiogyMsZG tXV5huhz5iUs4xEd6zQW9n0LU6EWuw6MCf92UoDgc7ysNmJ/IcnZJh2RIX0IpfjWAB1P iom3jsPFtwzBYYZN6j1Oiot0GyMGgu0Q5ZGerSbH76tP015Tezo8BbWOJTS+5NwpOByt 6XEVAz4CBIy63z3wBgSQgSqNc6zQaTQuGzVxGUPfnzbCMbhM7GKqX9XsynMOJYfVp/Qe FxDYZ46mkxgqZxfen6VoQmbBjCJfCj8/vFndFGePuuZOn7roQ0+cx/x7+j6suBq2/Zu+ 1Bsw== X-Gm-Message-State: AOJu0YyoibYWmjpArdto/iYaiXS6BizLyUqrUuPQcX/l9E9GJZTgvytC D/p9pizO6+MSwSqdVtry2fITArh4/yDD2qUJIpak/N8E30Ea+FshmepcBMnE X-Google-Smtp-Source: AGHT+IGegV9pUQ736TiP4jRVJe9rsh27eQbkjAFESfk7hdfAqboUSpXwlID9x6fPxwlcxQ//Hw2jDw== X-Received: by 2002:a05:6402:2425:b0:5c7:227f:3a5b with SMTP id 4fb4d7f45d1cf-5c8826035e5mr8265519a12.26.1727601864184; Sun, 29 Sep 2024 02:24:24 -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 4fb4d7f45d1cf-5c88248af7dsm2997166a12.78.2024.09.29.02.24.23 for <73551@debbugs.gnu.org> (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sun, 29 Sep 2024 02:24:23 -0700 (PDT) Message-ID: <27d754f008a21912ba775f08af50a24fbeddfb62.1727601398.git.liliana.prikler@gmail.com> In-Reply-To: References: From: Liliana Marie Prikler Date: Wed, 25 Sep 2024 21:03:03 +0200 Subject: [PATCH 1/8] gnu: scasp: Update to 1.1.4. to: 73551@debbugs.gnu.org MIME-Version: 1.0 X-Spam-Score: 2.2 (++) 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: * 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 libfla [...] Content analysis details: (2.2 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 0.0 RCVD_IN_VALIDITY_CERTIFIED_BLOCKED RBL: ADMINISTRATOR NOTICE: The query to Validity was blocked. See https://knowledge.validity.com/hc/en-us/articles/20961730681243 for more information. [209.85.208.65 listed in sa-accredit.habeas.com] -0.0 RCVD_IN_MSPIKE_H2 RBL: Average reputation (+2) [209.85.208.65 listed in wl.mailspike.net] 0.0 RCVD_IN_VALIDITY_RPBL_BLOCKED RBL: ADMINISTRATOR NOTICE: The query to Validity was blocked. See https://knowledge.validity.com/hc/en-us/articles/20961730681243 for more information. [209.85.208.65 listed in bl.score.senderscore.com] -0.0 RCVD_IN_DNSWL_NONE RBL: Sender listed at https://www.dnswl.org/, no trust [209.85.208.65 listed in list.dnswl.org] -0.0 SPF_PASS SPF: sender matches SPF record 0.0 SPF_HELO_NONE SPF: HELO does not publish an SPF Record 0.0 FREEMAIL_FROM Sender email is commonly abused enduser mail provider (liliana.prikler[at]gmail.com) 2.2 MALFORMED_FREEMAIL Bad headers on message from free email service -0.0 T_SCC_BODY_TEXT_LINE No description available. X-Debbugs-Envelope-To: 73551 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.4 (/) * 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 From debbugs-submit-bounces@debbugs.gnu.org Sun Sep 29 05:40:22 2024 Received: (at 73551) by debbugs.gnu.org; 29 Sep 2024 09:40:22 +0000 Received: from localhost ([127.0.0.1]:40112 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1suqPe-0001Zs-E3 for submit@debbugs.gnu.org; Sun, 29 Sep 2024 05:40:22 -0400 Received: from mail-ed1-f66.google.com ([209.85.208.66]:47338) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1suqBo-0007xQ-2q for 73551@debbugs.gnu.org; Sun, 29 Sep 2024 05:26:59 -0400 Received: by mail-ed1-f66.google.com with SMTP id 4fb4d7f45d1cf-5c876ed9c93so3369618a12.2 for <73551@debbugs.gnu.org>; Sun, 29 Sep 2024 02:25:32 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1727601867; x=1728206667; darn=debbugs.gnu.org; h=mime-version:to:subject:date:from:references:in-reply-to:message-id :from:to:cc:subject:date:message-id:reply-to; bh=10TWx9rP7OopVtRlpaVGeGlR+g+HXPaENGkdcGxGfhU=; b=aLWBYvxEudizEzqFIHl0sr9tqBH7LqlPbQ7CGEhETJSZIyHouBp9tVO0gvHFtHu9x2 yTztexQ0cs9mrDxBNaL3IDSkPSTT02v1FBdeWiWFd7g1Upg9/S9DykJivu3iePduny// gnIVZCYqrzYWI+Rz+zlCLoVFsGbZVvKL1imC6vxDkuRi2KlmnLUqOZRDtOYmWHJ1xAwb jCLetLkt54NnnjF36IL+QDbnWzt5aOqoTrEGDbHqHzB+DSIzI7KECapX+065mS+P5YAp 4xyMLfoX7T0LMK9oUA5bxL2rImewVSKwz/PyJT6otMmrp84Jlrb6J2mmrS9tKObCL6ss a26A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1727601867; x=1728206667; h=mime-version:to:subject:date:from:references:in-reply-to:message-id :x-gm-message-state:from:to:cc:subject:date:message-id:reply-to; bh=10TWx9rP7OopVtRlpaVGeGlR+g+HXPaENGkdcGxGfhU=; b=Avs3RDu4pZ5BvQCKtkpycXnerITq1NnoDl8FlV+HBwx1WiS+xSlxr/3BsEeT0XVA69 pn2JVfBjJMh9Br0qfIJbhCcX0BrU0+SkvFciWZbyyAAnVt+UTLrzt7oB3sErxPonM6Om ZMrH7b0zzZ5e0j8ocup4XF2MluMgVhzvRBSvloyVSSZqho4VUpcUJu0XtgaUnpfwf9ru VyDdsNnpHzYUgami3qs2lSJIEuzan1K4iNdQ7LtblPUCdWeXqh0yhYFLCdHXIpEhujVF 3GB9SaqjLKfSEqlGL822cN0pXHP2vsz+VimTNUXorPI8vsPf+c2wSafMlhu4Qs+6hvB0 atog== X-Gm-Message-State: AOJu0YwB1ocW407OP4T14BUtVQPt5goqEP7mBjFQ6jABQ2mDvLUz4MzN RlvwIblXHviIVBKENqkZNJEcQmH1UMhiOdU2Nq6vCeU3IZhWzEfRvnrBu35v X-Google-Smtp-Source: AGHT+IEv92Vp6EOfX9eihr/0+d+JP4CMFWJhUKlK9F2chojOED0EzdlZSHGLaxyUSVTbj1rRtUkoyQ== X-Received: by 2002:a05:6402:4019:b0:5c8:77a5:d469 with SMTP id 4fb4d7f45d1cf-5c88261ab43mr7466697a12.26.1727601867000; Sun, 29 Sep 2024 02:24:27 -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 4fb4d7f45d1cf-5c88248af7dsm2997166a12.78.2024.09.29.02.24.25 for <73551@debbugs.gnu.org> (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sun, 29 Sep 2024 02:24:26 -0700 (PDT) Message-ID: In-Reply-To: References: From: Liliana Marie Prikler Date: Wed, 25 Sep 2024 21:55:10 +0200 Subject: [PATCH 3/8] gnu: z3: Update to 4.13.0. to: 73551@debbugs.gnu.org MIME-Version: 1.0 X-Spam-Score: 2.2 (++) 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: * 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 (d [...] Content analysis details: (2.2 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 0.0 RCVD_IN_VALIDITY_CERTIFIED_BLOCKED RBL: ADMINISTRATOR NOTICE: The query to Validity was blocked. See https://knowledge.validity.com/hc/en-us/articles/20961730681243 for more information. [209.85.208.66 listed in sa-accredit.habeas.com] -0.0 RCVD_IN_MSPIKE_H2 RBL: Average reputation (+2) [209.85.208.66 listed in wl.mailspike.net] 0.0 RCVD_IN_VALIDITY_RPBL_BLOCKED RBL: ADMINISTRATOR NOTICE: The query to Validity was blocked. See https://knowledge.validity.com/hc/en-us/articles/20961730681243 for more information. [209.85.208.66 listed in bl.score.senderscore.com] -0.0 RCVD_IN_DNSWL_NONE RBL: Sender listed at https://www.dnswl.org/, no trust [209.85.208.66 listed in list.dnswl.org] -0.0 SPF_PASS SPF: sender matches SPF record 0.0 SPF_HELO_NONE SPF: HELO does not publish an SPF Record 0.0 FREEMAIL_FROM Sender email is commonly abused enduser mail provider (liliana.prikler[at]gmail.com) 2.2 MALFORMED_FREEMAIL Bad headers on message from free email service -0.0 T_SCC_BODY_TEXT_LINE No description available. X-Debbugs-Envelope-To: 73551 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.4 (/) * 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 From debbugs-submit-bounces@debbugs.gnu.org Sun Sep 29 05:40:23 2024 Received: (at 73551) by debbugs.gnu.org; 29 Sep 2024 09:40:23 +0000 Received: from localhost ([127.0.0.1]:40114 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1suqPe-0001a3-Qb for submit@debbugs.gnu.org; Sun, 29 Sep 2024 05:40:23 -0400 Received: from mail-ed1-f68.google.com ([209.85.208.68]:42316) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1suqBo-0007xc-Qn for 73551@debbugs.gnu.org; Sun, 29 Sep 2024 05:27:33 -0400 Received: by mail-ed1-f68.google.com with SMTP id 4fb4d7f45d1cf-5c88e45f467so947840a12.1 for <73551@debbugs.gnu.org>; Sun, 29 Sep 2024 02:25:33 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1727601868; x=1728206668; darn=debbugs.gnu.org; h=mime-version:to:subject:date:from:references:in-reply-to:message-id :from:to:cc:subject:date:message-id:reply-to; bh=fNyJduaD5flKVfMzTqiVMiB+xrf9W218f9pO9hSl9YM=; b=W0K6k2ikT6ZBaWZMNl+vBFn1WcuiBxCotp4G3oHGjfW663YXIMqCuue73+Jfoitux8 9y5a4/c9vDXqamh7fb/J+Pwm6aQtWhmMb5JK4/ldVPzkGZM1TDZH27m0HopQQeNgTl7E k3BDWiTeqoslkQndDO1P3VgYOEU0yVf6LeDjwquQdPnHFlOvXqZJk91pIz0u+tO+QEjO KY8yi6zYjEW5gpLLoUK/Ru9CCrEmTyNK4z2MIfmNmGVHbzBZ1RFKLUJmHnIZIlte5XI5 BFvuxsjlbKuERKL/awFe5qlzOOqt9T4Z6dO/VfXe1jTYwWaFw6+1X2LB3WhvkVv4OrI7 AMog== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1727601868; x=1728206668; h=mime-version:to:subject:date:from:references:in-reply-to:message-id :x-gm-message-state:from:to:cc:subject:date:message-id:reply-to; bh=fNyJduaD5flKVfMzTqiVMiB+xrf9W218f9pO9hSl9YM=; b=fqaPAURo5iaDjWCPPV6cLsiIvc08okFQaQ54ttA62Yp9GmOqNR4kdJWzrqHcn9kLc+ mSibeH/uKzZ+fIiSgnVMqcnBTt7IN3FJY2uTVDya6oaXUT6oQXAC0GY+jPNOu2jNk8+O jaAK3utycmNlqAFsCx7zS9FSKCmtAWi+jZYOFPrX4LrzKbbkzspZiSQ4ygaIQ73+wItg x3xOlZQH6vYdI0F2IEReGtHIo/V6J7bMskRYHLB3vDVrFxsIWEEgjzf2TT2K5uhQLHjR awsVA2kjR0WwjGq1qB3pwuSOjj/heetV/94LrXQ9igEZkBD6Sy2M6i+Uv0Dt4ofBTwwp imSg== X-Gm-Message-State: AOJu0YzQWZK1OPJaPMDRfKgk4WVFmnsDh5cYRFrKu31JAtj0a9kA50pP DuU5rt3Jb4oofYjfUVDRm3ef4dp28pNK9Uqwl3Q4GQ2GfUhstgpNOKzwEeB2 X-Google-Smtp-Source: AGHT+IFQ273XxIqHB5P5I5V27TQbQTR6pw4ujZW/K0CDiCjV6eC4x5vGj8IWSlGogCmS50Cq1R45HQ== X-Received: by 2002:a05:6402:4009:b0:5c5:c2a7:d535 with SMTP id 4fb4d7f45d1cf-5c88248325fmr9774598a12.16.1727601867672; Sun, 29 Sep 2024 02:24:27 -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 4fb4d7f45d1cf-5c88248af7dsm2997166a12.78.2024.09.29.02.24.27 for <73551@debbugs.gnu.org> (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sun, 29 Sep 2024 02:24:27 -0700 (PDT) Message-ID: <8ae7773ff494d9fedbd40bd1c59c1afa2db550ce.1727601398.git.liliana.prikler@gmail.com> In-Reply-To: References: From: Liliana Marie Prikler Date: Wed, 25 Sep 2024 22:02:49 +0200 Subject: [PATCH 4/8] gnu: lingeling: Update to 1.0.0. to: 73551@debbugs.gnu.org MIME-Version: 1.0 X-Spam-Score: 2.2 (++) 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: * gnu/packages/maths.scm (lingeling): Update to 1.0.0. [#:phases]: Adjust accordingly. --- gnu/packages/maths.scm | 132 ++++++++++++++++++++ 1 file changed, 65 i [...] Content analysis details: (2.2 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 0.0 RCVD_IN_VALIDITY_CERTIFIED_BLOCKED RBL: ADMINISTRATOR NOTICE: The query to Validity was blocked. See https://knowledge.validity.com/hc/en-us/articles/20961730681243 for more information. [209.85.208.68 listed in sa-accredit.habeas.com] -0.0 RCVD_IN_MSPIKE_H2 RBL: Average reputation (+2) [209.85.208.68 listed in wl.mailspike.net] 0.0 RCVD_IN_VALIDITY_RPBL_BLOCKED RBL: ADMINISTRATOR NOTICE: The query to Validity was blocked. See https://knowledge.validity.com/hc/en-us/articles/20961730681243 for more information. [209.85.208.68 listed in bl.score.senderscore.com] -0.0 RCVD_IN_DNSWL_NONE RBL: Sender listed at https://www.dnswl.org/, no trust [209.85.208.68 listed in list.dnswl.org] -0.0 SPF_PASS SPF: sender matches SPF record 0.0 SPF_HELO_NONE SPF: HELO does not publish an SPF Record 0.0 FREEMAIL_FROM Sender email is commonly abused enduser mail provider (liliana.prikler[at]gmail.com) 2.2 MALFORMED_FREEMAIL Bad headers on message from free email service -0.0 T_SCC_BODY_TEXT_LINE No description available. X-Debbugs-Envelope-To: 73551 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.4 (/) * gnu/packages/maths.scm (lingeling): Update to 1.0.0. [#:phases]: 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 From debbugs-submit-bounces@debbugs.gnu.org Sun Oct 06 10:20:24 2024 Received: (at 73551-done) by debbugs.gnu.org; 6 Oct 2024 14:20:24 +0000 Received: from localhost ([127.0.0.1]:41871 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1sxS7U-0004D5-49 for submit@debbugs.gnu.org; Sun, 06 Oct 2024 10:20:24 -0400 Received: from mail-wm1-f67.google.com ([209.85.128.67]:46417) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1sxS7S-0004Cw-S7 for 73551-done@debbugs.gnu.org; Sun, 06 Oct 2024 10:20:23 -0400 Received: by mail-wm1-f67.google.com with SMTP id 5b1f17b1804b1-42cd74c0d16so36006545e9.1 for <73551-done@debbugs.gnu.org>; Sun, 06 Oct 2024 07:20:16 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1728224356; x=1728829156; 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=GQV1lJMPtbLL92tstsHieiUYu/u9IZOz8BVEcqtz0eY=; b=Xyn9n3XdoLcpbRDGzN9uANiNFqDRgWiCKRLeBsdO71gEFSNk54NueeWY9f8ZPWBWbb mLdUtO8V/T+I27r3bodUfdQXs4Xvt99YzV+fwLnZwTm5ZHaKZV3A8DyStVHBL9nZ7c00 jY8wMoLuDzTOae881E8TAwVsjG89fEI21dwzw1DSJ5KFLChQkis4g8/Bpo+TcCj5ND4h 06u/DYhuJ4+MVLdu5ByrX7UtiVb6xO9U3WjlviprnihrNwaXQyqEEL6w0EjF5O0ssVEj Nk7P4wPy2BJeohact/gui0DCX1YPZGo5vYO343pg1CGmUDHY95C5Zb8mn65cJcxfTQ4K NkdQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1728224356; x=1728829156; 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=GQV1lJMPtbLL92tstsHieiUYu/u9IZOz8BVEcqtz0eY=; b=CYjCx6kbJucCepSilxuwf0WHpTMdDgA75EsFFc3EHZLyfvgoEGOnWJ04HlYAGPz+MO h/6xg05yNwZJqhUPQkiOra9TijYwIXRxMHuWxjOhTEgPDykXGl5qVxJrUrR2Ui1IKjH/ 8viwxDN8mz5wR8ItvSUI0rFIz7JKTEdOH+TETSK7ZIY5lHdtuDnDkKg1CGlaYd42bqJu bFdeaNmIDbuCFe+kMK65bdXKKad6i2loNr/X5fiFmPa4dg5f2o2zJH8sMi/lLwiAodPY +6vXvBAmrCVVBsOrdKhdIcg/9DX3DQxYIlGo0H+/eih0wW+FnzgXunWEaRjEc7JQGuwx IqbQ== X-Gm-Message-State: AOJu0YwMJF8ejVDBtfDkMqD9kLpXqyJsGj1ddcia6cb4o0CdXKteRbEP h7OmBmnuwVkVf9mFGkTyBL4+rpsi8wucknSOjmWHAeE0qXvLFoHy5V4sa5F6 X-Google-Smtp-Source: AGHT+IF0CYPe9T1a8XtSC5hgEruNfri/5lV+wsWt++eJkO8Y/GORkEta20wSFz/U1KOGGG2w1BXkTg== X-Received: by 2002:a05:600c:215:b0:42c:b74c:d8c3 with SMTP id 5b1f17b1804b1-42f85b64a17mr55834635e9.32.1728224356127; Sun, 06 Oct 2024 07:19:16 -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 ffacd0b85a97d-37d1697301fsm3684625f8f.100.2024.10.06.07.19.14 for <73551-done@debbugs.gnu.org> (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sun, 06 Oct 2024 07:19:15 -0700 (PDT) Message-ID: <3077c4187c0ac122f3ad8836562bdc098a918768.camel@gmail.com> Subject: Re: [PATCH 0/8] Update some SAT/ASP solvers From: Liliana Marie Prikler To: 73551-done@debbugs.gnu.org Date: Sun, 06 Oct 2024 16:19:14 +0200 In-Reply-To: References: Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable User-Agent: Evolution 3.48.4 MIME-Version: 1.0 X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 73551-done 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 (-) Am Sonntag, dem 29.09.2024 um 11:16 +0200 schrieb Liliana Marie Prikler: > Liliana Marie Prikler (8): > =C2=A0 gnu: scasp: Update to 1.1.4. > =C2=A0 gnu: kissat: Update to 4.0.1. > =C2=A0 gnu: z3: Update to 4.13.0. > =C2=A0 gnu: lingeling: Update to 1.0.0. > =C2=A0 gnu: Add cadical. > =C2=A0 gnu: Add cadiback. > =C2=A0 gnu: Add cadiback-for-cryptominisat. > =C2=A0 gnu: cryptominisat: Update to 5.11.22. Done and pushed. From unknown Sat Aug 16 21:58:37 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Mon, 04 Nov 2024 12:24:14 +0000 User-Agent: Fakemail v42.6.9 # This is a fake control message. # # The action: # bug archived. thanks # This fakemail brought to you by your local debbugs # administrator