From debbugs-submit-bounces@debbugs.gnu.org Sat Nov 16 10:20:07 2019 Received: (at submit) by debbugs.gnu.org; 16 Nov 2019 15:20:07 +0000 Received: from localhost ([127.0.0.1]:39576 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iVzrm-0005n8-FP for submit@debbugs.gnu.org; Sat, 16 Nov 2019 10:20:07 -0500 Received: from lists.gnu.org ([209.51.188.17]:56034) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iVzrg-0005mf-AI for submit@debbugs.gnu.org; Sat, 16 Nov 2019 10:20:00 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:51445) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1iVzre-0006cb-IY for guix-patches@gnu.org; Sat, 16 Nov 2019 10:19:56 -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_40,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 1iVzrc-0007z0-V6 for guix-patches@gnu.org; Sat, 16 Nov 2019 10:19:54 -0500 Received: from mout02.posteo.de ([185.67.36.66]:54937) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1iVzrc-0007u2-Cl for guix-patches@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 61018240100 for ; 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: 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 , 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: -0.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 =C2=A9 2018 Amin Bandali ;;; Copyright =C2=A9 2019 Nicolas Goaziou ;;; Copyright =C2=A9 2019 Steve Sprang +;;; Copyright =C2=A9 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+))) =20 +(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=3D" %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/S= olverTypes.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 =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-install.patch b/gnu/packages/pa= tches/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) +=20 +-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)$(bind= ir) ++ $(INSTALL) -m 755 $(BUILD_DIR)/release/bin/$(MINISAT) $(DESTDIR)$(bind= ir) +=20 + clean: + rm -f $(foreach t, release debug profile dynamic, $(foreach o, $(SRCS:= .cc=3D.o), $(BUILD_DIR)/$t/$o)) \ --=20 2.24.0 From debbugs-submit-bounces@debbugs.gnu.org Sat Nov 16 10:34:21 2019 Received: (at 38230) by debbugs.gnu.org; 16 Nov 2019 15:34:21 +0000 Received: from localhost ([127.0.0.1]:39594 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iW05d-00069o-2W for submit@debbugs.gnu.org; Sat, 16 Nov 2019 10:34:21 -0500 Received: from mout01.posteo.de ([185.67.36.65]:53638) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iW05a-00069Z-PQ for 38230@debbugs.gnu.org; Sat, 16 Nov 2019 10:34:19 -0500 Received: from submission (posteo.de [89.146.220.130]) by mout01.posteo.de (Postfix) with ESMTPS id 2C26E160061 for <38230@debbugs.gnu.org>; Sat, 16 Nov 2019 16:34:12 +0100 (CET) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=posteo.net; s=2017; t=1573918452; bh=ih1e19n2zhsyvC2x20w6YBZjIdm7oZR5qwVQQs74c0A=; h=Date:From:To:Subject:From; b=V9mkLIOy6HJHcgovBPnR+U4vBqr9fG2Y8mpKnrLY072jmzJxE+5vIMXIAZFCY69R2 bqmFjkW/sI7jAoz5J5N1m5YEi0B1BCDUsizpv+V8HTQXp/F1xRmZ1iNllcRebbSAVY 6qdtgj6rwLsuxWL0UXlpFCx2aNJdIp795eV/AJDbl2avQvkYp6FQs9AHvmpyOeJzKe HEI4H1zZ0rtS0c9NtNI8uC5hWulUopMQWlJsdjf2UFqExkQCr3jKSJjUUT0lGBW83X /7o9lGv97T5+0MZO68TN6OrMs2xuQpNa/GvTupdMGULJngHyhrvsXpBuArokGWhYGa drxxf6EDA/+KQ== Received: from customer (localhost [127.0.0.1]) by submission (posteo.de) with ESMTPSA id 47FfQQ1bSqz6tm5 for <38230@debbugs.gnu.org>; Sat, 16 Nov 2019 16:34:06 +0100 (CET) MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII; format=flowed Content-Transfer-Encoding: 7bit Date: Sat, 16 Nov 2019 16:34:06 +0100 From: Robert Smith To: 38230@debbugs.gnu.org Subject: Oops Message-ID: <9fe1ed912336ac9ed0f4d8bdaa011933@posteo.net> X-Sender: robertsmith@posteo.net User-Agent: Posteo Webmail X-Spam-Score: -2.3 (--) X-Debbugs-Envelope-To: 38230 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 (---) Apologies, I didn't intend to create a new issue. My email-foo is still weak :( -Robert 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:08 2019 Received: (at submit) by debbugs.gnu.org; 19 Nov 2019 16:31:08 +0000 Received: from localhost ([127.0.0.1]:48356 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iX6PD-0002Kx-T9 for submit@debbugs.gnu.org; Tue, 19 Nov 2019 11:31:08 -0500 Received: from lists.gnu.org ([209.51.188.17]:45041) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iX6P9-0002Ki-Uj for submit@debbugs.gnu.org; Tue, 19 Nov 2019 11:31:04 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:40486) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1iX6P7-0003nT-NG for guix-patches@gnu.org; Tue, 19 Nov 2019 11:31:03 -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.8 required=5.0 tests=BAYES_50,FREEMAIL_FROM autolearn=disabled version=3.3.2 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1iX6P5-0003yQ-H9 for guix-patches@gnu.org; Tue, 19 Nov 2019 11:31:01 -0500 Received: from mail-wm1-x343.google.com ([2a00:1450:4864:20::343]:33303) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1iX6P5-0003wU-AP for guix-patches@gnu.org; Tue, 19 Nov 2019 11:30:59 -0500 Received: by mail-wm1-x343.google.com with SMTP id a17so2905443wmb.0 for ; Tue, 19 Nov 2019 08:30:55 -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=NBOBh4x67yj7QFwGlKS4Mla02UWdH1pLI3NhqCPg7JtkPk3tp+ZcvnBw0jXUPdXCQR qz1/YVR0I50GxiAp4I7haDWF/3RLBVkelV9AmNRpu1AiuaIulEBQkgmTGSpgcuCF8KXM B7/9hwEVvVElRsBl91KiORrfK4ZXaBWWMyWj6CvpCz/yQuQTEVxoILYBdpDok64VElpl 8PHcd7UjNUa7owZA8bAP+nB2XElFSIQ1Jz0ZApG5DDQbsKjK/iMxSLaM9S4uPCDGtl44 w8+Hk7QlGwlFaRbjrzuupOY74exRFuYIENP6kyuRKjkk4YFXXycql+PxDD5908fMIlLd praw== X-Gm-Message-State: APjAAAV13SqBJGcAzRNfe4W0i0JvK8kCuEKs6kcatCzr0RR6pPqhDrGx GtCbeadylcQNJMESgvIiy/VEAXuY 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-detected-operating-system: by eggs.gnu.org: Genre and OS details not recognized. X-Received-From: 2a00:1450:4864:20::343 X-Spam-Score: -1.3 (-) X-Debbugs-Envelope-To: submit 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: -2.3 (--) Hello Robert, I fixed a small indentation issue, added both patches to local.mk, edited commit message accordingly and pushed! Thanks, Mathieu From unknown Sun Jun 22 11:42:37 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: 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