From unknown Sat Jun 14 03:58:11 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#57181] [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat Resent-From: Maximilian Heisinger Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sat, 13 Aug 2022 16:57:03 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 57181 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 57181@debbugs.gnu.org X-Debbugs-Original-To: "guix-patches@gnu.org" Received: via spool by submit@debbugs.gnu.org id=B.166040981024389 (code B ref -1); Sat, 13 Aug 2022 16:57:03 +0000 Received: (at submit) by debbugs.gnu.org; 13 Aug 2022 16:56:50 +0000 Received: from localhost ([127.0.0.1]:34975 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oMuRL-0006LE-1y for submit@debbugs.gnu.org; Sat, 13 Aug 2022 12:56:50 -0400 Received: from lists.gnu.org ([209.51.188.17]:44812) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oMtAP-0004Gq-0h for submit@debbugs.gnu.org; Sat, 13 Aug 2022 11:35:16 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:52886) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1oMtAD-0001AW-Co for guix-patches@gnu.org; Sat, 13 Aug 2022 11:35:04 -0400 Received: from mout-p-202.mailbox.org ([80.241.56.172]:56256) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_CHACHA20_POLY1305:256) (Exim 4.90_1) (envelope-from ) id 1oMtA8-0006Nf-MM for guix-patches@gnu.org; Sat, 13 Aug 2022 11:35:01 -0400 Received: from smtp2.mailbox.org (smtp2.mailbox.org [10.196.197.2]) (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 4M4l3F5VTBz9sTh for ; Sat, 13 Aug 2022 17:34:49 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=maxheisinger.at; s=MBO0001; t=1660404889; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version:content-type:content-type; bh=ugBfwExP9pqFp7Fzh18MxqZ3yTZmZOQ14UZnKuDRyXU=; b=JZVb1JsP8hkcK0KrIFuooT02Cx5orqlCPg5JHFaaLFCEMhAnmCokkN24ZvgPN1WjzRp+qA gydxKgHjFetpUdXZc+N3x+VgnPl6h/Tz6QchuIRWLL/U6CvWhO+IWbmO8WM6hSoxy3NGuX g7R+2dKePPlU7xsq0yapyUn6EwoossFtns8rWE2xHHxT4f+5Jq5SI11agUNfxPVeAmc9W2 /3DuTXnTa2COzymvU7pJbKKULHXzLPI/z9fcgPyeXIuzJM6HGmakzu2mcLW003eLUkBBfM 14SJQwQB6RPb/GYX3HJFSJP2t0Yezljf3X9bE7hGHsEohBPyooqFsMw8Qau3zg== Date: Sat, 13 Aug 2022 17:34:49 +0200 (CEST) From: Maximilian Heisinger Message-ID: <923508243.78855.1660404889221@ox93.mailbox.org> MIME-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha512; protocol="application/pgp-signature"; boundary="----=_Part_78854_1462168451.1660404889220" X-Priority: 3 Importance: Normal Received-SPF: pass client-ip=80.241.56.172; envelope-from=mail@maxheisinger.at; helo=mout-p-202.mailbox.org X-Spam_score_int: -27 X-Spam_score: -2.8 X-Spam_bar: -- X-Spam_report: (-2.8 / 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_DNSWL_LOW=-0.7, SPF_HELO_NONE=0.001, SPF_PASS=-0.001, T_SCC_BODY_TEXT_LINE=-0.01 autolearn=ham autolearn_force=no X-Spam_action: no action X-Spam-Score: -1.3 (-) X-Mailman-Approved-At: Sat, 13 Aug 2022 12:56:45 -0400 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: -2.3 (--) ------=_Part_78854_1462168451.1660404889220 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit >From dea29e40c0cfb5eaac49060082fe63c0ed1e08b7 Mon Sep 17 00:00:00 2001 From: Maximilian Heisinger Date: Sat, 13 Aug 2022 17:23:59 +0200 Subject: [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat * gnu/packages/maths.scm (cryptominisat5): Add package. * gnu/packages/maths.scm (kissat): Add package. --- gnu/packages/maths.scm | 64 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 64 insertions(+) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index c79058ab42..4a58b9eb3f 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -7311,6 +7311,70 @@ (define-public minisat "http://minisat.se/MiniSat.html") (license license:expat)))) +(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 `(#:tests? #false)) + (inputs (list zlib boost)) + (synopsis "Advanced incremental SAT solver") + (description + "Provides CryptoMiniSat, an advanced incremental SAT solver. The system +has 3 interfaces: command-line, C++ library and python. The command-line +interface takes a cnf as an input in the DIMACS format with the extension of +XOR clauses. The C++ and python interface mimics this and also allows for +incremental use: assumptions and multiple solve calls. A C compatible wrapper +is also provided.") + (home-page "https://github.com/msoos/cryptominisat") + (license license:expat))) + +(define-public kissat + (package + (name "kissat") + (version "3.0.0") + (source + (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/arminbiere/kissat") + (commit (string-append "rel-" version)))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "04x4w760srbdi4zci0s747qxk717x5d2x59ixraxh5104s9nyn8b")))) + (build-system gnu-build-system) + (arguments + `(#:tests? #f + #:phases + (modify-phases %standard-phases + (replace 'configure + (lambda* (#:key outputs #:allow-other-keys) + (invoke "./configure"))) + (replace 'install + (lambda* (#:key inputs outputs #:allow-other-keys) + (install-file + "build/kissat" + (string-append (assoc-ref outputs "out") "/bin"))))))) + (home-page "https://github.com/arminbiere/kissat") + (synopsis "Bare-metal SAT solver after the KISS principle principle +written in C") + (description + "Kissat is a \"keep it simple and clean bare metal SAT solver\" written +in C. It is a port of CaDiCaL back to C with improved data structures, better +scheduling of inprocessing and optimized algorithms and implementation.") + (license license:gpl3+))) + (define-public libqalculate (package (name "libqalculate") -- 2.37.1 ------=_Part_78854_1462168451.1660404889220 Content-Type: application/pgp-signature Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename=signature.asc -----BEGIN PGP SIGNATURE----- Version: BCPG v1.65 iQEcBAABCgAGBQJi98SZAAoJEIhyV2pwqbcQW1UH/ijwpo9WkbAbaJ+oW5YBz9K9 ogx65DSyABAtwd5z0wyKvERSBuSB/z0W4jeOjwrCIXCDIV1aDlHR6WHVvfIUgLk0 7GtiwnZW6nCnAYQBP8Zm7WdeEAucrhops5JDTzk/evI5rwJceC396yVH4lBv+3Q9 VRPDlQI/kQ3gPsXjIUbpUFSY8zQM5Dp1EPp2IaVteuy0r42XHET/hQLOuKK8BXwt rnfFlu3RcdfbKHH/2xTaIEwHeLp3FdmAZeMNuHdDEls2LY14lYSQEQeP4uVKk66m Wo29zupk86eDWsvMqjP8Ic1Jj0GA33XlajEH5ail4ymtMRITiO/74OkjiZPBrgo= =SmL6 -----END PGP SIGNATURE----- ------=_Part_78854_1462168451.1660404889220-- From unknown Sat Jun 14 03:58:11 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#57181] [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat Resent-From: Liliana Marie Prikler Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sat, 13 Aug 2022 20:06:02 +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: Maximilian Heisinger Cc: 57181@debbugs.gnu.org Received: via spool by 57181-submit@debbugs.gnu.org id=B57181.166042111318278 (code B ref 57181); Sat, 13 Aug 2022 20:06:02 +0000 Received: (at 57181) by debbugs.gnu.org; 13 Aug 2022 20:05:13 +0000 Received: from localhost ([127.0.0.1]:35193 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oMxNg-0004kk-Hn for submit@debbugs.gnu.org; Sat, 13 Aug 2022 16:05:12 -0400 Received: from mail-ej1-f65.google.com ([209.85.218.65]:43697) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oMxNe-0004kU-DR for 57181@debbugs.gnu.org; Sat, 13 Aug 2022 16:05:11 -0400 Received: by mail-ej1-f65.google.com with SMTP id gb36so7263383ejc.10 for <57181@debbugs.gnu.org>; Sat, 13 Aug 2022 13:05:10 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=content-transfer-encoding:mime-version:user-agent:references :in-reply-to:date:cc:to:from:subject:message-id:from:to:cc; bh=0IsE2Ds81o2vvWL+BE9twWtXklcAGJGKd7mPwecrFPc=; b=g1C1Egg2lZr4RymYmaJLXNPjyZkHQgr/l70myNlju0cfC6pWV1UDVGdmzbVTcmOIrl FTIe6dN5BR1xCjHyxUDF8V9VbxCUA+18GPQvztLkLohz7Yteq07R+0PjOA3QedM4ju5M ++K6gRN00TC6X9VQ9aaom/qu+4K1tvhJ66Ac9lXyAY+mCTErrzuEG44BR/kz3fb1KJAU jwRKu0X9APLe4eT7pP6o5kZPfIa0lq0ZOUNzVUVqbPGZGBWLl61H6empeOE/9ti6LFWl 9Sgk8vnUoau74V2cPOQl2tlbiWCz1T3p2qSJb9t+ZniNFbInnVMGP8XnB9Mc+Iq/+2fT Wwmg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=content-transfer-encoding:mime-version:user-agent:references :in-reply-to:date:cc:to:from:subject:message-id:x-gm-message-state :from:to:cc; bh=0IsE2Ds81o2vvWL+BE9twWtXklcAGJGKd7mPwecrFPc=; b=gK2va34inRU5e1UQOat+ahRoc7XWPbteFF4fhGhtGEIWx5kKknYsM7qjoto/1ihaBL FYFNt0My9BRm+LuP9YAQmCejYWQ/qaIS+rnwm7jt8QrQHY8Md95EE9UOOF754Ik/fvM3 tq3BNzf0/XwpPQfSUdUyi0zcuJBRLzipxw/h55QXeeuLvDP1h+Fijrywwf4jngzUnHty Mtuqi7LRfLzAMpKTrXwtF7LUz94//qcivLcIRRic/SNPleRGdwEWC/1inuXDIiPdAwuv 3UYCapMAHNFm/MOuJ4qFhcbE6Azdq6RdLonsdaxBkiUiDNO3bowomJYF8a3RcBnmgK9P u3bQ== X-Gm-Message-State: ACgBeo1l7hVomAPg0jfdCygyQPIGHb0cpoVeosTPxzsaCEayV9VNjdGb Lnn1fdH33M3U5W8G4IYnwwE= X-Google-Smtp-Source: AA6agR6BmLoUJWIih9FyMbYyQE4lOAu6g9y98ZMWZ5Vj+ahNKmjboBjeUf+ZOtsJSOsQ9TJOqOr/YQ== X-Received: by 2002:a17:907:7f0b:b0:731:b81a:1912 with SMTP id qf11-20020a1709077f0b00b00731b81a1912mr6335779ejc.8.1660421104509; Sat, 13 Aug 2022 13:05:04 -0700 (PDT) Received: from nijino.fritz.box (85-127-52-93.dsl.dynamic.surfer.at. [85.127.52.93]) by smtp.gmail.com with ESMTPSA id p22-20020a056402155600b0043a6e807febsm3480380edx.46.2022.08.13.13.05.03 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sat, 13 Aug 2022 13:05:03 -0700 (PDT) Message-ID: <1dbd4bac9403ed4dd17de75dfc2d210daf2d2ea3.camel@gmail.com> From: Liliana Marie Prikler Date: Sat, 13 Aug 2022 22:05:02 +0200 In-Reply-To: References: Content-Type: text/plain; charset="UTF-8" User-Agent: Evolution 3.42.1 MIME-Version: 1.0 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 (-) Hi, Am Samstag, dem 13.08.2022 um 17:23 +0200 schrieb Maximilian Heisinger: > * gnu/packages/maths.scm (cryptominisat5): Add package. > * gnu/packages/maths.scm (kissat): Add package. Split into two patches, one for cryptominisat and one for kissat. > --- >  gnu/packages/maths.scm | 64 > ++++++++++++++++++++++++++++++++++++++++++ >  1 file changed, 64 insertions(+) > > diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm > index c79058ab42..4a58b9eb3f 100644 > --- a/gnu/packages/maths.scm > +++ b/gnu/packages/maths.scm > @@ -7311,6 +7311,70 @@ (define-public minisat >         "http://minisat.se/MiniSat.html") >        (license license:expat)))) > > +(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 `(#:tests? #false)) Always state why tests are disabled. > +    (inputs (list zlib boost)) > +    (synopsis "Advanced incremental SAT solver") "Incremental SAT solver" is probably enough. > +    (description > +     "Provides CryptoMiniSat, an advanced incremental SAT solver.  > The system > +has 3 interfaces: command-line, C++ library and python. I'd shorten this to "CryptoMiniSat is an incremental SAT solver with three interfaces: command-line, C++ library and Python". >   The command-line > +interface takes a cnf as an input in the DIMACS format with the > extension of Use @abbrev for CNF (also capitalize). > +XOR clauses.  The C++ and python interface mimics this and also > allows for > +incremental use: assumptions and multiple solve calls.  A C > compatible wrapper > +is also provided.") Doesn't that technically make it a fourth interface? > +    (home-page "https://github.com/msoos/cryptominisat") > +    (license license:expat))) > +(define-public kissat > +  (package > +    (name "kissat") > +    (version "3.0.0") > +    (source > +     (origin > +       (method git-fetch) > +       (uri (git-reference > +             (url "https://github.com/arminbiere/kissat") > +             (commit (string-append "rel-" version)))) > +       (file-name (git-file-name name version)) > +       (sha256 > +        (base32 > +         "04x4w760srbdi4zci0s747qxk717x5d2x59ixraxh5104s9nyn8b")))) > +    (build-system gnu-build-system) > +    (arguments > +     `(#:tests? #f Specify why. > +       #:phases > +       (modify-phases %standard-phases > +         (replace 'configure > +           (lambda* (#:key outputs #:allow-other-keys) > +             (invoke "./configure"))) You probably want to (apply invoke "./configure" configure-flags). > +         (replace 'install > +           (lambda* (#:key inputs outputs #:allow-other-keys) > +             (install-file > +              "build/kissat" > +              (string-append (assoc-ref outputs "out") "/bin"))))))) Is this the only thing to install? > +    (home-page "https://github.com/arminbiere/kissat") > +    (synopsis "Bare-metal SAT solver after the KISS principle > principle > +written in C") "Bare-metal SAT solver" probably suffices. > +    (description > +     "Kissat is a \"keep it simple and clean bare metal SAT solver\" > written "bare metal SAT solver" again probably suffices. If you want to be generous with advertising terms, clean may be added, but I don't think it adds useful information. > +in C.  It is a port of CaDiCaL back to C with improved data > structures, better > +scheduling of inprocessing and optimized algorithms and > implementation.") > +    (license license:gpl3+))) > + Cheers From unknown Sat Jun 14 03:58:11 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#57181] [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat Resent-From: Liliana Marie Prikler Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 14 Aug 2022 22:08:02 +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: Maximilian Heisinger Cc: 57181@debbugs.gnu.org Received: via spool by 57181-submit@debbugs.gnu.org id=B57181.166051487222180 (code B ref 57181); Sun, 14 Aug 2022 22:08:02 +0000 Received: (at 57181) by debbugs.gnu.org; 14 Aug 2022 22:07:52 +0000 Received: from localhost ([127.0.0.1]:40027 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oNLlw-0005lf-1W for submit@debbugs.gnu.org; Sun, 14 Aug 2022 18:07:52 -0400 Received: from mail-ed1-f65.google.com ([209.85.208.65]:44929) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oNLlt-0005lT-V8 for 57181@debbugs.gnu.org; Sun, 14 Aug 2022 18:07:51 -0400 Received: by mail-ed1-f65.google.com with SMTP id t5so7544830edc.11 for <57181@debbugs.gnu.org>; Sun, 14 Aug 2022 15:07:49 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=content-transfer-encoding:mime-version:user-agent:references :in-reply-to:date:cc:to:from:subject:message-id:from:to:cc; bh=nAzUO8eY9MVBESB//nCEWGl4k5hAwnjv2UWwOZUpR4k=; b=hKYvIPlBa/Dw7L8I2Mg1lq4l2ECmuWWNWCyiGpPMEw04R1eH2HKczCR407w/0iyy7m k6AaAElXDArt51vxdcLBMGLNF3vd4XD+vIz+R8Nre8+kmipbYURqPaPRuGesj4Tmp1tu 9vXWZwEY3y6FtVPfNmPEkvRhveezeBM/bwxIAgxLcYk+DHMKDzhbnESjYN/+EdouwKd6 T8lB9ytJKUfBNOLGcZlFDA5XJHkcQs1PjiEsuU68iemnGq1egJi7MZ8h/3Ofz+TbPZ3/ Wkqjy4BAMEd/OyOncVCl+4N0r7pPH22wgnCyZeKYmCfPpOVwWtwIAgRXzoETMLYb+KM2 AFsA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=content-transfer-encoding:mime-version:user-agent:references :in-reply-to:date:cc:to:from:subject:message-id:x-gm-message-state :from:to:cc; bh=nAzUO8eY9MVBESB//nCEWGl4k5hAwnjv2UWwOZUpR4k=; b=QQdZp0ZxwQ4vhNn/S9/m/YF8C5uFCQZbZOmQGEXSYskNNd+mxTT1K/ke4Os5T+qXGW JmmjMaQf12LCTF9A3QjLvUaEH2QFHs7BePLzipGy7NSS85nsX6wpWbOb7P1wyU602k56 WPEAnFEif+UO1XWOqBqcSYm0SjsJ/f+H+O3PCy0QYH4DlCQASbTq3DrAs0cIvISBXLHd PuBuBrT22SaPUrNR6Mw0oWcs6UQipRMhQOPHLi2U14w2bkNhNUGSeqRYMXy5KVdypMSr HmUp1tnGlLzKWYKMsmpw1464Q7KefMju/6LyVzlf2D39C8ZcrkTap+fSrUxwZlr/hTwL BIOg== X-Gm-Message-State: ACgBeo1zatjpC3/D6YgGbsRbDc2bAcsSoC+Z1IAknzsv2U14fpQuYMrH TsJ6BMLEe5oGM6afVKsc0c8= X-Google-Smtp-Source: AA6agR7doXE4Qy3zufpCrg80NLmGkypyUDnipBGQX1N4PVofVLKIs84usocoZdHaX6fHWnlyRsiGfg== X-Received: by 2002:a05:6402:26cb:b0:43e:6fab:11c6 with SMTP id x11-20020a05640226cb00b0043e6fab11c6mr11471576edd.272.1660514864202; Sun, 14 Aug 2022 15:07:44 -0700 (PDT) Received: from nijino.fritz.box (85-127-52-93.dsl.dynamic.surfer.at. [85.127.52.93]) by smtp.gmail.com with ESMTPSA id n18-20020aa7c452000000b0043ba437fe04sm5472328edr.78.2022.08.14.15.07.43 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sun, 14 Aug 2022 15:07:43 -0700 (PDT) Message-ID: <4349f97ccc76a0ee579442c3a4f50b4ba2f4f34c.camel@gmail.com> From: Liliana Marie Prikler Date: Mon, 15 Aug 2022 00:07:42 +0200 In-Reply-To: <1840023126.104586.1660505267957@ox93.mailbox.org> References: <1dbd4bac9403ed4dd17de75dfc2d210daf2d2ea3.camel@gmail.com> <1840023126.104586.1660505267957@ox93.mailbox.org> Content-Type: text/plain; charset="UTF-8" User-Agent: Evolution 3.42.1 MIME-Version: 1.0 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 (-) Hi, Don't forget to CC the mailing list. Am Sonntag, dem 14.08.2022 um 21:27 +0200 schrieb Maximilian Heisinger: > gnu: maths: Add modern SAT solver cryptominisat5 Should simply be "gnu: Add cryptominisat5. > + (uri (git-reference > + (url "https://github.com/msoos/cryptominisat") > + (commit version) > + (recursive? #t))) Recursive checkout doesn't really sound "mini". > > + (description > + "Incremental SAT solver with four interfaces: command-line, C++ > library, > +C interface, and Python. I forgot this, but the description should consist of full sentences. Also, while I (jokingly) referred to the C interface as a separate interface, you should probably phrase this a little differently. > gnu: maths: Add modern SAT solver kissat As above. > + ;; One test fails in the guix build container: "main". > The cause > + ;; is not clear yet and this test is not enabled in the > tissat > + ;; test step. Kissat (called by tissat) just does not > finish. > + ;; Could be an issue with kissat. This could probably be shortened to something like "XXX: main test fails in build container". > + ;; Kissat has no `make install` step, so files are > installed > + ;; manually. This installs the (static) library, the > header and > + ;; the executable. Don't comment the obvious, but more importantly, could we try to make this a shared library? > Kissat is a bare-metal and clean SAT-solver written in C. I wouldn't use "and" as a joiner here. Both "clean, bare-metal SAT solver" and "bare-metal SAT solver" sound a little cleaner 🙂️ Cheers From unknown Sat Jun 14 03:58:11 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#57181] [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat Resent-From: Liliana Marie Prikler Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 15 Aug 2022 13:28:02 +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: Maximilian Heisinger Cc: 57181@debbugs.gnu.org Received: via spool by 57181-submit@debbugs.gnu.org id=B57181.16605700444312 (code B ref 57181); Mon, 15 Aug 2022 13:28:02 +0000 Received: (at 57181) by debbugs.gnu.org; 15 Aug 2022 13:27:24 +0000 Received: from localhost ([127.0.0.1]:41284 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oNa7o-00017U-02 for submit@debbugs.gnu.org; Mon, 15 Aug 2022 09:27:24 -0400 Received: from mail-ej1-f65.google.com ([209.85.218.65]:36704) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oNa7i-00017D-La for 57181@debbugs.gnu.org; Mon, 15 Aug 2022 09:27:22 -0400 Received: by mail-ej1-f65.google.com with SMTP id fy5so13534422ejc.3 for <57181@debbugs.gnu.org>; Mon, 15 Aug 2022 06:27:18 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=content-transfer-encoding:mime-version:user-agent:references :in-reply-to:date:cc:to:from:subject:message-id:from:to:cc; bh=nbfWErX7lv8n4APcaXonAPkKSVYsiEGsvvOEw694bvA=; b=FvcCsRB0Zljbj0oa+fDVUGrDZ49gYBDHVvef1xqCQF+KIls40nL9xID+YpCYeZh2is umxemOQijbE38xP5XOI/vUETRdK8bUXxH7zdxyBK1UeVrz6xMVlYdI/bcHUmbrJWITlr OnGBDS+lo+s4dW6ql2h70SlqR36hHrKVQCbl5BsLfwZnxi+AWfjMf5TzJmKk8BpGSpm2 aJxyCUuzGcfuy0sofgVeAlVfNgFBWsgMR9hKeFk37nuHZXKIQWkAnvIFZsCqkS5i7Mzj 2TgoJFS92SJh1Kk95Vxj7ExBzPqPZ01tM1utVARRcu9f2T78pKEmXWT6tffudJv09O3l MFPQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=content-transfer-encoding:mime-version:user-agent:references :in-reply-to:date:cc:to:from:subject:message-id:x-gm-message-state :from:to:cc; bh=nbfWErX7lv8n4APcaXonAPkKSVYsiEGsvvOEw694bvA=; b=R4r0SAxwRF1+OMBbNyy6jkKjutH2/PRqC5hjvMid4Sje9UFdKBsl1vrTkF2KxPpuwi 8JQtBdf7jeeh0k0RJd1T28HUmhRJXfwMhORcbjjkMPivx/pRpIMwhMh0Rp6O0xsuDctL K+C1j88nl4FLQQcKy2t+MwWFqe+5UOHp0ZIQza3KBPANGQ4TLed07mSld47a5LFlznD5 zJ4sTWwM/x+ZHtcJ+iBz1EW9T2M/tmw3t0/JuE5h7bcO23oMwqozo2fOq+Dju+/RY0Tn 6KxU5E9nd2wz8Jw3QgSwlKjhAbX69QeH6vTjE93+uKU153uJmJFAbQsviTYUCSkdE29d 2A4g== X-Gm-Message-State: ACgBeo0xyxiaBvszz7D4knm5JZD81auBHM7A8/mStXW8SG2WDN/iB9v3 NHJCndQ+/gBZSx6zOXLLVus= X-Google-Smtp-Source: AA6agR6OjrITajdIoQdbfPp2RsiY92k+0jpfYwQjI8QPWNv9aItsvv/ioSliC4YkPqo6amRJaX7odQ== X-Received: by 2002:a17:907:94c3:b0:730:9641:8dd8 with SMTP id dn3-20020a17090794c300b0073096418dd8mr10685280ejc.586.1660570032781; Mon, 15 Aug 2022 06:27:12 -0700 (PDT) Received: from nijino.fritz.box (85-127-52-93.dsl.dynamic.surfer.at. [85.127.52.93]) by smtp.gmail.com with ESMTPSA id wi2-20020a170906fd4200b007308bebce51sm4126696ejb.171.2022.08.15.06.27.12 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 15 Aug 2022 06:27:12 -0700 (PDT) Message-ID: <742d924abc9cfa0b2073c053e229e8ee437704ce.camel@gmail.com> From: Liliana Marie Prikler Date: Mon, 15 Aug 2022 15:27:11 +0200 In-Reply-To: <132482353.134362.1660560630571@ox93.mailbox.org> References: <1dbd4bac9403ed4dd17de75dfc2d210daf2d2ea3.camel@gmail.com> <1840023126.104586.1660505267957@ox93.mailbox.org> <4349f97ccc76a0ee579442c3a4f50b4ba2f4f34c.camel@gmail.com> <132482353.134362.1660560630571@ox93.mailbox.org> Content-Type: text/plain; charset="UTF-8" User-Agent: Evolution 3.42.1 MIME-Version: 1.0 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 (-) Hi, I've pushed kissat with some heavy edits. In particular, I - 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. Am Montag, dem 15.08.2022 um 12:50 +0200 schrieb Maximilian Heisinger: > Hi, > > sorry, doing the correct CC now. > > > Recursive checkout doesn't really sound "mini". > > Oh, there's some history behind the mini...  CryptoMiniSat adds some > stuff commonly needed in cryptography to MiniSat, which is a common > base for many other SAT solvers. I know about the existence of Minisat, but 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? > The library interfaces mimic this and also > +allow IPASIR-esque incremental use, including assumptions. "Incremental solving" sounds easier to understand. > + (inputs (list zlib boost)) > + (native-inputs (list python python-lit)) If you have a Python interface, you probably also need python in inputs, no? Cheers From unknown Sat Jun 14 03:58:11 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#57181] [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat Resent-From: Maximilian Heisinger Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 15 Aug 2022 15:46:02 +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 Marie Prikler Cc: 57181@debbugs.gnu.org Received: via spool by 57181-submit@debbugs.gnu.org id=B57181.166057831228520 (code B ref 57181); Mon, 15 Aug 2022 15:46:02 +0000 Received: (at 57181) by debbugs.gnu.org; 15 Aug 2022 15:45:12 +0000 Received: from localhost ([127.0.0.1]:43892 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oNcH9-0007Pu-A3 for submit@debbugs.gnu.org; Mon, 15 Aug 2022 11:45:12 -0400 Received: from mout-p-201.mailbox.org ([80.241.56.171]:44932) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oNXg9-0003G7-2B for 57181@debbugs.gnu.org; Mon, 15 Aug 2022 06:50:50 -0400 Received: from smtp102.mailbox.org (smtp102.mailbox.org [IPv6:2001:67c:2050:b231:465::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-201.mailbox.org (Postfix) with ESMTPS id 4M5rfH0wxsz9sW1; Mon, 15 Aug 2022 12:50:31 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=maxheisinger.at; s=MBO0001; t=1660560631; 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:references:references; bh=iBuZ12+sMuFFQV6UKVtynI6fRpbZuT/50DuAnPkEgJw=; b=uz+AliQw7BT7Q026zI9cUG0YwHPwvXMjQFL0oJpR7dkQGJgY2EWo3Aq5nBtNz3kI0acifG 6f86asXZa3tVVN+U7gerQktzEMmuKPvv/wUpMn72whX37320Dgvuxx3CQQWlN07XBirVDZ CUt7gD3xLw1KPnYeQTQRiyhIlruJzZWBLYJRE5HphtTyTjZ5GE6A6zRZLwVw/QyY3efYWs yjkfrgX7/I025udrASZCipEuWTLlOccAv9zOcFjTfNB0tt9uBIWk+qYyz2FhguFb+vPaAF vwBMtz5ELq4dEBVBrZarFXf1tw86PlyLEG/M3DNEAPuOKt1PhVeFgm0mHitZjA== Date: Mon, 15 Aug 2022 12:50:30 +0200 (CEST) From: Maximilian Heisinger Message-ID: <132482353.134362.1660560630571@ox93.mailbox.org> In-Reply-To: <4349f97ccc76a0ee579442c3a4f50b4ba2f4f34c.camel@gmail.com> References: <1dbd4bac9403ed4dd17de75dfc2d210daf2d2ea3.camel@gmail.com> <1840023126.104586.1660505267957@ox93.mailbox.org> <4349f97ccc76a0ee579442c3a4f50b4ba2f4f34c.camel@gmail.com> MIME-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha512; protocol="application/pgp-signature"; boundary="----=_Part_134361_1176128590.1660560630570" X-Priority: 3 Importance: Normal X-Rspamd-Queue-Id: 4M5rfH0wxsz9sW1 X-Spam-Score: 0.0 (/) X-Mailman-Approved-At: Mon, 15 Aug 2022 11:45:10 -0400 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.7 (-) ------=_Part_134361_1176128590.1660560630570 Date: Mon, 15 Aug 2022 12:50:30 +0200 (CEST) Content-Type: multipart/mixed; boundary="----=_Part_134358_2072499494.1660560630550" ------=_Part_134358_2072499494.1660560630550 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit Hi, sorry, doing the correct CC now. > Recursive checkout doesn't really sound "mini". Oh, there's some history behind the mini... CryptoMiniSat adds some stuff commonly needed in cryptography to MiniSat, which is a common base for many other SAT solvers. Kissat is "clean" mainly because it is a new solver that completely breaks with the old MiniSat codebase (and it cleans up some stuff, that was done in CaDiCaL, which I also intend to add later, as some features are still missing from Kissat). And MiniSat itself was a nice and minimal implementation containing (back then) the state-of-the-art optimizations. > could we try to make this a shared library? Done. Also updated the text and the commit messages :) Best regards, Max ------=_Part_134358_2072499494.1660560630550 Content-Type: text/x-patch; charset=UTF-8; name=0002-PATCH-gnu-Add-modern-SAT-solver-kissat.patch Content-Transfer-Encoding: base64 Content-Disposition: attachment; filename=0002-PATCH-gnu-Add-modern-SAT-solver-kissat.patch X-Part-Id: eafaf9a9f23a4f0aa7796e370592625b RnJvbSAyYTFhNTE3NjI0MWMyMDYyYjFkNGIxZjM3OWNhNmZiOTQ1ZmI3MDFmIE1vbiBTZXAgMTcg MDA6MDA6MDAgMjAwMQpGcm9tOiBNYXhpbWlsaWFuIEhlaXNpbmdlciA8bWFpbEBtYXhoZWlzaW5n ZXIuYXQ+CkRhdGU6IFN1biwgMTQgQXVnIDIwMjIgMjE6MDk6NTkgKzAyMDAKU3ViamVjdDogW1BB VENIIDIvMl0gUEFUQ0hdIGdudTogQWRkIG1vZGVybiBTQVQgc29sdmVyIGtpc3NhdAoKKiBnbnUv cGFja2FnZXMvbWF0aHMuc2NtIChraXNzYXQpOiBBZGQgcGFja2FnZS4KLS0tCiBnbnUvcGFja2Fn ZXMvbWF0aHMuc2NtIHwgNTUgKysrKysrKysrKysrKysrKysrKysrKysrKysrKysrKysrKysrKysr KysrCiAxIGZpbGUgY2hhbmdlZCwgNTUgaW5zZXJ0aW9ucygrKQoKZGlmZiAtLWdpdCBhL2dudS9w YWNrYWdlcy9tYXRocy5zY20gYi9nbnUvcGFja2FnZXMvbWF0aHMuc2NtCmluZGV4IGY2OWM2Y2U2 ZGUuLjU4MDc1MWU1MTYgMTAwNjQ0Ci0tLSBhL2dudS9wYWNrYWdlcy9tYXRocy5zY20KKysrIGIv Z251L3BhY2thZ2VzL21hdGhzLnNjbQpAQCAtNzM0NSw2ICs3MzQ1LDYxIEBAIChkZWZpbmUtcHVi bGljIGNyeXB0b21pbmlzYXQ1CiAgICAgKGhvbWUtcGFnZSAiaHR0cHM6Ly9naXRodWIuY29tL21z b29zL2NyeXB0b21pbmlzYXQiKQogICAgIChsaWNlbnNlIGxpY2Vuc2U6ZXhwYXQpKSkKIAorKGRl ZmluZS1wdWJsaWMga2lzc2F0CisgIChwYWNrYWdlCisgICAgKG5hbWUgImtpc3NhdCIpCisgICAg KHZlcnNpb24gIjMuMC4wIikKKyAgICAoc291cmNlCisgICAgIChvcmlnaW4KKyAgICAgICAobWV0 aG9kIGdpdC1mZXRjaCkKKyAgICAgICAodXJpIChnaXQtcmVmZXJlbmNlCisgICAgICAgICAgICAg KHVybCAiaHR0cHM6Ly9naXRodWIuY29tL2FybWluYmllcmUva2lzc2F0IikKKyAgICAgICAgICAg ICAoY29tbWl0IChzdHJpbmctYXBwZW5kICJyZWwtIiB2ZXJzaW9uKSkpKQorICAgICAgIChmaWxl LW5hbWUgKGdpdC1maWxlLW5hbWUgbmFtZSB2ZXJzaW9uKSkKKyAgICAgICAoc2hhMjU2CisgICAg ICAgIChiYXNlMzIKKyAgICAgICAgICIwNHg0dzc2MHNyYmRpNHpjaTBzNzQ3cXhrNzE3eDVkMng1 OWl4cmF4aDUxMDRzOW55bjhiIikpKSkKKyAgICAoYnVpbGQtc3lzdGVtIGdudS1idWlsZC1zeXN0 ZW0pCisgICAgKG5hdGl2ZS1pbnB1dHMgKGxpc3QgeHogZ3ppcCBsemlwIGJ6aXAyKSkKKyAgICAo YXJndW1lbnRzCisgICAgIGAoIzp0ZXN0LXRhcmdldCAidGVzdCIKKyAgICAgICAjOnBoYXNlcwor ICAgICAgIChtb2RpZnktcGhhc2VzICVzdGFuZGFyZC1waGFzZXMKKyAgICAgICAgIChyZXBsYWNl ICdjb25maWd1cmUKKyAgICAgICAgICAgKGxhbWJkYSogKCM6a2V5IGNvbmZpZ3VyZS1mbGFncyAj OmFsbG93LW90aGVyLWtleXMpCisgICAgICAgICAgICAgOzsgVGhlIGNvbmZpZ3VyZSBzY3JpcHQg b2Yga2lzc2F0IGlzIGN1c3RvbSBhbmQgZG9lcyBub3Qgc3VwcG9ydAorICAgICAgICAgICAgIDs7 IHN0YW5kYXJkIEdOVSBvcHRpb25zIGxpa2UgQ09ORklHX1NIRUxMLiAgV2UgdGhlcmVmb3JlIG92 ZXJ3cml0ZQorICAgICAgICAgICAgIDs7IHRoZSBkZWZhdWx0LgorICAgICAgICAgICAgIChhcHBs eSBpbnZva2UgIi4vY29uZmlndXJlIiAiLXNoYXJlZCIgY29uZmlndXJlLWZsYWdzKSkpCisgICAg ICAgICAoYWRkLWJlZm9yZSAnY2hlY2sgJ3BhdGNoLXRlc3QKKyAgICAgICAgICAgKGxhbWJkYSog KCM6a2V5IGlucHV0cyBvdXRwdXRzICM6YWxsb3ctb3RoZXIta2V5cykKKyAgICAgICAgICAgICA7 OyAibWFpbiIgdGVzdCBmYWlscyBpbiBidWlsZCBjb250YWluZXIuICBUaGUgbGlzdCBiZWxvdyBp bmNsdWRlcworICAgICAgICAgICAgIDs7IGFsbCB0ZXN0cyBidXQgdGhlIGZhaWxpbmcgb25lLgor ICAgICAgICAgICAgIChzdWJzdGl0dXRlKiAiYnVpbGQvbWFrZWZpbGUiCisgICAgICAgICAgICAg ICAoKCIuL3Rpc3NhdCIpCisgICAgICAgICAgICAgICAgICIuL3Rpc3NhdCBlcnJvciB1dGlsaXRp ZXMgZW5kaWFubmVzcyBjZWlsIGZvcm1hdCByZWZlcmVuY2VzIFxcCitcdHJlbHVjdGFudCByYW5k b20gcXVldWUgYWxsb2NhdGUgYXJyYXkgc3RhY2sgYXJlbmEgaGVhcCB2ZWN0b3IgcmFuayBzb3J0 IGJ1bXAgXFwKK1x0b3B0aW9ucyBjb25maWcgaW5pdCBhZGQgZmlsZSBwYXJzZSBjb2xsZWN0IGtp dHRlbiBzb2x2ZSBjb3ZlcmFnZSB1c2FnZSBcXAorXHR0ZXJtaW5hdGUiKSkpKQorICAgICAgICAg KHJlcGxhY2UgJ2luc3RhbGwKKyAgICAgICAgICAgKGxhbWJkYSogKCM6a2V5IGlucHV0cyBvdXRw dXRzICM6YWxsb3ctb3RoZXIta2V5cykKKyAgICAgICAgICAgICAoaW5zdGFsbC1maWxlCisgICAg ICAgICAgICAgICJidWlsZC9raXNzYXQiCisgICAgICAgICAgICAgIChzdHJpbmctYXBwZW5kIChh c3NvYy1yZWYgb3V0cHV0cyAib3V0IikgIi9iaW4iKSkKKyAgICAgICAgICAgICAoaW5zdGFsbC1m aWxlCisgICAgICAgICAgICAgICJidWlsZC9saWJraXNzYXQuc28iCisgICAgICAgICAgICAgIChz dHJpbmctYXBwZW5kIChhc3NvYy1yZWYgb3V0cHV0cyAib3V0IikgIi9saWIiKSkKKyAgICAgICAg ICAgICAoaW5zdGFsbC1maWxlCisgICAgICAgICAgICAgICJzcmMva2lzc2F0LmgiCisgICAgICAg ICAgICAgIChzdHJpbmctYXBwZW5kIChhc3NvYy1yZWYgb3V0cHV0cyAib3V0IikgIi9pbmNsdWRl L2tpc3NhdCIpKSkpKSkpCisgICAgKGhvbWUtcGFnZSAiaHR0cHM6Ly9naXRodWIuY29tL2FybWlu YmllcmUva2lzc2F0IikKKyAgICAoc3lub3BzaXMgIkJhcmUtbWV0YWwgU0FUIHNvbHZlciIpCisg ICAgKGRlc2NyaXB0aW9uCisgICAgICJLaXNzYXQgaXMgYSBiYXJlLW1ldGFsIFNBVC1zb2x2ZXIg d3JpdHRlbiBpbiBDLiAgSXQgaXMgYSBwb3J0IG9mIENhRGlDYUwKK2JhY2sgdG8gQyB3aXRoIGlt cHJvdmVkIGRhdGEgc3RydWN0dXJlcywgYmV0dGVyIHNjaGVkdWxpbmcgb2YgaW5wcm9jZXNzaW5n IGFuZAorb3B0aW1pemVkIGFsZ29yaXRobXMgYW5kIGltcGxlbWVudGF0aW9uLiIpCisgICAgKGxp Y2Vuc2UgbGljZW5zZTpleHBhdCkpKQorCiAoZGVmaW5lLXB1YmxpYyBsaWJxYWxjdWxhdGUKICAg KHBhY2thZ2UKICAgICAobmFtZSAibGlicWFsY3VsYXRlIikKLS0gCjIuMzcuMQoK ------=_Part_134358_2072499494.1660560630550 Content-Type: text/x-patch; charset=UTF-8; name=0001-PATCH-gnu-Add-modern-SAT-solver-cryptominisat5.patch Content-Transfer-Encoding: base64 Content-Disposition: attachment; filename=0001-PATCH-gnu-Add-modern-SAT-solver-cryptominisat5.patch X-Part-Id: b77d7d7503344b5984ab6033e5c84551 RnJvbSBjMjEyYzQ1MzAwMmYwY2Q3ZTU0N2M5OGY1MTY3MmYyODM4N2RlZjA1IE1vbiBTZXAgMTcg MDA6MDA6MDAgMjAwMQpGcm9tOiBNYXhpbWlsaWFuIEhlaXNpbmdlciA8bWFpbEBtYXhoZWlzaW5n ZXIuYXQ+CkRhdGU6IFN1biwgMTQgQXVnIDIwMjIgMTU6NDA6MDIgKzAyMDAKU3ViamVjdDogW1BB VENIIDEvMl0gW1BBVENIXSBnbnU6IEFkZCBtb2Rlcm4gU0FUIHNvbHZlciBjcnlwdG9taW5pc2F0 NQoKKiBnbnUvcGFja2FnZXMvbWF0aHMuc2NtIChjcnlwdG9taW5pc2F0NSk6IEFkZCBwYWNrYWdl LgotLS0KIGdudS9wYWNrYWdlcy9tYXRocy5zY20gfCAzNCArKysrKysrKysrKysrKysrKysrKysr KysrKysrKysrKysrCiAxIGZpbGUgY2hhbmdlZCwgMzQgaW5zZXJ0aW9ucygrKQoKZGlmZiAtLWdp dCBhL2dudS9wYWNrYWdlcy9tYXRocy5zY20gYi9nbnUvcGFja2FnZXMvbWF0aHMuc2NtCmluZGV4 IGM3OTA1OGFiNDIuLmY2OWM2Y2U2ZGUgMTAwNjQ0Ci0tLSBhL2dudS9wYWNrYWdlcy9tYXRocy5z Y20KKysrIGIvZ251L3BhY2thZ2VzL21hdGhzLnNjbQpAQCAtNzMxMSw2ICs3MzExLDQwIEBAIChk ZWZpbmUtcHVibGljIG1pbmlzYXQKICAgICAgICAiaHR0cDovL21pbmlzYXQuc2UvTWluaVNhdC5o dG1sIikKICAgICAgIChsaWNlbnNlIGxpY2Vuc2U6ZXhwYXQpKSkpCiAKKyhkZWZpbmUtcHVibGlj IGNyeXB0b21pbmlzYXQ1CisgIChwYWNrYWdlCisgICAgKG5hbWUgImNyeXB0b21pbmlzYXQ1IikK KyAgICAodmVyc2lvbiAiNS44LjAiKQorICAgIChzb3VyY2UKKyAgICAgKG9yaWdpbgorICAgICAg IChtZXRob2QgZ2l0LWZldGNoKQorICAgICAgICh1cmkgKGdpdC1yZWZlcmVuY2UKKyAgICAgICAg ICAgICAodXJsICJodHRwczovL2dpdGh1Yi5jb20vbXNvb3MvY3J5cHRvbWluaXNhdCIpCisgICAg ICAgICAgICAgKGNvbW1pdCB2ZXJzaW9uKQorICAgICAgICAgICAgIDs7IFJlY3Vyc2l2ZSBjaGVj a291dCBpcyByZXF1aXJlZCB0byBlbmFibGUgdGVzdGluZy4KKyAgICAgICAgICAgICAocmVjdXJz aXZlPyAjdCkpKQorICAgICAgKGZpbGUtbmFtZSAoZ2l0LWZpbGUtbmFtZSBuYW1lIHZlcnNpb24p KQorICAgICAgKHNoYTI1NgorICAgICAgIChiYXNlMzIKKyAgICAgICAgIjFkejRiNG1qbWJtMmo3 NThsM3k1MjB4OTE4bWg1YjFpYTczeHg2Ynl3MGg5N2t3eXg4enciKSkpKQorICAgIChidWlsZC1z eXN0ZW0gY21ha2UtYnVpbGQtc3lzdGVtKQorICAgIChhcmd1bWVudHMKKyAgICAgKGxpc3QgIzpi dWlsZC10eXBlICJSZWxlYXNlIgorICAgICAgICAgICAjOnRlc3QtdGFyZ2V0ICJ0ZXN0IgorICAg ICAgICAgICAjOmNvbmZpZ3VyZS1mbGFncworICAgICAgICAgICAjfihsaXN0ICItREVOQUJMRV9U RVNUSU5HPU9OIikpKQorICAgIChpbnB1dHMgKGxpc3QgemxpYiBib29zdCkpCisgICAgKG5hdGl2 ZS1pbnB1dHMgKGxpc3QgcHl0aG9uIHB5dGhvbi1saXQpKQorICAgIChzeW5vcHNpcyAiSW5jcmVt ZW50YWwgU0FUIHNvbHZlciIpCisgICAgKGRlc2NyaXB0aW9uCisgICAgICJDcnlwdG9NaW5pU2F0 IGlzIGFuIGluY3JlbWVudGFsIFNBVCBzb2x2ZXIgd2l0aCBib3RoIGNvbW1hbmQgbGluZSBhbmQK K2xpYnJhcnkgKEMrKywgQywgUHl0aG9uKSBpbnRlcmZhY2VzLiAgVGhlIGNvbW1hbmQtbGluZSBp bnRlcmZhY2UgdGFrZXMgYQorQGFjcm9ueW17Q05GLCBDb25qdW5jdGl2ZSBOb3JtYWwgRm9ybX0g YXMgYW4gaW5wdXQgaW4gdGhlIERJTUFDUyBmb3JtYXQgd2l0aAordGhlIGV4dGVuc2lvbiBvZiBY T1IgY2xhdXNlcy4gIFRoZSBsaWJyYXJ5IGludGVyZmFjZXMgbWltaWMgdGhpcyBhbmQgYWxzbwor YWxsb3cgSVBBU0lSLWVzcXVlIGluY3JlbWVudGFsIHVzZSwgaW5jbHVkaW5nIGFzc3VtcHRpb25z LiIpCisgICAgKGhvbWUtcGFnZSAiaHR0cHM6Ly9naXRodWIuY29tL21zb29zL2NyeXB0b21pbmlz YXQiKQorICAgIChsaWNlbnNlIGxpY2Vuc2U6ZXhwYXQpKSkKKwogKGRlZmluZS1wdWJsaWMgbGli cWFsY3VsYXRlCiAgIChwYWNrYWdlCiAgICAgKG5hbWUgImxpYnFhbGN1bGF0ZSIpCi0tIAoyLjM3 LjEKCg== ------=_Part_134358_2072499494.1660560630550-- ------=_Part_134361_1176128590.1660560630570 Content-Type: application/pgp-signature Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename=signature.asc -----BEGIN PGP SIGNATURE----- Version: BCPG v1.65 iQEcBAABCgAGBQJi+iT2AAoJEIhyV2pwqbcQg2MH/32E3TtnAUEQ6cqRYB3CoGb1 n9rpaFa0MC+6ULvZBPy2RV95G0FpAiycwN3ipqJGnaI1YJXiQJlVfTMS+R4H/V0N VDiSWvTZXiMfoEGQoDHjcsQcQF+BaCvIh7SLHnAaxnv2/mF8a1qdf5Jxgxv0m/qt IzP+EhyEps3ZK9t/nxT2O6Xd+whgZ08ht50SJc4rPf/pDQPM+xsDQpRoVPun3v4e K5tr/HOrpMEWhMkAjnARLbzZbt045TBjGqu/YDhre+w2mNqpdr418FUymDC+MbUG xuQ4R3z/PvezLTuDd+r0MKAFvqY1jlgZowSVZgOdwE2mlwIpdpy3rzOGibyWv7w= =r16Z -----END PGP SIGNATURE----- ------=_Part_134361_1176128590.1660560630570-- From unknown Sat Jun 14 03:58:11 2025 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-Spam-Score: -0.7 (/) 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 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.7 (-) --=-=-= 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 --=-=-=-- From unknown Sat Jun 14 03:58:11 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#57181] [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat Resent-From: Liliana Marie Prikler Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Wed, 17 Aug 2022 20:17:02 +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: mail@maxheisinger.at Cc: 57181@debbugs.gnu.org Received: via spool by 57181-submit@debbugs.gnu.org id=B57181.166076737617023 (code B ref 57181); Wed, 17 Aug 2022 20:17:02 +0000 Received: (at 57181) by debbugs.gnu.org; 17 Aug 2022 20:16:16 +0000 Received: from localhost ([127.0.0.1]:53141 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oOPSa-0004QV-AG for submit@debbugs.gnu.org; Wed, 17 Aug 2022 16:16:16 -0400 Received: from mail-ej1-f67.google.com ([209.85.218.67]:39860) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oOPSV-0004QD-IF for 57181@debbugs.gnu.org; Wed, 17 Aug 2022 16:16:15 -0400 Received: by mail-ej1-f67.google.com with SMTP id i14so26422058ejg.6 for <57181@debbugs.gnu.org>; Wed, 17 Aug 2022 13:16:11 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=content-transfer-encoding:mime-version:user-agent:references :in-reply-to:date:cc:to:from:subject:message-id:from:to:cc; bh=nDVyUvwwis9U6SMmOhI0TCdYLQz69XENKTaoozAEQqw=; b=M3PFuiURJBI+0kcTakzNf43bOA9hCdCNaGeKVajdaxF6D+YM1O0GYGvCcl+vmuOdl9 Dt4HWnJeDhIL+2pTeLx7cA/558TnOqgLQsQKmL9gg8H8pDnBMmi+9DSvtJtxy8MCI9iG Cp5q0zaBnJJCfgFF1dVpJxgpfbicbQz3XxwZwAoXgUPTivYW5eH2jYQmJR6X3WEzbWih CzUtFr74i6g080WV9HJVeH0h5E/S+1G2bDO5g9Ws+HgwSh23elsuZCSYbAzmdrAWmZDE rVyQ/qRWlzZ7tKJrcDC3VYWIQk1muRPXoXr/uvbK6YMVF5pJBXSoqdT1fFjaOivjRCOp cbSw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=content-transfer-encoding:mime-version:user-agent:references :in-reply-to:date:cc:to:from:subject:message-id:x-gm-message-state :from:to:cc; bh=nDVyUvwwis9U6SMmOhI0TCdYLQz69XENKTaoozAEQqw=; b=EJhs+Ydb+a9n4plYoS/jWP/tWcGkDDDKI76zeDs4BvRPn8edHVpAjcix3DsNdXy/pI 3wLh+2RzL+XhV2LCvJLX8SykRFAQnabWQ39UeWoKAN5bd1NRBdbAOgVhrLW37yj8bMNE mqSdnNiyIBf4JFofcRVmV0jcntREa8zx3Ek+mu8mnwzcIhJgS3MsGm6uK45oC7N8UhrK BuOyEP3sC/2djuf2dA9dS6NdMUDyLnZ0O05f/G+06lFKx8tPAhglfNxsWfosesqduyWi JA+SyZAaz5u8uRCbGSUDP9IpZLfT9Tivn1Upafh80x5UkUAOo+Ym7qMA2XgW/gqhJhDi dOBw== X-Gm-Message-State: ACgBeo0WBO3X4IJgt/LgyyC5fgJL0WSLNrv++/7n/sxQ3X+Tlc/uB2Pj Oq8g39Udp/Nx5kx5y79qE1k= X-Google-Smtp-Source: AA6agR5+MSqdxBohngMH5441IgqE70/YnLW61bsPZ50W8yUmL430H7W9ackOaGLhAKMbb9m62+MwAA== X-Received: by 2002:a17:906:58c6:b0:731:39e0:3eb8 with SMTP id e6-20020a17090658c600b0073139e03eb8mr18400204ejs.205.1660767365572; Wed, 17 Aug 2022 13:16:05 -0700 (PDT) Received: from nijino.fritz.box (85-127-52-93.dsl.dynamic.surfer.at. [85.127.52.93]) by smtp.gmail.com with ESMTPSA id c21-20020a170906341500b00730cc173c6asm7225308ejb.43.2022.08.17.13.16.04 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Wed, 17 Aug 2022 13:16:04 -0700 (PDT) Message-ID: From: Liliana Marie Prikler Date: Wed, 17 Aug 2022 22:16:03 +0200 In-Reply-To: <87wnb74c7n.fsf@maxheisinger.at> References: <87wnb74c7n.fsf@maxheisinger.at> Content-Type: text/plain; charset="UTF-8" User-Agent: Evolution 3.42.1 MIME-Version: 1.0 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 (-) Hi, Am Mittwoch, dem 17.08.2022 um 08:26 +0200 schrieb mail@maxheisinger.at: > [...] [W]e 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? Only running simple tests is preferable to running no tests at all. If you think that unvendoring everything is an unreasonable amount of work, that's a viable solution. However, we do strive to offer complete packages, so feel free to do 1. :) If you need some pointers as for the test files, ppsspp includes both another package's source (not so great, needs better unvendoring) and test files, and there's probably some other packages you could consult as well. > > "Incremental solving" sounds easier to understand. > > Changed it. LGTM. > > 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). Note that python is now missing from native-inputs, but python-lit is in there. I suppose you need python both as input (for linking) and native-input (to run whatever python-lit is supposed to do). Cheers From unknown Sat Jun 14 03:58:11 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#57181] [PATCH v2 2/4] gnu: Add lingeling. References: <923508243.78855.1660404889221@ox93.mailbox.org> In-Reply-To: <923508243.78855.1660404889221@ox93.mailbox.org> Resent-From: Liliana Marie Prikler Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sat, 15 Oct 2022 14:56:02 +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: 57181@debbugs.gnu.org Cc: mail@maxheisinger.at Received: via spool by 57181-submit@debbugs.gnu.org id=B57181.16658457555030 (code B ref 57181); Sat, 15 Oct 2022 14:56:02 +0000 Received: (at 57181) by debbugs.gnu.org; 15 Oct 2022 14:55:55 +0000 Received: from localhost ([127.0.0.1]:42414 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ojiZu-0001J2-Gj for submit@debbugs.gnu.org; Sat, 15 Oct 2022 10:55:54 -0400 Received: from mail-ej1-f66.google.com ([209.85.218.66]:45663) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ojiZr-0001IE-Cx for 57181@debbugs.gnu.org; Sat, 15 Oct 2022 10:55:53 -0400 Received: by mail-ej1-f66.google.com with SMTP id sc25so16103414ejc.12 for <57181@debbugs.gnu.org>; Sat, 15 Oct 2022 07:55:51 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=mime-version:message-id:content-transfer-encoding:cc:to:subject :date:from:from:to:cc:subject:date:message-id:reply-to; bh=XdPsWsuu0ISBY1mQKc2DJF5HZsHaD5IzR6mOKoUtJe8=; b=ja7XbtSYyz/7LJftClytsi9wZzDu8sYvBix6oRrHVIrUTeLipe7JXiKq8EvBYu6QM7 Qq2kISeuPx0gPZJ0c3TCDt/9O8xUW45fm6SKsS8gC8QL1p5DztLiNJRLtVZ9sGQPMM/3 Iv1YlMBtz2nL8Ug88evvysjMCpFnqnHpGc83RGxBMLmOFDfvw/7abY8Tx3JJmn7aDUHI vZdZK713nVRzjym4rR7njTqgix4+YROQ0BJnQjwLEW/ZkbsaKMyFKaaX6Df0FH89203D sa5hLMwGT06xlzPiGUrc6soFgLzfmXmkGFge+6wA3/k1X+shXSRxmdXmgNcNieQ9w1Qy ySkw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=mime-version:message-id:content-transfer-encoding:cc:to:subject :date:from:x-gm-message-state:from:to:cc:subject:date:message-id :reply-to; bh=XdPsWsuu0ISBY1mQKc2DJF5HZsHaD5IzR6mOKoUtJe8=; b=65/ygXYhJahn8/erIFfVWEc4Tf5MUBeikzYiuUo6wow74foaM7VM+ul1jhGJdvTNFV EAR5+Ze8LOkdRdSf07LZZcKaienHK5k6ZPnN6hwkxk4mMTCnOlUtDIqHb6IRArmIJIaB jtrOe4nio6b4gB+39MjcRKxFs7qycAsYF+gI14oBx51gEs8xKtAvTX8cVsbPO8ytZi5Z NWunAYMm0RpR1rN/uLO6jj8WjzS+PpVMaRTPQDVp7vz0ZJ6/iCpVdyf83ImUnjqfbZvE 8CT5k8MfQcFQ6cyHnuiIn0rZZADqpXr1Qj1FXs2dWHOHYssf8KUjYRPVeneOX4XKnuQ7 5B5w== X-Gm-Message-State: ACrzQf0DZpWEhz2XKDM05NlMevuSg4nYT1prlFZQ0331Bcy8DmtwhC70 RXyUGsXrW7ai+JemypCJw97jJivIfUE= X-Google-Smtp-Source: AMsMyM42XoNDo1JtzJUJYTkqg7XFXo1Oh8zqMbKLOGDnJ7bY141Xspr8vGfF5mxvuz2AMYkDqcpdWg== X-Received: by 2002:a17:907:968e:b0:78d:d4c7:b74f with SMTP id hd14-20020a170907968e00b0078dd4c7b74fmr2282128ejc.727.1665845745814; Sat, 15 Oct 2022 07:55:45 -0700 (PDT) Received: from lumine.fritz.box (85-127-52-93.dsl.dynamic.surfer.at. [85.127.52.93]) by smtp.gmail.com with ESMTPSA id f20-20020a17090631d400b0078a543e9301sm3129583ejf.200.2022.10.15.07.55.45 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sat, 15 Oct 2022 07:55:45 -0700 (PDT) From: Liliana Marie Prikler Date: Sat, 15 Oct 2022 16:45:44 +0200 Content-Transfer-Encoding: 7bit Message-ID: <435c49a1276da39ff1b2a2a6f125f09f2d492ae2.camel@gmail.com> 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 (-) * gnu/packages/maths.scm (lingeling): New variable. --- gnu/packages/maths.scm | 82 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 82 insertions(+) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 1e9d7b8be8..5c8a0fe2ef 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -7429,6 +7429,88 @@ (define-public aiger (license (list license:expat license:bsd-3)))) ; blif2aig +(define-public lingeling + (let ((commit "72d2b13eea5fbd95557a3d0d199cd98dfbdc76ee") + (revision "1")) + (package + (name "lingeling") + (version (git-version "sc2022" revision commit)) + (source (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/arminbiere/lingeling") + (commit commit))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "16s30x8s2cw6icchwm65zj56ph4qwz6i07g3hwkknvajisvjq85c")))) + (build-system gnu-build-system) + (arguments + (list #:test-target "test" + #:modules `((ice-9 match) + ,@%gnu-build-system-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 + '("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") 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)))) + (define-public libqalculate (package (name "libqalculate") -- 2.38.0 From unknown Sat Jun 14 03:58:11 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#57181] [PATCH v2 1/4] gnu: Add aiger. References: <923508243.78855.1660404889221@ox93.mailbox.org> In-Reply-To: <923508243.78855.1660404889221@ox93.mailbox.org> Resent-From: Liliana Marie Prikler Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sat, 15 Oct 2022 14:56:02 +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: 57181@debbugs.gnu.org Cc: mail@maxheisinger.at Received: via spool by 57181-submit@debbugs.gnu.org id=B57181.16658457555037 (code B ref 57181); Sat, 15 Oct 2022 14:56:02 +0000 Received: (at 57181) by debbugs.gnu.org; 15 Oct 2022 14:55:55 +0000 Received: from localhost ([127.0.0.1]:42416 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ojiZu-0001J5-UR for submit@debbugs.gnu.org; Sat, 15 Oct 2022 10:55:55 -0400 Received: from mail-ej1-f65.google.com ([209.85.218.65]:38514) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ojiZr-0001ID-62 for 57181@debbugs.gnu.org; Sat, 15 Oct 2022 10:55:53 -0400 Received: by mail-ej1-f65.google.com with SMTP id fy4so16163205ejc.5 for <57181@debbugs.gnu.org>; Sat, 15 Oct 2022 07:55:51 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=mime-version:message-id:content-transfer-encoding:cc:to:subject :date:from:from:to:cc:subject:date:message-id:reply-to; bh=kuvSxt1n3+tIFGjf6oi1gG/JPRN5V09UHwnJSZLiyNA=; b=p2ENY2hmVLWeAl5ROPjEiDZteE2YboutUlEGYCfioLBkuvT16HuA6tLoglYpVKspr/ bDI/AGVNZTQ12pBSlPnm5a/O2b71QUMlHKFrhYrPJC1j4/l5ejsiZAFEdS+pszSTo5ro pNmIjHHkcCROX107D0913Lwt+DHFRDPkpCkcBnkO1E5gyHH767vHJElRgfGUASaeRHQe fW4/3DN4GNWvJ3tqJWolc8UCMPIyn7b6qM1MUyC/FWXX8ABkyJd2aGwDm103+d6TBXM9 +WHdVXCfE4kDfmhAYpyT35Mgqvl30tSbrj01h4kYGrLduRog1MYt9KmIb+xzz57EunQm J72A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=mime-version:message-id:content-transfer-encoding:cc:to:subject :date:from:x-gm-message-state:from:to:cc:subject:date:message-id :reply-to; bh=kuvSxt1n3+tIFGjf6oi1gG/JPRN5V09UHwnJSZLiyNA=; b=syBCt5ZjAQgpdTbGh0hcc1QGg0aH0OPgD/c0cWb8+4UoNIqZS4Qyz/vii36adUNzli iLAHzgo331VeOxDf0uzx6qUdbumPRCXKisNgBcZz74gYR6864Dc8xgN97XbFLgkipzIu 3cyLD33fW+/+i4mm8DuFk0HQGDXKrgR1iRAihntcwR7Onou8p308B1HMSAZD78rLmVWO 432YjQWY/sxaiBszYIw6mTTQVkf4bfghvNTnkn6AyTVnjdI1jClcs5qi7mXXhhzY8djA J7tM86CQv51m22LHSWqymIHaSkaeKuSaCetFJK5ZaR9eVebQbr3gX7W5u2t5HxdJYQrO A0nA== X-Gm-Message-State: ACrzQf0pQWBn8CSfMEstuPcI8nl+DbostskNkTe0m1HDOiZr3Aq4qV6X ZpPChJtga+vAeFKo36HWXxqdpK+Hcvg= X-Google-Smtp-Source: AMsMyM5uS62PanmOIAiIHnEIU599Uav65Sf9P8LLSobWJacs98uLE0cxRXg859ghxAia58GzauaZ4g== X-Received: by 2002:a17:907:724a:b0:78d:b3bb:9ca7 with SMTP id ds10-20020a170907724a00b0078db3bb9ca7mr2301517ejc.86.1665845745075; Sat, 15 Oct 2022 07:55:45 -0700 (PDT) Received: from lumine.fritz.box (85-127-52-93.dsl.dynamic.surfer.at. [85.127.52.93]) by smtp.gmail.com with ESMTPSA id f20-20020a17090631d400b0078a543e9301sm3129583ejf.200.2022.10.15.07.55.44 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sat, 15 Oct 2022 07:55:44 -0700 (PDT) From: Liliana Marie Prikler Date: Sat, 15 Oct 2022 16:45:33 +0200 Content-Transfer-Encoding: 8bit Message-ID: <754c3ee44aed42ff2e441178d3d3328bfdde15dd.camel@gmail.com> 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 (-) * gnu/packages/maths.scm (aiger): New variable. --- gnu/packages/maths.scm | 54 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 54 insertions(+) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index ffd2a89d2f..1e9d7b8be8 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -55,6 +55,7 @@ ;;; Copyright © 2022 Philip McGrath ;;; Copyright © 2022 Marek Felšöci ;;; Copyright © 2022 vicvbcun +;;; Copyright © 2022 Liliana Marie Prikler ;;; ;;; This file is part of GNU Guix. ;;; @@ -7375,6 +7376,59 @@ (define-public kissat optimized algorithms and implementation.") (license license:expat))) +(define-public aiger + (package + (name "aiger") + (version "1.9.9") + (source (origin + (method url-fetch) + (uri (string-append "http://fmv.jku.at/aiger/aiger-" + version ".tar.gz")) + (sha256 + (base32 + "1ish0dw0nf9gyghxsdhpy1jjiy5wp54c993swp85xp7m6vdx6l0y")))) + (outputs (list "out" "static")) + (build-system gnu-build-system) + (arguments + (list #:tests? #f ; no check target + #:phases + #~(modify-phases %standard-phases + (add-after 'unpack 'patch-source + (lambda* (#:key inputs #:allow-other-keys) + (substitute* "aiger.c" + (("\"(gzip|gunzip)" all cmd) + (string-append + "\"" + (search-input-file inputs (string-append "bin/" cmd))))))) + (add-after 'unpack 'patch-build-files + (lambda* (#:key outputs #:allow-other-keys) + (substitute* "makefile.in" + (("test -d .*") "true") + (("/usr/local") (assoc-ref outputs "out"))))) + (replace 'configure + (lambda* (#:key configure-flags #:allow-other-keys) + (apply invoke "./configure.sh" configure-flags))) + (add-after 'install 'install-static + (lambda* (#:key outputs #:allow-other-keys) + (apply invoke #$(ar-for-target) "rcs" "libaiger.a" + (find-files "." "\\.o$")) + (let* ((static (assoc-ref outputs "static")) + (lib (string-append static "/lib")) + (incl (string-append static "/include/aiger"))) + (mkdir-p lib) + (mkdir-p incl) + (install-file "libaiger.a" lib) + (for-each (lambda (f) (install-file f incl)) + (find-files "." "\\.h$")))))))) + (inputs (list gzip)) + (home-page "http://fmv.jku.at/aiger") + (synopsis "Utilities for And-Inverter Graphs") + (description "AIGER is a format, library and set of utilities for +@acronym{AIG, And-Inverter Graphs}s. The focus is on conversion utilities and a +generic reader and writer API.") + (license (list license:expat + license:bsd-3)))) ; blif2aig + (define-public libqalculate (package (name "libqalculate") -- 2.38.0 From unknown Sat Jun 14 03:58:11 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#57181] [PATCH v2 3/4] gnu: Add louvain-community. References: <923508243.78855.1660404889221@ox93.mailbox.org> In-Reply-To: <923508243.78855.1660404889221@ox93.mailbox.org> Resent-From: Liliana Marie Prikler Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sat, 15 Oct 2022 14:56:03 +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: 57181@debbugs.gnu.org Cc: mail@maxheisinger.at Received: via spool by 57181-submit@debbugs.gnu.org id=B57181.16658457555045 (code B ref 57181); Sat, 15 Oct 2022 14:56:03 +0000 Received: (at 57181) by debbugs.gnu.org; 15 Oct 2022 14:55:55 +0000 Received: from localhost ([127.0.0.1]:42418 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ojiZv-0001JC-Eh for submit@debbugs.gnu.org; Sat, 15 Oct 2022 10:55:55 -0400 Received: from mail-ed1-f66.google.com ([209.85.208.66]:37860) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ojiZs-0001IL-9I for 57181@debbugs.gnu.org; Sat, 15 Oct 2022 10:55:53 -0400 Received: by mail-ed1-f66.google.com with SMTP id m16so10437815edc.4 for <57181@debbugs.gnu.org>; Sat, 15 Oct 2022 07:55:52 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=mime-version:message-id:content-transfer-encoding:cc:to:subject :date:from:from:to:cc:subject:date:message-id:reply-to; bh=4hpSVGl1F+FaOIyMOKJ0vdwcz+Qm6QRweUTz1okhAuo=; b=C1lZV0jeEH5D0J6GOegkX0fexBxBfvgoAic9SuGCkSFPysnYvRJWPD5NLelUhh2TsG MoG7f1V+koTXvBedEcc6iXB23dxyHwIhS9SH3QG0mJ/yEnVzoG/Kmf6Pf1pwkYlAwI+d aNSJUDxYPhr0fZLB5lM1afhY0FuUpInTwh93nE0mw9DzcSZttvOHylGRpLgu0x1aTM7M nnnnfW4DD/zVpYDvlgZeStaJx1XHm9TdLTcNdgXa5TLyWoYLtjSU4glVgVdnO4jnvkSc ChFs4YZu9nmVCUDxa8EV2q31ee+nLYSWresB2g5tdxggICi0htCHOzkJWw3KJqqGC4VK pCOg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=mime-version:message-id:content-transfer-encoding:cc:to:subject :date:from:x-gm-message-state:from:to:cc:subject:date:message-id :reply-to; bh=4hpSVGl1F+FaOIyMOKJ0vdwcz+Qm6QRweUTz1okhAuo=; b=gZJycAhezOqi4mO3W1lbvPEufXmpkQPgm4L5yoW0Rs7L3tCxB5abFVz9M7B4EQFcnQ fDL9qrSZ0Hbd5OgWwLGXgY15I+wCWIkfrCTh7um6VuWmo1Uzhd47RoDCnoURQQot6dSb t2kTSHXWf+5LjRGPIKJlkEUKyISmNwjdCACrBhhYrhQ+PuBFCieAR6Dw+2b560MpzBA5 MJUmAdurJ2iMeuhIk4YdUUAWMDLY+KH9cr0K3K+kJMv2BTMc72ejuJeW79j/k14UL/+c ujYjw2L4S8fpVgJ9RlcNEGSySVE5464+JJa81+gvpfzUTx9ZYUHLNh0+IKWoboBFtwjL lQYQ== X-Gm-Message-State: ACrzQf3SKk3SycKUxgrTYUDRtVBYoy0l/0/1CA1ChGPce/6AgczBHIIL Rzh0aAL3ch41Meinc8S+NxCgf6A5Qn4= X-Google-Smtp-Source: AMsMyM4ZwfNh0nZAvRK1Tfep0a1L5XOU1mFYpjMGxq56+oDeKX6gxaZ5/ajfgjOmiit0tH9lTnNR1g== X-Received: by 2002:a05:6402:26c5:b0:45d:21fc:19e4 with SMTP id x5-20020a05640226c500b0045d21fc19e4mr2607838edd.117.1665845746475; Sat, 15 Oct 2022 07:55:46 -0700 (PDT) Received: from lumine.fritz.box (85-127-52-93.dsl.dynamic.surfer.at. [85.127.52.93]) by smtp.gmail.com with ESMTPSA id f20-20020a17090631d400b0078a543e9301sm3129583ejf.200.2022.10.15.07.55.45 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sat, 15 Oct 2022 07:55:46 -0700 (PDT) From: Liliana Marie Prikler Date: Sat, 15 Oct 2022 16:46:40 +0200 Content-Transfer-Encoding: 7bit Message-ID: <70d4e4d117d08591f8b722c46f6891298e71485c.camel@gmail.com> 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 (-) * gnu/packages/maths.scm (louvain-community): New variable. --- gnu/packages/maths.scm | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 5c8a0fe2ef..58faa6674b 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -7511,6 +7511,37 @@ (define-public lingeling also included.") (license license:expat)))) +(define-public louvain-community + (let ((commit "8cc5382d4844af127b1c1257373740d7e6b76f1e") + (revision "1")) + (package + (name "louvain-community") + (version (git-version "1.0.0" revision commit)) + (source (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/meelgroup/louvain-community") + (commit commit))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "1ss00hkdvr9bdkd355hxf8zd7xycb3nm8qpy7s75gjjf6yng0bfj")))) + (build-system cmake-build-system) + (arguments + (list #:tests? #f ; tests appear to require missing files + #:phases + #~(modify-phases %standard-phases + (add-after 'unpack 'encode-git-hash + (lambda _ + (substitute* "CMakeLists.txt" + (("GIT-hash-notfound") #$commit))))))) + (native-inputs (list python)) + (home-page "https://github.com/meelgroup/louvain-communities") + (synopsis "Multi-criteria community detection") + (description "This package provides a C++ implementation of the Louvain +community detection algorithm.") + (license license:lgpl3+)))) + (define-public libqalculate (package (name "libqalculate") -- 2.38.0 From unknown Sat Jun 14 03:58:11 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#57181] [PATCH v2 4/4] gnu: Add cryptominisat. References: <923508243.78855.1660404889221@ox93.mailbox.org> In-Reply-To: <923508243.78855.1660404889221@ox93.mailbox.org> Resent-From: Liliana Marie Prikler Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sat, 15 Oct 2022 14:56:03 +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: 57181@debbugs.gnu.org Cc: mail@maxheisinger.at Received: via spool by 57181-submit@debbugs.gnu.org id=B57181.16658457565051 (code B ref 57181); Sat, 15 Oct 2022 14:56:03 +0000 Received: (at 57181) by debbugs.gnu.org; 15 Oct 2022 14:55:56 +0000 Received: from localhost ([127.0.0.1]:42420 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ojiZv-0001JK-Ou for submit@debbugs.gnu.org; Sat, 15 Oct 2022 10:55:56 -0400 Received: from mail-ej1-f68.google.com ([209.85.218.68]:34732) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ojiZs-0001IR-Sj for 57181@debbugs.gnu.org; Sat, 15 Oct 2022 10:55:54 -0400 Received: by mail-ej1-f68.google.com with SMTP id ot12so16207276ejb.1 for <57181@debbugs.gnu.org>; Sat, 15 Oct 2022 07:55:52 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=mime-version:message-id:content-transfer-encoding:cc:to:subject :date:from:from:to:cc:subject:date:message-id:reply-to; bh=Z1IGjcsbRUZbjBdJTcSrD6Rgzp/fUbn+8c4vSLM0pX8=; b=nOm/5WicCkQk5ciZJCLXTFQhadBWWNlLB9cHx5leqeavruBkEKFmoi9JpHdkkfMTUX /d832YaN7QUTrfVNAw0Rt6aulBeLMf8Zpn2Fh3HRLvq6hJffX3KO2eUD5iVbF9MtmL+z OCrIwJ76WHOWwFQ7oqCAU8yZ3x4lPqxBm7kYfo2PhFM4x+GirY175x+Pud54nKoBpeSu Kp1jidElX7q2LOmGyOkYfePu8Tt3+vtDnfUfS5I4iHTv135WpkbV6Wa5NlcJijNPiUOU TAFmtbuHlcbQUkB0RRnYnIx9NvW3WCtZ9i+gkD30w+yGM4bHt0SYWWfCghaBmfujqkfn EqsQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=mime-version:message-id:content-transfer-encoding:cc:to:subject :date:from:x-gm-message-state:from:to:cc:subject:date:message-id :reply-to; bh=Z1IGjcsbRUZbjBdJTcSrD6Rgzp/fUbn+8c4vSLM0pX8=; b=vd/tthEHNpahN/+nCzDkRshDhRV7QwIU0DfydGJQenuFhQ6DzObu3qb7Gjajgyk6gH mhNcWywh9gL0v8OAowqPvZbGtcAqLrcXq692EOO0YeaCJaTmtDUSiPma3lvjp/KHEqms zq20FmPZuS5uMgUrOlGBNKjJrYKB6s0cZk1gKX+owlKnC3F6urVgWxHXX0azrPWOwlMm u6F7Tu4AKecDv7rVVrozlhHPjKfl2qMcRkmPd16mD+XtUjyXl9Be726gi6SqA/6zckep BvELTyTYGPu3TzDHRYwtE3+5SHcMqJHPezaz+v2+3O1hWkDQjxqYzsXm5BvKE6fdnZdM RMCQ== X-Gm-Message-State: ACrzQf33IIk1+9f93ZU2FSGUrdjHFFppWlTom8+gbw8kWB8DqEIloxUI Ga9QMqwX4sebdtPMb6mGS48OO849nfU= X-Google-Smtp-Source: AMsMyM6E34ZPGbiU8sgUqy093Q9oVgBSDdHTi/XP7EFbMfiN9Sme0GPh1NoDwuHS/mG30n55zZ9KVA== X-Received: by 2002:a17:907:968e:b0:78d:d68d:6751 with SMTP id hd14-20020a170907968e00b0078dd68d6751mr2257485ejc.403.1665845747271; Sat, 15 Oct 2022 07:55:47 -0700 (PDT) Received: from lumine.fritz.box (85-127-52-93.dsl.dynamic.surfer.at. [85.127.52.93]) by smtp.gmail.com with ESMTPSA id f20-20020a17090631d400b0078a543e9301sm3129583ejf.200.2022.10.15.07.55.46 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sat, 15 Oct 2022 07:55:46 -0700 (PDT) From: Liliana Marie Prikler Date: Sat, 15 Oct 2022 16:47:03 +0200 Content-Transfer-Encoding: 8bit Message-ID: <72146c36adf1eddc32377307b8855038b53e8cba.camel@gmail.com> 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 (-) * gnu/packages/maths.scm (cryptominisat): New variable. Co-authored-by: Maximilian Heisinger --- gnu/packages/maths.scm | 51 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 58faa6674b..9db28239fd 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -56,6 +56,7 @@ ;;; Copyright © 2022 Marek Felšöci ;;; Copyright © 2022 vicvbcun ;;; Copyright © 2022 Liliana Marie Prikler +;;; Copyright © 2022 Maximilian Heisinger ;;; ;;; This file is part of GNU Guix. ;;; @@ -159,6 +160,7 @@ (define-module (gnu packages maths) #:use-module (gnu packages serialization) #:use-module (gnu packages shells) #:use-module (gnu packages sphinx) + #:use-module (gnu packages sqlite) #:use-module (gnu packages swig) #:use-module (gnu packages tcl) #:use-module (gnu packages texinfo) @@ -7542,6 +7544,55 @@ (define-public louvain-community community detection algorithm.") (license license:lgpl3+)))) +(define-public cryptominisat + (package + (name "cryptominisat") + (version "5.11.4") + (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 + "1izjn44phjp9670s7bxrdx4p0r59idqwv3bm6sr0qnlqlha5z4zc")))) + (build-system cmake-build-system) + (arguments + (list + #:build-type "Release" + #:test-target "test" + #:configure-flags #~(list "-DENABLE_TESTING=ON" "-DSTATS=ON") + #: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)") + (("add_subdirectory\\(\\$\\{PROJECT_SOURCE_DIR\\}/utils/.*\\)") + ""))))))) + (inputs (list boost louvain-community python python-numpy sqlite zlib)) + (native-inputs (list googletest lingeling python python-wrapper python-lit)) + (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 with +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 libqalculate (package (name "libqalculate") -- 2.38.0 From unknown Sat Jun 14 03:58:11 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: Maximilian Heisinger Subject: bug#57181: closed (Re: [PATCH v2 4/4] gnu: Add cryptominisat.) Message-ID: References: <4f47de966a995ce3dca2cd4b8f4256b032730e14.camel@gmail.com> <923508243.78855.1660404889221@ox93.mailbox.org> X-Gnu-PR-Message: they-closed 57181 X-Gnu-PR-Package: guix-patches X-Gnu-PR-Keywords: patch Reply-To: 57181@debbugs.gnu.org Date: Sat, 26 Nov 2022 13:16:02 +0000 Content-Type: multipart/mixed; boundary="----------=_1669468562-4267-1" This is a multi-part message in MIME format... ------------=_1669468562-4267-1 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" Your bug report #57181: [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat 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 57181@debbugs.gnu.org. --=20 57181: https://debbugs.gnu.org/cgi/bugreport.cgi?bug=3D57181 GNU Bug Tracking System Contact help-debbugs@gnu.org with problems ------------=_1669468562-4267-1 Content-Type: message/rfc822 Content-Disposition: inline Content-Transfer-Encoding: 7bit Received: (at 57181-done) by debbugs.gnu.org; 26 Nov 2022 13:15:45 +0000 Received: from localhost ([127.0.0.1]:38156 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oyv21-0000nE-BJ for submit@debbugs.gnu.org; Sat, 26 Nov 2022 08:15:45 -0500 Received: from mail-wr1-f66.google.com ([209.85.221.66]:36851) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oyv1y-0000WF-QR for 57181-done@debbugs.gnu.org; Sat, 26 Nov 2022 08:15:43 -0500 Received: by mail-wr1-f66.google.com with SMTP id z4so10354892wrr.3 for <57181-done@debbugs.gnu.org>; Sat, 26 Nov 2022 05:15:42 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=mime-version:user-agent:content-transfer-encoding:references :in-reply-to:date:cc:to:from:subject:message-id:from:to:cc:subject :date:message-id:reply-to; bh=j0Pz8efDdRqmIrfEueRiAjuuTIcWACn2nP4r/B/0V3A=; b=IX3YGJib5fbv30PgMzDCJSGepIYmFRqlTnNAMfPduVPu0Lcub/VSFD5gEMV22nYs/b U+EW7+TxC8U5Buxg+LW3AzMFoXiTl/qBjTvT4YEKT/sXSVJoQvnZP/tPU4my0jOzo6oV 6O2hxb3f8QLa+B4Ayc9VYf53rMWilpSXIN6orcAOOgEw8vPZID8q9gHEva4H3d/DIVXq /JsynCDrjd0tX6Zkwq+Sd8SLiCKS2Oh7DI/rmrXkBAtnr6oq5YhI/3warI10lSt7M4bo eEvrG4/33R8hkmAr6huzFCejGvYT9Hsixl1y3tK0eFPLAxOh6Cz7oUwrht+H8IOAHb2P AWSg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=mime-version:user-agent:content-transfer-encoding:references :in-reply-to:date:cc:to:from:subject:message-id:x-gm-message-state :from:to:cc:subject:date:message-id:reply-to; bh=j0Pz8efDdRqmIrfEueRiAjuuTIcWACn2nP4r/B/0V3A=; b=p7xPLfV3edu08S2vjazHDCvP1YPVj7hb4w/1Gfh9YxXukb6EMCn8NKjFge7SzPc/kD uv3jyE8I69wpfFayrvdAGtI4vxEcvS6a4JeIoWsGYyBfYTM6oe77F+0M09xyWf8NtiGF 3NQU93JoIeo+mHMTOvh5VxfyRQ5tf97u8MrYG3uePtK2DbQ/+gre07cx5Cv5j2/cpDqo 72cyxAr+2jZ4kCfdPWvJh/yGlMGoeYWOMg4poJxEHSqv803fke/UaDeFNrnKmbrl/eNv 8HyObd/H7hsXXiARXkz0Bv07Z3HFECHgRUId2v9RlfmHqJWKEoqEoHOMXto0GC36qnvC BFPA== X-Gm-Message-State: ANoB5pkjKGt540x4xuu5eLoCgn0DsUYIRnAwdT0Q81GV3H04A82Lu6rp g/bVBIoUTk4P81eBXkAeqVSWQJgnK5Q= X-Google-Smtp-Source: AA0mqf4PG8JdhZ/9tmavB6jqInYvjKebJBx/Iy4YMC+rf23BO4YrCXFau4TlDmXFfEy3PETLgq3H9Q== X-Received: by 2002:a5d:4568:0:b0:241:e8b0:cdcc with SMTP id a8-20020a5d4568000000b00241e8b0cdccmr12349743wrc.581.1669468537000; Sat, 26 Nov 2022 05:15:37 -0800 (PST) Received: from lumine.fritz.box (85-127-52-93.dsl.dynamic.surfer.at. [85.127.52.93]) by smtp.gmail.com with ESMTPSA id q4-20020adff944000000b002366c3eefccsm6053720wrr.109.2022.11.26.05.15.36 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sat, 26 Nov 2022 05:15:36 -0800 (PST) Message-ID: <4f47de966a995ce3dca2cd4b8f4256b032730e14.camel@gmail.com> Subject: Re: [PATCH v2 4/4] gnu: Add cryptominisat. From: Liliana Marie Prikler To: 57181-done@debbugs.gnu.org Date: Sat, 26 Nov 2022 14:15:35 +0100 In-Reply-To: <72146c36adf1eddc32377307b8855038b53e8cba.camel@gmail.com> References: <72146c36adf1eddc32377307b8855038b53e8cba.camel@gmail.com> Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable User-Agent: Evolution 3.46.0 MIME-Version: 1.0 X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 57181-done Cc: mail@maxheisinger.at 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 Samstag, dem 15.10.2022 um 16:47 +0200 schrieb Liliana Marie Prikler: > * gnu/packages/maths.scm (cryptominisat): New variable. >=20 > Co-authored-by: Maximilian Heisinger Aaaand it's pushed. ------------=_1669468562-4267-1 Content-Type: message/rfc822 Content-Disposition: inline Content-Transfer-Encoding: 7bit Received: (at submit) by debbugs.gnu.org; 13 Aug 2022 16:56:50 +0000 Received: from localhost ([127.0.0.1]:34975 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oMuRL-0006LE-1y for submit@debbugs.gnu.org; Sat, 13 Aug 2022 12:56:50 -0400 Received: from lists.gnu.org ([209.51.188.17]:44812) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oMtAP-0004Gq-0h for submit@debbugs.gnu.org; Sat, 13 Aug 2022 11:35:16 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:52886) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1oMtAD-0001AW-Co for guix-patches@gnu.org; Sat, 13 Aug 2022 11:35:04 -0400 Received: from mout-p-202.mailbox.org ([80.241.56.172]:56256) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_CHACHA20_POLY1305:256) (Exim 4.90_1) (envelope-from ) id 1oMtA8-0006Nf-MM for guix-patches@gnu.org; Sat, 13 Aug 2022 11:35:01 -0400 Received: from smtp2.mailbox.org (smtp2.mailbox.org [10.196.197.2]) (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 4M4l3F5VTBz9sTh for ; Sat, 13 Aug 2022 17:34:49 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=maxheisinger.at; s=MBO0001; t=1660404889; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version:content-type:content-type; bh=ugBfwExP9pqFp7Fzh18MxqZ3yTZmZOQ14UZnKuDRyXU=; b=JZVb1JsP8hkcK0KrIFuooT02Cx5orqlCPg5JHFaaLFCEMhAnmCokkN24ZvgPN1WjzRp+qA gydxKgHjFetpUdXZc+N3x+VgnPl6h/Tz6QchuIRWLL/U6CvWhO+IWbmO8WM6hSoxy3NGuX g7R+2dKePPlU7xsq0yapyUn6EwoossFtns8rWE2xHHxT4f+5Jq5SI11agUNfxPVeAmc9W2 /3DuTXnTa2COzymvU7pJbKKULHXzLPI/z9fcgPyeXIuzJM6HGmakzu2mcLW003eLUkBBfM 14SJQwQB6RPb/GYX3HJFSJP2t0Yezljf3X9bE7hGHsEohBPyooqFsMw8Qau3zg== Date: Sat, 13 Aug 2022 17:34:49 +0200 (CEST) From: Maximilian Heisinger To: "guix-patches@gnu.org" Message-ID: <923508243.78855.1660404889221@ox93.mailbox.org> Subject: [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat MIME-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha512; protocol="application/pgp-signature"; boundary="----=_Part_78854_1462168451.1660404889220" X-Priority: 3 Importance: Normal Received-SPF: pass client-ip=80.241.56.172; envelope-from=mail@maxheisinger.at; helo=mout-p-202.mailbox.org X-Spam_score_int: -27 X-Spam_score: -2.8 X-Spam_bar: -- X-Spam_report: (-2.8 / 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_DNSWL_LOW=-0.7, SPF_HELO_NONE=0.001, SPF_PASS=-0.001, T_SCC_BODY_TEXT_LINE=-0.01 autolearn=ham autolearn_force=no X-Spam_action: no action X-Spam-Score: -1.3 (-) X-Debbugs-Envelope-To: submit X-Mailman-Approved-At: Sat, 13 Aug 2022 12:56:45 -0400 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: -2.3 (--) ------=_Part_78854_1462168451.1660404889220 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit >From dea29e40c0cfb5eaac49060082fe63c0ed1e08b7 Mon Sep 17 00:00:00 2001 From: Maximilian Heisinger Date: Sat, 13 Aug 2022 17:23:59 +0200 Subject: [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat * gnu/packages/maths.scm (cryptominisat5): Add package. * gnu/packages/maths.scm (kissat): Add package. --- gnu/packages/maths.scm | 64 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 64 insertions(+) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index c79058ab42..4a58b9eb3f 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -7311,6 +7311,70 @@ (define-public minisat "http://minisat.se/MiniSat.html") (license license:expat)))) +(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 `(#:tests? #false)) + (inputs (list zlib boost)) + (synopsis "Advanced incremental SAT solver") + (description + "Provides CryptoMiniSat, an advanced incremental SAT solver. The system +has 3 interfaces: command-line, C++ library and python. The command-line +interface takes a cnf as an input in the DIMACS format with the extension of +XOR clauses. The C++ and python interface mimics this and also allows for +incremental use: assumptions and multiple solve calls. A C compatible wrapper +is also provided.") + (home-page "https://github.com/msoos/cryptominisat") + (license license:expat))) + +(define-public kissat + (package + (name "kissat") + (version "3.0.0") + (source + (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/arminbiere/kissat") + (commit (string-append "rel-" version)))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "04x4w760srbdi4zci0s747qxk717x5d2x59ixraxh5104s9nyn8b")))) + (build-system gnu-build-system) + (arguments + `(#:tests? #f + #:phases + (modify-phases %standard-phases + (replace 'configure + (lambda* (#:key outputs #:allow-other-keys) + (invoke "./configure"))) + (replace 'install + (lambda* (#:key inputs outputs #:allow-other-keys) + (install-file + "build/kissat" + (string-append (assoc-ref outputs "out") "/bin"))))))) + (home-page "https://github.com/arminbiere/kissat") + (synopsis "Bare-metal SAT solver after the KISS principle principle +written in C") + (description + "Kissat is a \"keep it simple and clean bare metal SAT solver\" written +in C. It is a port of CaDiCaL back to C with improved data structures, better +scheduling of inprocessing and optimized algorithms and implementation.") + (license license:gpl3+))) + (define-public libqalculate (package (name "libqalculate") -- 2.37.1 ------=_Part_78854_1462168451.1660404889220 Content-Type: application/pgp-signature Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename=signature.asc -----BEGIN PGP SIGNATURE----- Version: BCPG v1.65 iQEcBAABCgAGBQJi98SZAAoJEIhyV2pwqbcQW1UH/ijwpo9WkbAbaJ+oW5YBz9K9 ogx65DSyABAtwd5z0wyKvERSBuSB/z0W4jeOjwrCIXCDIV1aDlHR6WHVvfIUgLk0 7GtiwnZW6nCnAYQBP8Zm7WdeEAucrhops5JDTzk/evI5rwJceC396yVH4lBv+3Q9 VRPDlQI/kQ3gPsXjIUbpUFSY8zQM5Dp1EPp2IaVteuy0r42XHET/hQLOuKK8BXwt rnfFlu3RcdfbKHH/2xTaIEwHeLp3FdmAZeMNuHdDEls2LY14lYSQEQeP4uVKk66m Wo29zupk86eDWsvMqjP8Ic1Jj0GA33XlajEH5ail4ymtMRITiO/74OkjiZPBrgo= =SmL6 -----END PGP SIGNATURE----- ------=_Part_78854_1462168451.1660404889220-- ------------=_1669468562-4267-1-- From unknown Sat Jun 14 03:58:11 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#57181] [PATCH v2 4/4] gnu: Add cryptominisat. Resent-From: Maximilian Heisinger Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 27 Nov 2022 17:53:02 +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 Marie Prikler , "57181@debbugs.gnu.org" <57181@debbugs.gnu.org> Received: via spool by 57181-submit@debbugs.gnu.org id=B57181.166957157127747 (code B ref 57181); Sun, 27 Nov 2022 17:53:02 +0000 Received: (at 57181) by debbugs.gnu.org; 27 Nov 2022 17:52:51 +0000 Received: from localhost ([127.0.0.1]:43349 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ozLpi-0007DO-G3 for submit@debbugs.gnu.org; Sun, 27 Nov 2022 12:52:50 -0500 Received: from mout-p-102.mailbox.org ([80.241.56.152]:59390) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ozLll-0007B9-U0 for 57181@debbugs.gnu.org; Sun, 27 Nov 2022 12:48:47 -0500 Received: from smtp1.mailbox.org (smtp1.mailbox.org [IPv6:2001:67c:2050:b231:465::1]) (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-102.mailbox.org (Postfix) with ESMTPS id 4NKx0j5Qxhz9sJB; Sun, 27 Nov 2022 18:48:37 +0100 (CET) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=maxheisinger.at; s=MBO0001; t=1669571317; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version:content-type:content-type: in-reply-to:in-reply-to:references:references; bh=bN2ZsO3kVa5W32w/YvURzxrH4nv5Btr8UJY7PPEIoNc=; b=lLqCJpX+QPqF76TIO+sBcZhRw6OCjwfoO5Jm4O2gzzWZ+VDI0tdqmbs9dIDVoZm4pAfpEZ KWjxwDU9lLUMkVI62EIfZFHI+iehQmdjvX+UC2V16yUS/wekhCxQYOW+Q5lxdSn+Jy66Gw 5sT2y26YiY0ZmjmU+6vV20PBsyT3CQvWXaNoYjCtJ7eP/4NgHWwvCat1Q1jH7yeLJGbh15 4zcvqAfEuA5pdYLjZnh+YxgKQkzj4r1vbtwkPS61UTYF+6ELrfNQmg4akYNwE1YsnZLSma 2CHH1FP5lRYWKS3oIM7tUzEMmbQr4doaMiaZ1F9KHCih4h1DmoEcD9B66lAqfQ== Date: Sun, 27 Nov 2022 18:48:37 +0100 (CET) From: Maximilian Heisinger Message-ID: <2043553104.672393.1669571317340@ox93.mailbox.org> In-Reply-To: <4f47de966a995ce3dca2cd4b8f4256b032730e14.camel@gmail.com> References: <72146c36adf1eddc32377307b8855038b53e8cba.camel@gmail.com> <4f47de966a995ce3dca2cd4b8f4256b032730e14.camel@gmail.com> MIME-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha512; protocol="application/pgp-signature"; boundary="----=_Part_672392_1810064204.1669571317340" X-Priority: 3 Importance: Normal X-Rspamd-Queue-Id: 4NKx0j5Qxhz9sJB X-Spam-Score: -0.7 (/) X-Mailman-Approved-At: Sun, 27 Nov 2022 12:52:47 -0500 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.7 (-) ------=_Part_672392_1810064204.1669571317340 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit > Liliana Marie Prikler hat am 26.11.2022 14:15 CET geschrieben: > > Aaaand it's pushed. Thank you so much! Sorry for not working on the patch in the meantime, I started doing this while at a conference and was completely wrapped up in other issues and some deadlines after coming back... This is a beautiful patch series and I am looking forward to being able to coming up with such constructs myself. Integrating libraries like this is really interesting and opens up quite a few possibilities for research, especially with preserving old releases and making them comparable. Thanks again, and I'm looking forward to future submissions! They will be bottom-up next time :) Best regards, Max ------=_Part_672392_1810064204.1669571317340 Content-Type: application/pgp-signature Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename=signature.asc -----BEGIN PGP SIGNATURE----- Version: BCPG v1.65 iQEcBAABCgAGBQJjg6L1AAoJEIhyV2pwqbcQ4IoIAKD/DM1ZCP4u3FNziV0J4Cyo /avci2wQIC4UHUKKY/437ZOvtfdaGXSKTUkOHVXiSq96KCDCxEYmzHY4JVGBL35T ndvKNWdaskrpjcq0hdxs923nxz4SkftObEmrsChnZt6AGT7n7SbG6899RN0Wyst0 HeM+9H/CcGYlPtTe5qQ1+hP+BNaLkuVp+DxbLfOftTQDlapVL3cCOHj3jhVcWXc7 yNFJcKa8S5k1i2JMFaWG4gzl0WVMVGG/IoO16gghNSGYepdw7AYX1zuMPUXLD1Ae sqiGJ3FFl3CN9aOT1QKTcqVa+MP9Eeu5J28V9ufmjhIaGFfwSl81KiwDmU9OzME= =gkaT -----END PGP SIGNATURE----- ------=_Part_672392_1810064204.1669571317340--