summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMaciej Barć <xgqt@gentoo.org>2023-02-06 17:14:41 +0100
committerMaciej Barć <xgqt@gentoo.org>2023-02-06 18:23:18 +0100
commit58bf1623e2f1be955a04a7b5adbbb03b79459fbd (patch)
treefc43bab06adb7be89e5daf9065518e7fb3ba360c /sci-mathematics
parentsci-mathematics/vampire: fix build on musl (diff)
downloadgentoo-58bf1623e2f1be955a04a7b5adbbb03b79459fbd.tar.gz
gentoo-58bf1623e2f1be955a04a7b5adbbb03b79459fbd.tar.bz2
gentoo-58bf1623e2f1be955a04a7b5adbbb03b79459fbd.zip
sci-mathematics/minisat: fix build on musl
Bug: https://github.com/stp/minisat/pull/6 Closes: https://bugs.gentoo.org/832519 Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Diffstat (limited to 'sci-mathematics')
-rw-r--r--sci-mathematics/minisat/files/minisat-2.2.1-musl.patch41
-rw-r--r--sci-mathematics/minisat/minisat-2.2.1-r1.ebuild13
2 files changed, 50 insertions, 4 deletions
diff --git a/sci-mathematics/minisat/files/minisat-2.2.1-musl.patch b/sci-mathematics/minisat/files/minisat-2.2.1-musl.patch
new file mode 100644
index 000000000000..3a25d5964318
--- /dev/null
+++ b/sci-mathematics/minisat/files/minisat-2.2.1-musl.patch
@@ -0,0 +1,41 @@
+From 4c8afcd6bfbf2cbdb5ebe271f20503a6d34d7d49 Mon Sep 17 00:00:00 2001
+From: =?UTF-8?q?Maciej=20Bar=C4=87?= <xgqt@gentoo.org>
+Date: Mon, 6 Feb 2023 17:09:18 +0100
+Subject: [PATCH] utils/System.*: use fpu_control only on glibc
+MIME-Version: 1.0
+Content-Type: text/plain; charset=UTF-8
+Content-Transfer-Encoding: 8bit
+
+Bug: https://github.com/vprover/vampire/pull/432
+Signed-off-by: Maciej Barć <xgqt@gentoo.org>
+---
+ minisat/utils/System.cc | 2 +-
+ minisat/utils/System.h | 2 +-
+ 2 files changed, 2 insertions(+), 2 deletions(-)
+
+diff --git a/minisat/utils/System.cc b/minisat/utils/System.cc
+index 282f98ed..112708f7 100644
+--- a/minisat/utils/System.cc
++++ b/minisat/utils/System.cc
+@@ -97,7 +97,7 @@ double Minisat::memUsedPeak(bool /*strictlyPeak*/) { return 0; }
+
+ void Minisat::setX86FPUPrecision()
+ {
+-#if defined(__linux__) && defined(_FPU_EXTENDED) && defined(_FPU_DOUBLE) && defined(_FPU_GETCW)
++#if defined(__GLIBC__) && defined(_FPU_EXTENDED) && defined(_FPU_DOUBLE) && defined(_FPU_GETCW)
+ // Only correct FPU precision on Linux architectures that needs and supports it:
+ fpu_control_t oldcw, newcw;
+ _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
+diff --git a/minisat/utils/System.h b/minisat/utils/System.h
+index a51d4c2e..189fcbff 100644
+--- a/minisat/utils/System.h
++++ b/minisat/utils/System.h
+@@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
+ #ifndef Minisat_System_h
+ #define Minisat_System_h
+
+-#if defined(__linux__)
++#if defined(__GLIBC__)
+ #include <fpu_control.h>
+ #endif
+
diff --git a/sci-mathematics/minisat/minisat-2.2.1-r1.ebuild b/sci-mathematics/minisat/minisat-2.2.1-r1.ebuild
index 15d260429e0f..ac28363ef0f5 100644
--- a/sci-mathematics/minisat/minisat-2.2.1-r1.ebuild
+++ b/sci-mathematics/minisat/minisat-2.2.1-r1.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2022 Gentoo Authors
+# Copyright 1999-2023 Gentoo Authors
# Distributed under the terms of the GNU General Public License v2
EAPI=8
@@ -6,10 +6,11 @@ EAPI=8
inherit cmake
DESCRIPTION="Small yet efficient SAT solver with reference paper"
-HOMEPAGE="http://minisat.se/Main.html"
+HOMEPAGE="http://minisat.se/Main.html
+ https://github.com/stp/minisat/"
SRC_URI="https://github.com/stp/${PN}/archive/releases/${PV}.tar.gz -> ${P}.tar.gz
doc? ( http://minisat.se/downloads/MiniSat.pdf )"
-S="${WORKDIR}/${PN}-releases-${PV}"
+S="${WORKDIR}"/${PN}-releases-${PV}
LICENSE="MIT"
SLOT="0/${PV}"
@@ -19,9 +20,13 @@ IUSE="doc"
RDEPEND="sys-libs/zlib:="
DEPEND="${RDEPEND}"
-PATCHES=( "${FILESDIR}"/${P}-cmake.patch )
+PATCHES=(
+ "${FILESDIR}"/${P}-cmake.patch
+ "${FILESDIR}"/${P}-musl.patch
+)
src_install() {
cmake_src_install
+
use doc && dodoc "${DISTDIR}"/MiniSat.pdf
}