From debbugs-submit-bounces@debbugs.gnu.org Thu Nov 14 21:34:25 2019 Received: (at submit) by debbugs.gnu.org; 15 Nov 2019 02:34:25 +0000 Received: from localhost ([127.0.0.1]:35452 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iVRRI-0004Ho-7B for submit@debbugs.gnu.org; Thu, 14 Nov 2019 21:34:24 -0500 Received: from lists.gnu.org ([209.51.188.17]:46435) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iVRRG-0004Hg-5R for submit@debbugs.gnu.org; Thu, 14 Nov 2019 21:34:22 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:39012) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1iVRRE-0001dv-8Y for guix-patches@gnu.org; Thu, 14 Nov 2019 21:34:21 -0500 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=-2.3 required=5.0 tests=BAYES_20,RCVD_IN_DNSWL_MED, URIBL_BLOCKED autolearn=disabled version=3.3.2 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1iVRRC-0005GB-Fx for guix-patches@gnu.org; Thu, 14 Nov 2019 21:34:19 -0500 Received: from mout02.posteo.de ([185.67.36.66]:35009) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1iVRRB-0005FN-Uf for guix-patches@gnu.org; Thu, 14 Nov 2019 21:34:18 -0500 Received: from submission (posteo.de [89.146.220.130]) by mout02.posteo.de (Postfix) with ESMTPS id C302C2400FB for ; Fri, 15 Nov 2019 03:34:14 +0100 (CET) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=posteo.net; s=2017; t=1573785254; bh=5uOFUhRE69bBpglW6oIoY73iO5rCOeGxyGGHMnmevvI=; h=From:To:Cc:Subject:Date:From; b=GMshZGgCXbhL9XTMlL3IxP/sawifVA2SE5yTtUCLak7FAjj3vX3o/jRE2l/vI+CS0 77KtRhSHQz02M+EqpwUkxNYmVA75xDPaZsWcPJKgwzzRJr3bhV3wGH0HQO1SpdLQCh ySzy4pV8BEO7WzvVljcKNPEwwA3IlbxSVaKgvAPZUB4NLWn3eqlKxLxvZP67IF/QQb c5VGIlBpiymRmpc8s2Wk/0viIXrQr/efCKPu9S8vzN5pUVe1IiXiHabH6Lb5BubKjv OrBttkS2Wv6UuGBt+y0k6jfS61yqpbmZhEwoO5Q46eO7NMJwPzBY+t8vACG34OB0Ny FnPpSgkU6JqQA== Received: from customer (localhost [127.0.0.1]) by submission (posteo.de) with ESMTPSA id 47Dj915mWWz9rxL; Fri, 15 Nov 2019 03:34:13 +0100 (CET) From: Robert Smith To: guix-patches@gnu.org Subject: [PATCH] gnu: Add minisat. Date: Fri, 15 Nov 2019 03:34:01 +0100 Message-Id: <20191115023401.8126-1-robertsmith@posteo.net> X-Mailer: git-send-email 2.24.0 MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] [fuzzy] X-Received-From: 185.67.36.66 X-Spam-Score: -1.3 (-) X-Debbugs-Envelope-To: submit Cc: Robert Smith 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 (--) * gnu/packages/maths.scm (minisat): New variable. --- gnu/packages/maths.scm | 41 +++++++++++++++++++ .../patches/minisat-friend-declaration.patch | 23 +++++++++++ .../patches/minisat-mroot-and-install.patch | 30 ++++++++++++++ 3 files changed, 94 insertions(+) create mode 100644 gnu/packages/patches/minisat-friend-declaration.patch create mode 100644 gnu/packages/patches/minisat-mroot-and-install.patch diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 16a9d97a47..9271609843 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -5242,3 +5242,44 @@ fields of knowledge.") (home-page "http://speedcrunch.org/") (license license:gpl2+))) =20 +(define-public minisat + (package + (name "minisat") + (version "2.2.0") + (source + (origin + (method url-fetch) + (uri (string-append "http://minisat.se/downloads/minisat-" + version ".tar.gz")) + (sha256 + (base32 + "023qdnsb6i18yrrawlhckm47q8x0sl7chpvvw3gssfyw3j2pv5cj")) + (patches + (search-patches "minisat-friend-declaration.patch" + "minisat-mroot-and-install.patch")))) + (build-system gnu-build-system) + (arguments + '(#:make-flags (list (string-append "PREFIX=3D" %output)) + #:tests? #f ;no check target + #:phases + (modify-phases %standard-phases + (delete 'configure) + (add-before 'build 'mroot + (lambda* (#:key inputs #:allow-other-keys) + (setenv "MROOT" (getcwd)) + (chdir "simp") + #t))))) + (inputs + `(("zlib:static" ,zlib "static") + ("zlib" ,zlib) + ("kernel-headers" ,linux-libre-headers))) + (home-page + "http://minisat.se/MiniSat.html") + (synopsis + "Small, yet efficient, SAT solver with good documentation") + (license license:expat) + (description + "MiniSat is a minimalistic, open-source SAT solver, developed to h= elp +researchers and developers alike to get started on SAT. It is released = under +the MIT licence, and is currently used in a number of projects."))) + diff --git a/gnu/packages/patches/minisat-friend-declaration.patch b/gnu/= packages/patches/minisat-friend-declaration.patch new file mode 100644 index 0000000000..8283084086 --- /dev/null +++ b/gnu/packages/patches/minisat-friend-declaration.patch @@ -0,0 +1,23 @@ +See https://groups.google.com/forum/#!topic/minisat/FCocZsC8oMQ + +diff -rupN minisat-2.2.0/core/SolverTypes.h minisat-2.2.0.patched/core/S= olverTypes.h +--- a/core/SolverTypes.h 2010-07-10 17:07:36.000000000 +0100 ++++ b/core/SolverTypes.h 2014-03-29 11:57:49.000000000 +0000 +@@ -47,7 +47,7 @@ struct Lit { + int x; + + // Use this as a constructor: +- friend Lit mkLit(Var var, bool sign =3D false); ++ //friend Lit mkLit(Var var, bool sign =3D false); + + bool operator =3D=3D (Lit p) const { return x =3D=3D p.x; } + bool operator !=3D (Lit p) const { return x !=3D p.x; } +@@ -55,7 +55,7 @@ struct Lit { + }; + + +-inline Lit mkLit (Var var, bool sign) { Lit p; p.x =3D var + var = + (int)sign; return p; } ++inline Lit mkLit (Var var, bool sign =3D false) { Lit p; p.x =3D = var + var + (int)sign; return p; } + inline Lit operator ~(Lit p) { Lit q; q.x =3D p.x ^ 1; r= eturn q; } + inline Lit operator ^(Lit p, bool b) { Lit q; q.x =3D p.x ^ (uns= igned int)b; return q; } + inline bool sign (Lit p) { return p.x & 1; } diff --git a/gnu/packages/patches/minisat-mroot-and-install.patch b/gnu/p= ackages/patches/minisat-mroot-and-install.patch new file mode 100644 index 0000000000..7862314f75 --- /dev/null +++ b/gnu/packages/patches/minisat-mroot-and-install.patch @@ -0,0 +1,30 @@ +Add install target, change default + + * rs now default build target + +--- a/simp/Makefile ++++ b/simp/Makefile +@@ -2,3 +2,8 @@ + DEPDIR =3D mtl utils core + + include $(MROOT)/mtl/template.mk ++ ++install: ++ mkdir -p $(DESTDIR)$(PREFIX)/bin ++ cp -f $(EXEC)_static $(DESTDIR)$(PREFIX)/bin/minisat ++ +--- a/mtl/template.mk ++++ b/mtl/template.mk +@@ -29,11 +29,11 @@ + + .PHONY : s p d r rs clean + ++rs: $(EXEC)_static + s: $(EXEC) + p: $(EXEC)_profile + d: $(EXEC)_debug + r: $(EXEC)_release +-rs: $(EXEC)_static + + libs: lib$(LIB)_standard.a + libp: lib$(LIB)_profile.a --=20 2.24.0 From debbugs-submit-bounces@debbugs.gnu.org Fri Nov 15 10:03:45 2019 Received: (at submit) by debbugs.gnu.org; 15 Nov 2019 15:03:45 +0000 Received: from localhost ([127.0.0.1]:37219 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iVd8T-0007SH-C2 for submit@debbugs.gnu.org; Fri, 15 Nov 2019 10:03:45 -0500 Received: from lists.gnu.org ([209.51.188.17]:56393) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iVd8R-0007S9-MM for submit@debbugs.gnu.org; Fri, 15 Nov 2019 10:03:44 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:39433) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1iVd8P-0006jO-N7 for guix-patches@gnu.org; Fri, 15 Nov 2019 10:03:42 -0500 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=BAYES_40,FREEMAIL_FROM, URIBL_BLOCKED autolearn=disabled version=3.3.2 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1iVd8O-0006Gg-Au for guix-patches@gnu.org; Fri, 15 Nov 2019 10:03:41 -0500 Received: from mail-wm1-x344.google.com ([2a00:1450:4864:20::344]:37882) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1iVd8O-0006GL-4p for guix-patches@gnu.org; Fri, 15 Nov 2019 10:03:40 -0500 Received: by mail-wm1-x344.google.com with SMTP id b17so10749301wmj.2 for ; Fri, 15 Nov 2019 07:03:40 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=references:user-agent:from:to:cc:subject:in-reply-to:date :message-id:mime-version; bh=uZEnt0qSd8h6S/B/hyNNvVW96T0Y16nO5C0MQb+5lVc=; b=Oymot2PkytWrx1p4h4BN0dE45Qs3cEIocMfFfIdfBAvlazmj3Al2wT52audF9Z4IR5 K7kNnwxqCFPCO76Z4aeezHRSux7jII8CSjMrcfwsk3mE5vr9vASh/nEhmfRVfT+MkpJ4 1X7W6TDtTypImzsBo8Nsj8axWOUZzZzrvZvTXyfOHIIqUdsYZNxquwO8wziaRvWM3eVb JVLsewo+JNBWD3euHwYZS6yhDlCY04sNnERDcafbP4lUvf+ywHkAcFX9L3T4azO2Snbv YWhjLtDZU6COZNja8li61i/MgljTy0tD7bej/+mg5zQvsMUUHAO2CgNIPVsTcOhPdFcF s2YQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:references:user-agent:from:to:cc:subject :in-reply-to:date:message-id:mime-version; bh=uZEnt0qSd8h6S/B/hyNNvVW96T0Y16nO5C0MQb+5lVc=; b=hWD2j/h0e23dE1zVwZpR3nVFmU5AUPaxL4Mrdrd6IZqqt36yLuw2Hq3bQs0d8X4p3f RqkfwZjSSfyctxsyckYi1yCmKXBuav2K0IOYCmihPceFiK3/EwB55y42Fr28HpYNwo5e jgeisM42QSZA1ZVWWiU74TeDf7Gjp6ifA6wlA/Qs3nkO5QeWgY+t33ZUfhi+Ij/nAfBs jyTTm8zdOlTwztUBiqPNZ48dzVBZK/YthOeJGcXnjErPXrRIMNnX4A/dNwd36ciUiJyX wp6SRdHrId2GhA/qfU4dFti8NNDoQuzpiUFGeYB4SLvzjK71eRWj1AzEP2v/QSCxS13b fRFQ== X-Gm-Message-State: APjAAAXePDTHIFyRG5xtDu0cNrtg9lY9kwS2tV7urxVVJraASl9UDjLR qeFByXzPHqs5+JEu6F8XoOo= X-Google-Smtp-Source: APXvYqxGdo5MKYByP2kuAWcLgIlkrCniAD6mRccZQGYMY6MRVKhNtPLClpj3Iom3gx+F086N0SuXHg== X-Received: by 2002:a05:600c:2550:: with SMTP id e16mr14531639wma.69.1573830219096; Fri, 15 Nov 2019 07:03:39 -0800 (PST) Received: from meru ([90.114.75.61]) by smtp.gmail.com with ESMTPSA id b3sm10777520wmh.17.2019.11.15.07.03.37 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 15 Nov 2019 07:03:37 -0800 (PST) References: <20191115023401.8126-1-robertsmith@posteo.net> User-agent: mu4e 1.2.0; emacs 26.3 From: Mathieu Othacehe To: guix-patches@gnu.org Subject: Re: [bug#38214] [PATCH] gnu: Add minisat. In-reply-to: <20191115023401.8126-1-robertsmith@posteo.net> Date: Fri, 15 Nov 2019 16:03:35 +0100 Message-ID: <87d0dtfago.fsf@gmail.com> MIME-Version: 1.0 Content-Type: text/plain X-detected-operating-system: by eggs.gnu.org: Genre and OS details not recognized. X-Received-From: 2a00:1450:4864:20::344 X-Spam-Score: -1.3 (-) X-Debbugs-Envelope-To: submit Cc: Robert Smith , 38214@debbugs.gnu.org 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 (--) Hello Robert, Thanks for your patch, a few remarks below. > + (search-patches "minisat-friend-declaration.patch" > + "minisat-mroot-and-install.patch")))) Why are these patch needed? It seems that the last release was a long time ago, maybe we should package it from a git commit? > + ("kernel-headers" ,linux-libre-headers))) ^ Is this really useful? It seems to build without. > + (synopsis > + "Small, yet efficient, SAT solver with good documentation") > + (license license:expat) It's a tacit agreement, but the order of package fields is often: - synopsis - description - home-page - license. Could you re-order those fields? Do not forget to add your copyright on top of the file, and to indent your code properly (see: https://guix.gnu.org/manual/en/html_node/Formatting-Code.html). Could you send an updated patch? Thanks, Mathieu From debbugs-submit-bounces@debbugs.gnu.org Fri Nov 15 15:00:40 2019 Received: (at submit) by debbugs.gnu.org; 15 Nov 2019 20:00:40 +0000 Received: from localhost ([127.0.0.1]:37427 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iVhln-000698-Vx for submit@debbugs.gnu.org; Fri, 15 Nov 2019 15:00:40 -0500 Received: from lists.gnu.org ([209.51.188.17]:40048) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iVhlm-00068u-4h for submit@debbugs.gnu.org; Fri, 15 Nov 2019 15:00:39 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:37839) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1iVhlk-0002aa-3U for guix-patches@gnu.org; Fri, 15 Nov 2019 15:00:37 -0500 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=-4.2 required=5.0 tests=BAYES_00,RCVD_IN_DNSWL_MED, URIBL_BLOCKED autolearn=disabled version=3.3.2 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1iVhli-0007cw-Kl for guix-patches@gnu.org; Fri, 15 Nov 2019 15:00:35 -0500 Received: from mout01.posteo.de ([185.67.36.65]:34228) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1iVhli-0007cf-5i for guix-patches@gnu.org; Fri, 15 Nov 2019 15:00:34 -0500 Received: from submission (posteo.de [89.146.220.130]) by mout01.posteo.de (Postfix) with ESMTPS id DC5B916005E for ; Fri, 15 Nov 2019 21:00:31 +0100 (CET) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=posteo.net; s=2017; t=1573848031; bh=hGV2wb51/w/xONdJOTy/Fj5eeeYWuBBRZ73/BV+t/LU=; h=Date:Cc:Subject:From:To:From; b=qAjXNrKfssfZb5gsCxyuXswj/e2jrphlLfiZ01UbWIqr2pyhr5VcUkLyDpC/0gzf1 OAwJARirZdl3Ya5KNrtPxkCyNzXz9XmQIA47jD8sClpioRkzj2LcoCvzjbgOzR9a5p ESlfboqyi9iwoS3mGI9xHsG64uiGouzK+KMgEdO/0xFQSfb0+qYnDox2HgqsrJZXcH rdn+fDr+9+B3YLHgsXaVIcH7SaPO5VCf4OIFFh6KtF+Nf6qJTxCYJ0QeRkIf6+mfYa turgU8Ax0rP462OU1c54weAk6OijDSAAQqGUQh67qTGmLD1hC+ltzgE/UvtbGGWQZh rE7uOzLyjHr+g== Received: from customer (localhost [127.0.0.1]) by submission (posteo.de) with ESMTPSA id 47F8NG3F1nz6tmF; Fri, 15 Nov 2019 21:00:29 +0100 (CET) Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=UTF-8 In-Reply-To: <87d0dtfago.fsf@gmail.com> Date: Fri, 15 Nov 2019 21:00:27 +0100 Subject: Re: [bug#38214] [PATCH] gnu: Add minisat. From: "Robert Smith" To: Message-Id: X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] [fuzzy] X-Received-From: 185.67.36.65 X-Spam-Score: -1.3 (-) X-Debbugs-Envelope-To: submit Cc: Mathieu Othacehe , 38214@debbugs.gnu.org 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 (--) On Fri Nov 15, 2019 at 4:03 PM Mathieu Othacehe wrote: > > + (search-patches "minisat-friend-declaration.patch" > > + "minisat-mroot-and-install.patch")))) >=20 > Why are these patch needed? It seems that the last release was a long > time ago, maybe we should package it from a git commit? Thanks for the catch, I didn't realize that the git repo was so far ahead of the last release. > > + ("kernel-headers" ,linux-libre-headers))) > ^ > Is this really useful? It seems to build without. I could have sworn that it refused to build without them, but testing it now seems to work fine. I must have either been confused or it was some other problem that I fixed. Thanks for the feedback, I'll work on making the changes and submitting a new patch. -Robert From debbugs-submit-bounces@debbugs.gnu.org Sat Nov 16 10:20:01 2019 Received: (at 38214) by debbugs.gnu.org; 16 Nov 2019 15:20:01 +0000 Received: from localhost ([127.0.0.1]:39572 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iVzrf-0005md-2d for submit@debbugs.gnu.org; Sat, 16 Nov 2019 10:20:01 -0500 Received: from mout02.posteo.de ([185.67.36.66]:56251) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iVzrY-0005mM-GO for 38214@debbugs.gnu.org; Sat, 16 Nov 2019 10:19:52 -0500 Received: from submission (posteo.de [89.146.220.130]) by mout02.posteo.de (Postfix) with ESMTPS id 66F50240101 for <38214@debbugs.gnu.org>; Sat, 16 Nov 2019 16:19:42 +0100 (CET) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=posteo.net; s=2017; t=1573917582; bh=dgGuBhCVCa7vOb/Kgr+LYzOe+qsxusq7HsOkg3qAPGE=; h=From:To:Cc:Subject:Date:From; b=e+yXsX2QdkT63jtib/4GNq4XWxaQlWZK5iXytIGPjyzzPLGbDkkw7FYiay5wiJ7tl 5Og4erx2nl714SwY3SMg2wjrIfpKru+4g/96PQbm7wfm2bD3arpwN4o1/riiWZqhzP WOAdppZWQZriv0FkugTAISszFMiLnFEGLvr+wQBYOc83HRj4iSFoRqIu9dPj94Q+ne 1iTgUCxjvqkQq0RvV4/9ToVMn+joOpainfYgO0P1jYH4jX+RCDrPwkhdIyOQCMB/WV uDRU/yTQGcKvMdtnFBk+vZDlwxInr5up8XZpz6SXzES4SG2OlIii9XHY7dYB80cyDo qt4uIHZpoihcA== Received: from customer (localhost [127.0.0.1]) by submission (posteo.de) with ESMTPSA id 47Ff5m6rN1z9rxG; Sat, 16 Nov 2019 16:19:40 +0100 (CET) From: Robert Smith To: m.othacehe@gmail.com Subject: [PATCH v2] gnu: Add minisat. Date: Sat, 16 Nov 2019 16:18:43 +0100 Message-Id: <20191116151843.30150-1-robertsmith@posteo.net> X-Mailer: git-send-email 2.24.0 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-Spam-Score: -2.3 (--) X-Debbugs-Envelope-To: 38214 Cc: Robert Smith , 38214@debbugs.gnu.org, guix-patches@gnu.org 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 (minisat): New variable. --- I updated the source to the latest commit available, which unfortunately only gets us from 2010 to 2013. Although the minisat-friend-declaration patch was written by the original author in 2014, they never committed it to the repo. Additionally an install patch is still needed to avoid a dependency on our own shared library. Hopefully all style issues have been fixed, and a copyright line was added. gnu/packages/maths.scm | 42 +++++++++++++++++++ .../patches/minisat-friend-declaration.patch | 25 +++++++++++ gnu/packages/patches/minisat-install.patch | 19 +++++++++ 3 files changed, 86 insertions(+) create mode 100644 gnu/packages/patches/minisat-friend-declaration.patch create mode 100644 gnu/packages/patches/minisat-install.patch diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 16a9d97a47..42a72737da 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -32,6 +32,7 @@ ;;; Copyright © 2018 Amin Bandali ;;; Copyright © 2019 Nicolas Goaziou ;;; Copyright © 2019 Steve Sprang +;;; Copyright © 2019 Robert Smith ;;; ;;; This file is part of GNU Guix. ;;; @@ -5242,3 +5243,44 @@ fields of knowledge.") (home-page "http://speedcrunch.org/") (license license:gpl2+))) +(define-public minisat + ;; This is the last commit which is available upstream, no + ;; release happened since 2010. + (let ((commit "37dc6c67e2af26379d88ce349eb9c4c6160e8543") + (revision "1")) + (package + (name "minisat") + (version (string-append "2.2.0-" revision "." (string-take commit 7))) + (source + (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/niklasso/minisat.git") + (commit commit))) + (file-name (string-append name "-" version "-checkout")) + (sha256 + (base32 + "091hf3qkm197s5r7xcr3m07xsdwyz2rqk1hc9kj0hn13imz09irq")) + (patches + (search-patches "minisat-friend-declaration.patch" + "minisat-install.patch")))) + (build-system gnu-build-system) + (arguments + '(#:make-flags (list (string-append "prefix=" %output)) + #:tests? #f ;no check target + #:phases + (modify-phases %standard-phases + (delete 'configure)))) + (inputs + `(("zlib:static" ,zlib "static") + ("zlib" ,zlib))) + (synopsis + "Small, yet efficient, SAT solver with good documentation") + (description + "MiniSat is a minimalistic, open-source SAT solver, developed to help +researchers and developers alike to get started on SAT. It is released under +the MIT licence, and is currently used in a number of projects.") + (home-page + "http://minisat.se/MiniSat.html") + (license license:expat)))) + diff --git a/gnu/packages/patches/minisat-friend-declaration.patch b/gnu/packages/patches/minisat-friend-declaration.patch new file mode 100644 index 0000000000..14a886ae2f --- /dev/null +++ b/gnu/packages/patches/minisat-friend-declaration.patch @@ -0,0 +1,25 @@ +See https://groups.google.com/forum/#!topic/minisat/FCocZsC8oMQ +This seems to only be a problem with newer versions of g++, and +upstream development seems to have stopped in 2013. + +diff -rupN minisat-2.2.0/core/SolverTypes.h minisat-2.2.0.patched/core/SolverTypes.h +--- a/minisat/core/SolverTypes.h 2010-07-10 17:07:36.000000000 +0100 ++++ b/minisat/core/SolverTypes.h 2014-03-29 11:57:49.000000000 +0000 +@@ -47,7 +47,7 @@ struct Lit { + int x; + + // Use this as a constructor: +- friend Lit mkLit(Var var, bool sign = false); ++ //friend Lit mkLit(Var var, bool sign = false); + + bool operator == (Lit p) const { return x == p.x; } + bool operator != (Lit p) const { return x != p.x; } +@@ -55,7 +55,7 @@ struct Lit { + }; + + +-inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; } ++inline Lit mkLit (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; } + inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; } + inline Lit operator ^(Lit p, bool b) { Lit q; q.x = p.x ^ (unsigned int)b; return q; } + inline bool sign (Lit p) { return p.x & 1; } diff --git a/gnu/packages/patches/minisat-install.patch b/gnu/packages/patches/minisat-install.patch new file mode 100644 index 0000000000..23cde89bec --- /dev/null +++ b/gnu/packages/patches/minisat-install.patch @@ -0,0 +1,19 @@ +Avoid the default dynamic executable, which depends on minisat.so +Instead install the release version, which is statically linked. + +diff --git a/Makefile b/Makefile +index ceb9d77..7b91906 100644 +--- a/Makefile ++++ b/Makefile +@@ -191,9 +191,9 @@ install-lib: $(BUILD_DIR)/release/lib/$(MINISAT_SLIB) $(BUILD_DIR)/dynamic/lib/$ + ln -sf $(MINISAT_DLIB).$(SOMAJOR) $(DESTDIR)$(libdir)/$(MINISAT_DLIB) + $(INSTALL) -m 644 $(BUILD_DIR)/release/lib/$(MINISAT_SLIB) $(DESTDIR)$(libdir) + +-install-bin: $(BUILD_DIR)/dynamic/bin/$(MINISAT) ++install-bin: $(BUILD_DIR)/release/bin/$(MINISAT) + $(INSTALL) -d $(DESTDIR)$(bindir) +- $(INSTALL) -m 755 $(BUILD_DIR)/dynamic/bin/$(MINISAT) $(DESTDIR)$(bindir) ++ $(INSTALL) -m 755 $(BUILD_DIR)/release/bin/$(MINISAT) $(DESTDIR)$(bindir) + + clean: + rm -f $(foreach t, release debug profile dynamic, $(foreach o, $(SRCS:.cc=.o), $(BUILD_DIR)/$t/$o)) \ -- 2.24.0 From debbugs-submit-bounces@debbugs.gnu.org Tue Nov 19 04:34:10 2019 Received: (at control) by debbugs.gnu.org; 19 Nov 2019 09:34:10 +0000 Received: from localhost ([127.0.0.1]:46580 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iWzth-0005Io-QZ for submit@debbugs.gnu.org; Tue, 19 Nov 2019 04:34:10 -0500 Received: from eggs.gnu.org ([209.51.188.92]:50762) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iWztd-0005IE-1h for control@debbugs.gnu.org; Tue, 19 Nov 2019 04:34:05 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]:43218) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1iWztX-0005m1-R1 for control@debbugs.gnu.org; Tue, 19 Nov 2019 04:33:59 -0500 Received: from [2001:660:6102:320:e120:2c8f:8909:cdfe] (port=56558 helo=ribbon) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1iWztW-0003PY-Qg for control@debbugs.gnu.org; Tue, 19 Nov 2019 04:33:59 -0500 Date: Tue, 19 Nov 2019 10:33:56 +0100 Message-Id: <87sgmkrz0b.fsf@gnu.org> To: control@debbugs.gnu.org From: =?utf-8?Q?Ludovic_Court=C3=A8s?= Subject: control message for bug #38214 MIME-version: 1.0 Content-type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Spam-Score: -2.3 (--) X-Debbugs-Envelope-To: control 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: -3.3 (---) merge 38214 38230 quit From debbugs-submit-bounces@debbugs.gnu.org Tue Nov 19 11:31:02 2019 Received: (at 38214) by debbugs.gnu.org; 19 Nov 2019 16:31:03 +0000 Received: from localhost ([127.0.0.1]:48352 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iX6P8-0002Ka-BX for submit@debbugs.gnu.org; Tue, 19 Nov 2019 11:31:02 -0500 Received: from mail-wm1-f67.google.com ([209.85.128.67]:38804) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iX6P6-0002K5-K5 for 38214@debbugs.gnu.org; Tue, 19 Nov 2019 11:31:00 -0500 Received: by mail-wm1-f67.google.com with SMTP id z19so4451108wmk.3 for <38214@debbugs.gnu.org>; Tue, 19 Nov 2019 08:31:00 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=references:user-agent:from:to:cc:subject:in-reply-to:date :message-id:mime-version; bh=V0yHFqd02W8t6gWvYcv+ZSJ93ITmVJdjJB+eDSLC8uM=; b=LvD8TPzYT5gzk5pRGjQ2zRyUpUAfKrc/5blMWkWAJM0RHY1kABk5LlAemeNTW9KMGQ Xq7qYCxDeVBL4GxAwamn7Dv12G9FKXTWtNspCU6OFaxfeP/FjqiOIiMP7n9KzAqL/F/s CnowVSB2L5SAxvMRVFdlr8sv5FnGZj/J/BTHdupFAffKifkYfqgQSEcS2UAazXnImoCB pyDLmFsreC/prraE0BZmlzJKjWc3ts0r36yFdFOaXKhHm7OGHuyvYQ9LhMBFvIcxHomJ JjVGTaaLBH/Q3G358F1wKjQE+hWX7FaeaiCJR8HlXexnpW0JSdLC3BPALfY8GvO0+dd7 EGbw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:references:user-agent:from:to:cc:subject :in-reply-to:date:message-id:mime-version; bh=V0yHFqd02W8t6gWvYcv+ZSJ93ITmVJdjJB+eDSLC8uM=; b=bDsw+sffap7LoNTOVl9BTVLPwTvvI1CgCHm3tgO1Kthl6H2Pweg10iLKm0LA+ZcZcl gy/mnUx6z3+2Bluxzpm8OsbBHdZo2cTUL9fb3MwF66Qt0ja3ejZObbtlFIIUKsc++dgP gZYt0QLSx0gdunfbLFeK4geOqTpoxih+RKO+UP5fXpAhTVaSXthv+YmMZqHRkUGf6G2R j2bX7DdkzJhdZN0PpV/WCkLSqYQ/ZgIANJ/t1JLjlAjQR3LB4tfahGEgKwwoqsBtZ9XE ALrwORVQkMd+tht4Luw9P8vEvgoJaF9QUCjhKtkvv+Fn+t5UxRxfIWPEHqsRK9fCx+JT kCYA== X-Gm-Message-State: APjAAAWFOmuDqYaT41T7uPKT0a3ViJUig4sCIge00ORWKAWDPjnjR75S fiLR9+SUFuhtTx7Rjo4Rbgo= X-Google-Smtp-Source: APXvYqzu0ZR4ahhq5eqXeMxAoIK5abBXKa5cmHEObDmxNY2FqFjnJCvKbAyf37zcl4oasaFsRxZxwg== X-Received: by 2002:a1c:28d4:: with SMTP id o203mr6836266wmo.147.1574181054829; Tue, 19 Nov 2019 08:30:54 -0800 (PST) Received: from meru ([90.114.75.61]) by smtp.gmail.com with ESMTPSA id 76sm3770854wma.0.2019.11.19.08.30.53 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 19 Nov 2019 08:30:54 -0800 (PST) References: <20191116151843.30150-1-robertsmith@posteo.net> User-agent: mu4e 1.2.0; emacs 26.3 From: Mathieu Othacehe To: Robert Smith Subject: Re: [PATCH v2] gnu: Add minisat. In-reply-to: <20191116151843.30150-1-robertsmith@posteo.net> Date: Tue, 19 Nov 2019 17:30:52 +0100 Message-ID: <87zhgr3k1v.fsf@gmail.com> MIME-Version: 1.0 Content-Type: text/plain X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 38214 Cc: 38214@debbugs.gnu.org, guix-patches@gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) Hello Robert, I fixed a small indentation issue, added both patches to local.mk, edited commit message accordingly and pushed! Thanks, Mathieu From debbugs-submit-bounces@debbugs.gnu.org Tue Nov 19 11:32:52 2019 Received: (at 38214-done) by debbugs.gnu.org; 19 Nov 2019 16:32:52 +0000 Received: from localhost ([127.0.0.1]:48369 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iX6Qu-0002O3-6c for submit@debbugs.gnu.org; Tue, 19 Nov 2019 11:32:52 -0500 Received: from mail-wr1-f41.google.com ([209.85.221.41]:37549) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iX6Qs-0002Np-53 for 38214-done@debbugs.gnu.org; Tue, 19 Nov 2019 11:32:50 -0500 Received: by mail-wr1-f41.google.com with SMTP id t1so24622538wrv.4 for <38214-done@debbugs.gnu.org>; Tue, 19 Nov 2019 08:32:50 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=references:user-agent:from:to:cc:subject:in-reply-to:date :message-id:mime-version; bh=wmbppt0qVAkKZmsCQ1MzkIGsGuPfh+CpH56Muv22JLk=; b=og/825iemJ+Z7n9ahMIoBgM92wzJUKO6FZpjWAimlVikUH1z4IyGq7A3mUHCWNI9AW SsENLQ75SO8wZNpyuIdfrrB4D/kVVlm6Pf/CbVZhB751Sos4ENHBt73hcZI2pKaBYSly 0f/s1fUTysgyTssjkcJMUWspgSNzskKNdl/3DkBIqggkZQFciHqHVvhSK3sWzBVQybsa Xn3wSSKiY4ww/JKvm/HmUQIOfmY7fGn+nilT3qItIIW5emuT7S0X7Vh1YXxQuq/0Xt4r J03w0O0io6wh2I32jUefr/OJu5ORH3lGYNcRkddQaOXutTdT24WjnEkPcAYqwfYOUPPH qUiQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:references:user-agent:from:to:cc:subject :in-reply-to:date:message-id:mime-version; bh=wmbppt0qVAkKZmsCQ1MzkIGsGuPfh+CpH56Muv22JLk=; b=UYI7RW/h+SWZ00tVKyZrEcOvmndRW9oygcoh+d+WpvGSLchkV5WIMOrqcLitlOCgEs EgYCncuSN018wZm5yscTJx4n15uKvyB9r7fcQSF+GE6mIlKrW4D+Qyg20VFK5QPuCUhm dyDlP5gNRfByUYlXaUrwgKlhHYuUIQTYOGAZMb9kpIQt+Ve/kFP6cYmx9ngF79vMDiwy REl1vQA5Gzt9VblCtoxJXeX/MIztasbtIbDlfNSqqWTaAB9B5qjwIxDd/ILCGienPTNo hwxf8/gbB7hXzN8H22wqIk5rZZlWZlYpQqjpqbg82jVG0I0LsYUquHUH6iYO9/rTJskE lWWw== X-Gm-Message-State: APjAAAXP9nzXvB0dCo1G4Kd2TbGeElTOSCj6IYOoi8eZoL5XyHQD+e4x pOEk/z50syPT8c8UJZoAP95eAwVo X-Google-Smtp-Source: APXvYqzNy8OJWuPGZ1GtUudyIy9eD8DfESdOXLH79TOaEsIN2QChUDg3nLdob27JZRx3xjs3gcm5vA== X-Received: by 2002:adf:e505:: with SMTP id j5mr34781339wrm.46.1574181164060; Tue, 19 Nov 2019 08:32:44 -0800 (PST) Received: from meru ([90.114.75.61]) by smtp.gmail.com with ESMTPSA id l13sm3547115wmh.12.2019.11.19.08.32.43 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 19 Nov 2019 08:32:43 -0800 (PST) References: <20191116151843.30150-1-robertsmith@posteo.net> User-agent: mu4e 1.2.0; emacs 26.3 From: Mathieu Othacehe To: Robert Smith Subject: Re: [PATCH v2] gnu: Add minisat. In-reply-to: <20191116151843.30150-1-robertsmith@posteo.net> Date: Tue, 19 Nov 2019 17:32:42 +0100 Message-ID: <87wobv3jyt.fsf@gmail.com> MIME-Version: 1.0 Content-Type: text/plain X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 38214-done Cc: 38214-done@debbugs.gnu.org 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 (-) And closing! From unknown Sun Jun 22 20:59:02 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Wed, 18 Dec 2019 12:24:04 +0000 User-Agent: Fakemail v42.6.9 # This is a fake control message. # # The action: # bug archived. thanks # This fakemail brought to you by your local debbugs # administrator