From patchwork Sat Nov 16 15:18:43 2019 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Patchwork-Submitter: Robert Smith X-Patchwork-Id: 16124 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 0C909176F6; Sat, 16 Nov 2019 15:20:13 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,T_DKIM_INVALID, URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.0 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTP id 3F6F6176F5 for ; Sat, 16 Nov 2019 15:20:12 +0000 (GMT) Received: from localhost ([::1]:48594 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1iVzrv-0006ew-Kg for patchwork@mira.cbaines.net; Sat, 16 Nov 2019 10:20:11 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:51467) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1iVzro-0006eg-Cv for guix-patches@gnu.org; Sat, 16 Nov 2019 10:20:05 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1iVzrm-00085y-Un for guix-patches@gnu.org; Sat, 16 Nov 2019 10:20:04 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:58988) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1iVzrm-00085r-Re for guix-patches@gnu.org; Sat, 16 Nov 2019 10:20:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1iVzrm-0005n9-Hm for guix-patches@gnu.org; Sat, 16 Nov 2019 10:20:02 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#38214] [PATCH v2] gnu: Add minisat. References: <20191115023401.8126-1-robertsmith@posteo.net> In-Reply-To: <20191115023401.8126-1-robertsmith@posteo.net> Resent-From: Robert Smith Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sat, 16 Nov 2019 15:20:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 38214 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: m.othacehe@gmail.com Cc: robertsmith@posteo.net, 38214@debbugs.gnu.org X-Debbugs-Original-Cc: Robert Smith , 38214@debbugs.gnu.org, guix-patches@gnu.org Received: via spool by 38214-submit@debbugs.gnu.org id=B38214.157391760122251 (code B ref 38214); Sat, 16 Nov 2019 15:20:02 +0000 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 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 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 209.51.188.43 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 (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)) \