From patchwork Sat Aug 13 15:34:49 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Maximilian Heisinger X-Patchwork-Id: 41609 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id 98FA227BBEA; Sat, 13 Aug 2022 17:58:23 +0100 (BST) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-2.7 required=5.0 tests=BAYES_00,DKIM_INVALID, DKIM_SIGNED,MAILING_LIST_MULTI,SPF_HELO_PASS,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id 0A95327BBE9 for ; Sat, 13 Aug 2022 17:58:23 +0100 (BST) Received: from localhost ([::1]:54456 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1oMuSs-0006Ww-7V for patchwork@mira.cbaines.net; Sat, 13 Aug 2022 12:58:22 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:36102) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1oMuRd-0005mY-CS for guix-patches@gnu.org; Sat, 13 Aug 2022 12:57:05 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:45229) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1oMuRb-0001O3-Ur for guix-patches@gnu.org; Sat, 13 Aug 2022 12:57:05 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1oMuRb-0006M9-Qm for guix-patches@gnu.org; Sat, 13 Aug 2022 12:57:03 -0400 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 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-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 X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches 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(+) -- 2.37.1 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") From patchwork Sat Oct 15 14:45:44 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Liliana Marie Prikler X-Patchwork-Id: 43424 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id 7A5E727BBEA; Sat, 15 Oct 2022 15:56:24 +0100 (BST) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-3.7 required=5.0 tests=BAYES_00,DKIM_ADSP_CUSTOM_MED, DKIM_INVALID,DKIM_SIGNED,FREEMAIL_FROM,MAILING_LIST_MULTI, RCVD_IN_MSPIKE_H2,SPF_HELO_PASS,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id 9649C27BBE9 for ; Sat, 15 Oct 2022 15:56:23 +0100 (BST) Received: from localhost ([::1]:43500 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ojiaM-0001QA-Fz for patchwork@mira.cbaines.net; Sat, 15 Oct 2022 10:56:22 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:37808) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1ojia2-0001Pi-Su for guix-patches@gnu.org; Sat, 15 Oct 2022 10:56:02 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:43342) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1ojia2-0000DQ-LB for guix-patches@gnu.org; Sat, 15 Oct 2022 10:56:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ojia2-0001Jj-GZ for guix-patches@gnu.org; Sat, 15 Oct 2022 10:56:02 -0400 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 Message-ID: <435c49a1276da39ff1b2a2a6f125f09f2d492ae2.camel@gmail.com> MIME-Version: 1.0 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches * 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") From patchwork Sat Oct 15 14:46:40 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Liliana Marie Prikler X-Patchwork-Id: 43427 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id AD4C727BBEA; Sat, 15 Oct 2022 15:56:37 +0100 (BST) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-3.7 required=5.0 tests=BAYES_00,DKIM_ADSP_CUSTOM_MED, DKIM_INVALID,DKIM_SIGNED,FREEMAIL_FROM,MAILING_LIST_MULTI, RCVD_IN_MSPIKE_H2,SPF_HELO_PASS autolearn=unavailable autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id 7423D27BBE9 for ; Sat, 15 Oct 2022 15:56:37 +0100 (BST) Received: from localhost ([::1]:45272 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ojiaa-0001ub-LH for patchwork@mira.cbaines.net; Sat, 15 Oct 2022 10:56:36 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:37812) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1ojia3-0001Px-Pa for guix-patches@gnu.org; Sat, 15 Oct 2022 10:56:03 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:43344) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1ojia3-0000Du-HO for guix-patches@gnu.org; Sat, 15 Oct 2022 10:56:03 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ojia3-0001K0-Di for guix-patches@gnu.org; Sat, 15 Oct 2022 10:56:03 -0400 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 Message-ID: <70d4e4d117d08591f8b722c46f6891298e71485c.camel@gmail.com> MIME-Version: 1.0 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches * 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") From patchwork Sat Oct 15 14:47:03 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Patchwork-Submitter: Liliana Marie Prikler X-Patchwork-Id: 43425 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id A245627BBEA; Sat, 15 Oct 2022 15:56:25 +0100 (BST) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-2.7 required=5.0 tests=BAYES_00,DKIM_ADSP_CUSTOM_MED, DKIM_INVALID,DKIM_SIGNED,FREEMAIL_FROM,MAILING_LIST_MULTI, PP_MIME_FAKE_ASCII_TEXT,RCVD_IN_MSPIKE_H2,SPF_HELO_PASS autolearn=unavailable autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id 28BFA27BBE9 for ; Sat, 15 Oct 2022 15:56:25 +0100 (BST) Received: from localhost ([::1]:43514 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ojiaO-0001R5-Az for patchwork@mira.cbaines.net; Sat, 15 Oct 2022 10:56:24 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:37814) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1ojia4-0001Q9-6w for guix-patches@gnu.org; Sat, 15 Oct 2022 10:56:05 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:43345) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1ojia3-0000E1-VT for guix-patches@gnu.org; Sat, 15 Oct 2022 10:56:03 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ojia3-0001K7-RI for guix-patches@gnu.org; Sat, 15 Oct 2022 10:56:03 -0400 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 Message-ID: <72146c36adf1eddc32377307b8855038b53e8cba.camel@gmail.com> MIME-Version: 1.0 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches * 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")