From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp12.migadu.com ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms5.migadu.com with LMTPS id yAByH2qd/GJL/AAAbAwnHQ (envelope-from ) for ; Wed, 17 Aug 2022 09:48:58 +0200 Received: from aspmx1.migadu.com ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp12.migadu.com with LMTPS id kWtAH2qd/GJYMwAAauVa8A (envelope-from ) for ; Wed, 17 Aug 2022 09:48:58 +0200 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by aspmx1.migadu.com (Postfix) with ESMTPS id 2A5CEB656 for ; Wed, 17 Aug 2022 09:48:58 +0200 (CEST) Received: from localhost ([::1]:60218 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1oODnN-0000cd-30 for larch@yhetil.org; Wed, 17 Aug 2022 03:48:57 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:41126) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1oODlY-0000bb-0K for guix-patches@gnu.org; Wed, 17 Aug 2022 03:47:08 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:59609) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1oODlW-00062p-25 for guix-patches@gnu.org; Wed, 17 Aug 2022 03:47:03 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1oODlV-0003It-Se for guix-patches@gnu.org; Wed, 17 Aug 2022 03:47:01 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#57181] [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat References: <923508243.78855.1660404889221@ox93.mailbox.org> Resent-From: mail@maxheisinger.at Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Wed, 17 Aug 2022 07:47:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 57181 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: liliana.prikler@gmail.com Cc: 57181@debbugs.gnu.org Received: via spool by 57181-submit@debbugs.gnu.org id=B57181.166072238912653 (code B ref 57181); Wed, 17 Aug 2022 07:47:01 +0000 Received: (at 57181) by debbugs.gnu.org; 17 Aug 2022 07:46:29 +0000 Received: from localhost ([127.0.0.1]:49355 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oODkv-0003Hv-Dy for submit@debbugs.gnu.org; Wed, 17 Aug 2022 03:46:29 -0400 Received: from mout-p-202.mailbox.org ([80.241.56.172]:46968) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oOCW7-0001JD-3S for 57181@debbugs.gnu.org; Wed, 17 Aug 2022 02:27:07 -0400 Received: from smtp102.mailbox.org (smtp102.mailbox.org [10.196.197.102]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange ECDHE (P-384) server-signature RSA-PSS (4096 bits) server-digest SHA256) (No client certificate requested) by mout-p-202.mailbox.org (Postfix) with ESMTPS id 4M6yjB4M8Vz9sVy; Wed, 17 Aug 2022 08:26:54 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=maxheisinger.at; s=MBO0001; t=1660717614; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version:content-type:content-type: in-reply-to:in-reply-to; bh=yxbCjAobSX90sbiAo8O1SdeoHuNhOFO5yJLU7BX3/8E=; b=qpNs3o6qahkH3mhoUyRUTNs0AKhQczQ3gkWWdidh7k5JfAnBZvCQxB5rUQGk3nNS+no8JQ qqoQeDoWhA8lq0UJRpxHtLjdPbVjdRUDLg/CQ95kcMdqOxzA1l94I2eWeO5jbJm2pu//6r 0M/g11JoXtYKamJC7AILCiC1CucsvMwPcPKuBA3mf5Z1nd4S3hIFjmFnhxf1i/R1e6HbX5 WegYBijlm5eY6J2BXy8ZvMnnKAVfQ3lmOF4sGSnWgX4PG/SpI81rMEJoHP/Ulyaq+PZvG8 /7TWKiaZ1aRfJQvYraV2M5xQRnfc0KloVRMzoGgTjF0UxaP+w2/BO39QOujJgQ== From: mail@maxheisinger.at In-Reply-To: <742d924abc9cfa0b2073c053e229e8ee437704ce.camel@gmail.com> Date: Wed, 17 Aug 2022 08:26:52 +0200 Message-ID: <87wnb74c7n.fsf@maxheisinger.at> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="=-=-=" X-Mailman-Approved-At: Wed, 17 Aug 2022 03:46:24 -0400 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+larch=yhetil.org@gnu.org Sender: "Guix-patches" X-Migadu-Flow: FLOW_IN X-Migadu-To: larch@yhetil.org X-Migadu-Country: US ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1660722538; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:cc:mime-version:mime-version: content-type:content-type:resent-cc:resent-from:resent-sender: resent-message-id:in-reply-to:in-reply-to:references:references: list-id:list-help:list-unsubscribe:list-subscribe:list-post: dkim-signature; bh=yxbCjAobSX90sbiAo8O1SdeoHuNhOFO5yJLU7BX3/8E=; b=FMgni/lcexwKAvbDfCB5lGFNguGAjeGU7obqt6UvwofnuMc4+B0Fhk8RDTqu0epk51w/mJ VrjkZrtQuPgYlgPY+coL+joyG2+x/dcfZ73vEOtgySYbiW7Bj9y311bCiP9ekmGAEgvKJl fEjI4j0Y1oNyojSxccJKHpi6vA1TO0wxDMEufl9smVHatZ9av480qthlWP5kwVzsLLcHZU 2liLipnGIlFRoX1T2foXNdJyW/uVFclmj6m+fIH9ieVlaBVQgp+A0fZdVnMyovBcF0lNvc XreSxiR2iex5l3b4+mArxxtTB67kM0KG7XWHxQbc3oSLhtKP1bxj16LE/hcnFQ== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1660722538; a=rsa-sha256; cv=none; b=kMircJfq+y4bClurzgd4S7Et1GkZcmApN/NcU8rU7QZ+KnPiaVG45jqsLIFkaX1e2pawHW Uw09pAIOf/T3d+1mIhETrAJEjXF8As58rnJPpcw5CO9QCetCEuLQMaslWkHTxZMh7nPf8/ GtoGvShzZXXmnk3Uvc4VXehzlnTx0pbLSLxOE3RX06HTXIdeeuHLxbQG/EfFLHpepioVkA 0epnUbYVfOvU+ELf2KrDAnQLWucc2sS+y7n4gU3T+Wi2VnClLHRa80e/KewlYCeM5otRVN 6efytcljY7YDjXkekCdQRH1Dci6UjqXiguymocvUM9rALQUdZT3zvBRCQdXFgg== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=maxheisinger.at header.s=MBO0001 header.b=qpNs3o6q; dmarc=fail reason="SPF not aligned (relaxed)" header.from=maxheisinger.at (policy=none); spf=pass (aspmx1.migadu.com: domain of "guix-patches-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="guix-patches-bounces+larch=yhetil.org@gnu.org" X-Migadu-Spam-Score: 7.04 Authentication-Results: aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=maxheisinger.at header.s=MBO0001 header.b=qpNs3o6q; dmarc=fail reason="SPF not aligned (relaxed)" header.from=maxheisinger.at (policy=none); spf=pass (aspmx1.migadu.com: domain of "guix-patches-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="guix-patches-bounces+larch=yhetil.org@gnu.org" X-Migadu-Queue-Id: 2A5CEB656 X-Spam-Score: 7.04 X-Migadu-Scanner: scn0.migadu.com X-TUID: 5RwDSO2LSUZl --=-=-= Content-Type: text/plain Hi, > - fixed the commit message, > - hard-coded the compression binaries (and made them regular inputs), > - fixed the actual test failure, > - used G-Expressions rather than quasiquoting. > > See 9ddd37d6ab59e2519bbcefad15ce62561128f0ee. Thank you very much! This really is clearer, better, and gives me more pointers to research about Guix. > the problem here is rather that cryptominisat seems to pull in lots of > stuff that we'd rather have packaged separately instead of vendored > (e.g. googletest). Could you try unvendoring those things and place > the remaining parts in the right location without a recursive > checkout? Yes, that would be better... Then we have two choices now I think: 1. Try to unvendor everything and add minisat as transformed package with different sources + lingeling as a new package. This would also still require to download the external test files as additional source repositories. 2. Or we rely on using the ~ONLY_SIMPLE~ CMake option CryptoMiniSat offers that is meant to build a simpler binary, but also deactivates more complex tests. We still build a complex binary (i.e. Boost program options for options parsing) by not setting it, but instead substitute the query for the option in the ~test/CMakeLists.txt~ file. Additionally, we substitute some other issues away. The second option loses some scripts and the more comprehensive tests. I would argue though, that these would be better suited for developing the solver and less for such a package management situation. What is your opinion about this trade-off? > "Incremental solving" sounds easier to understand. Changed it. > If you have a Python interface, you probably also need python in > inputs, no? True - it is better to directly expose it. I also took another look at the solver's capabilities and output in more detail and added python-numpy (required dependency for the py API) and sqlite (optional dependency used for collecting statistics). Thank you again for your patience and effort! You find my updated patch attached. Best regards (now even written from an Emacs mail client), Max --=-=-= Content-Type: text/x-patch; charset=utf-8 Content-Disposition: inline; filename=0001-gnu-Add-cryptominisat5.patch Content-Transfer-Encoding: quoted-printable >From 5541a0aeb7660eacd5dbec8ef88db42af7b3b7b5 Mon Sep 17 00:00:00 2001 From: Maximilian Heisinger Date: Tue, 16 Aug 2022 20:59:06 +0200 Subject: [PATCH] gnu: Add cryptominisat5 * gnu/packages/maths.scm (cryptominisat5): Add package. --- gnu/packages/maths.scm | 50 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 50 insertions(+) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 72d5e9a83a..a01f386831 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -55,6 +55,7 @@ ;;; Copyright =C2=A9 2022 Philip McGrath ;;; Copyright =C2=A9 2022 Marek Fel=C5=A1=C3=B6ci ;;; Copyright =C2=A9 2022 vicvbcun +;;; Copyright =C2=A9 2022 Maximilian Heisinger ;;; ;;; This file is part of GNU Guix. ;;; @@ -159,6 +160,7 @@ (define-module (gnu packages maths) #:use-module (gnu packages shells) #:use-module (gnu packages sphinx) #:use-module (gnu packages swig) + #:use-module (gnu packages sqlite) #:use-module (gnu packages tcl) #:use-module (gnu packages texinfo) #:use-module (gnu packages tex) @@ -7317,6 +7319,54 @@ (define-public minisat "http://minisat.se/MiniSat.html") (license license:expat)))) =20 +(define-public cryptominisat5 + (package + (name "cryptominisat5") + (version "5.8.0") + (source + (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/msoos/cryptominisat") + (commit version))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "00hmxdlyhn7pwk9jlvc5g0l5z5xqfchjzf5jgn3pkj9xhl8yqq50")))) + (build-system cmake-build-system) + (arguments + (list #:build-type "Release" + #:test-target "test" + #:configure-flags + #~(list "-DENABLE_TESTING=3DON" "-DSTATS=3DON") + #:phases + #~(modify-phases %standard-phases + (add-after 'unpack 'patch-source + (lambda* (#:key inputs #:allow-other-keys) + (substitute* "CMakeLists.txt" + (("add_subdirectory\\(utils/lingeling-ala\\)") "")) + ;; Transitively included in vendored gtest.h. Fixed in + ;; upstream: + ;; https://github.com/msoos/cryptominisat/pull/686 + (substitute* "tests/assump_test.cpp" + (("#include ") + "#include \n#include ")) + (substitute* "tests/CMakeLists.txt" + (("add_subdirectory\\(\\$\\{GTEST_PREFIX\\} gtest\\)") + "find_package(GTest REQUIRED)") + (("if\\(NOT ONLY_SIMPLE\\)") "if(FALSE)"))))))) + (inputs (list zlib boost sqlite python python-numpy)) + (native-inputs (list python-lit googletest)) + (synopsis "Incremental SAT solver") + (description + "CryptoMiniSat is an incremental SAT solver with both command line and +library (C++, C, Python) interfaces. The command-line interface takes a +@acronym{CNF, Conjunctive Normal Form} as an input in the DIMACS format wi= th +the extension of XOR clauses. The library interfaces mimic this and also +allow incremental solving, including assumptions.") + (home-page "https://github.com/msoos/cryptominisat") + (license license:expat))) + (define-public kissat (package (name "kissat") --=20 2.37.2 --=-=-=--