From patchwork Fri Nov 15 02:34:01 2019 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Robert Smith X-Patchwork-Id: 16118 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 81CEC1774D; Fri, 15 Nov 2019 02:35:24 +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 330751774B for ; Fri, 15 Nov 2019 02:35:24 +0000 (GMT) Received: from localhost ([::1]:34996 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1iVRSF-0001iQ-JI for patchwork@mira.cbaines.net; Thu, 14 Nov 2019 21:35:23 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:39110) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1iVRRw-0001iD-6t for guix-patches@gnu.org; Thu, 14 Nov 2019 21:35:05 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1iVRRu-0005ig-Nr for guix-patches@gnu.org; Thu, 14 Nov 2019 21:35:04 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:54864) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1iVRRu-0005ia-KY for guix-patches@gnu.org; Thu, 14 Nov 2019 21:35:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1iVRRu-0004Ik-Ed for guix-patches@gnu.org; Thu, 14 Nov 2019 21:35:02 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#38214] [PATCH] gnu: Add minisat. Resent-From: Robert Smith Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Fri, 15 Nov 2019 02:35:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 38214 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 38214@debbugs.gnu.org Cc: Robert Smith X-Debbugs-Original-To: guix-patches@gnu.org Received: via spool by submit@debbugs.gnu.org id=B.157378526516485 (code B ref -1); Fri, 15 Nov 2019 02:35:02 +0000 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 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 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 X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] [fuzzy] 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. --- 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+))) +(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=" %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 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."))) + 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/SolverTypes.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 = 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-mroot-and-install.patch b/gnu/packages/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 = 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