summaryrefslogtreecommitdiff
path: root/sci-mathematics/opensmt
diff options
context:
space:
mode:
authorV3n3RiX <venerix@koprulu.sector>2023-02-06 21:22:20 +0000
committerV3n3RiX <venerix@koprulu.sector>2023-02-06 21:22:20 +0000
commit7842f444601c620f190db9801e59c4f11e686f15 (patch)
treebd6f22298de6de933ea0b3b327ce4b26a2dc1ca5 /sci-mathematics/opensmt
parent734ebb79080aab27a82cb1a8380d4fc581e25638 (diff)
gentoo auto-resync : 06:02:2023 - 21:22:20
Diffstat (limited to 'sci-mathematics/opensmt')
-rw-r--r--sci-mathematics/opensmt/Manifest4
-rw-r--r--sci-mathematics/opensmt/files/opensmt-2.4.3-musl.patch132
-rw-r--r--sci-mathematics/opensmt/opensmt-2.4.3-r1.ebuild2
-rw-r--r--sci-mathematics/opensmt/opensmt-2.4.3.ebuild70
4 files changed, 136 insertions, 72 deletions
diff --git a/sci-mathematics/opensmt/Manifest b/sci-mathematics/opensmt/Manifest
index 8c9168b70006..197f0963ea9b 100644
--- a/sci-mathematics/opensmt/Manifest
+++ b/sci-mathematics/opensmt/Manifest
@@ -1,4 +1,4 @@
+AUX opensmt-2.4.3-musl.patch 4317 BLAKE2B 7f1349452d31edac8e90ba322396fd4725399512481b035f6996b5ec4ad09cc1af3579668ee4da79deb198befdde2cd2fbb9fcc4159ec97b0aaedfce9e73a443 SHA512 09c2cea9928e89806136c5cae2403eb4168bf3984974f6212c0c1b9857affd3b1559bf6cb1bb5a0b8a3a6d9a340cca559446fe4d535b87b1f5b2cdc176f7b7ad
DIST opensmt-2.4.3.tar.gz 1912077 BLAKE2B d945d5b85d81b9b991f2f881f2d8f160dbefad8ce6484cf0d28c9a35c0fa64d18f45442a59cdd45bd29fcf526a09717d902d30376dfe2784de2d4df9627f803b SHA512 a2adbbdebb133d7e97428c0ac9bf4c2413c95bca61567c5475f889f550904fc33a385712536c9026b38a1645b73c943876fa36724b634db061cb7cc0932543f2
-EBUILD opensmt-2.4.3-r1.ebuild 1484 BLAKE2B cc6abf84eda262a35389464c2de630ffca88c672509708712c822e033d2eea66ac673fdd65fc91069fd333cff83f1a257810629458874a3a9282137006694165 SHA512 9d97fb719d2e179b26d7e6bbf5b7abfb5e649a9358c5744b1a3aa5da1ae70270dcf47d87d1da0d32c874c50cf6f1c7819840a3815c3c7542e036989ab549efc2
-EBUILD opensmt-2.4.3.ebuild 1560 BLAKE2B 58b42d294098458926e79378b48aad42a75eebf4fa2feb532cfcbc91fbb653812596d8969eca973d2f66af29e7aca536874025c1aeb167ba8613a50a08d07864 SHA512 f77aa8dbe36c4f85119a3761e05d21837dfb750f3e9fe69c1ea60c91f75ffc500759105ecf6a78ed642a7d1533faa62e2ef386caeed472952e1b822759d1a974
+EBUILD opensmt-2.4.3-r1.ebuild 1527 BLAKE2B 545d60ba243da4b5ed4325e4e16dcf0f9f4f8a770e33b3bb07d8a8bb9eaffad60efa3fdbb2d58c083443c7504ff96354dde2abc9925d6bd9bac6d9a8eb0ef88b SHA512 4837003c49d520012c38586a7316beaa69e81ced190edfcc91b75ab145a78863417c4db0bb418be65d4636c5e4810128fb4702e5cfc80da0810129854df6783c
MISC metadata.xml 798 BLAKE2B 173b47beab9c5ecc15caf32dd0514230f5dbefea8a9c75b33ab4f4cc51bc7e66e1a90240c3d0ba55f09959accf4203136c2b1ab400c2289e8329906cc0aabb56 SHA512 e3acadb473098ff0985b15ce2fb7ffcd8ef2f29fde2736a9c7e5d297a0857e358cdfa508b9f030add29f8bd808ce1594961e9a92768cbc8cff155a8195bd392e
diff --git a/sci-mathematics/opensmt/files/opensmt-2.4.3-musl.patch b/sci-mathematics/opensmt/files/opensmt-2.4.3-musl.patch
new file mode 100644
index 000000000000..5f80a0de116c
--- /dev/null
+++ b/sci-mathematics/opensmt/files/opensmt-2.4.3-musl.patch
@@ -0,0 +1,132 @@
+From e88b83b3b52ebc6ff4cdf1f92a876861fc2c5598 Mon Sep 17 00:00:00 2001
+From: =?UTF-8?q?Maciej=20Bar=C4=87?= <xgqt@gentoo.org>
+Date: Mon, 6 Feb 2023 17:27:34 +0100
+Subject: [PATCH] use fpu_control only on glibc
+MIME-Version: 1.0
+Content-Type: text/plain; charset=UTF-8
+Content-Transfer-Encoding: 8bit
+
+Signed-off-by: Maciej Barć <xgqt@gentoo.org>
+---
+ bin/opensmt.C | 4 ++--
+ src/bin/opensmt.cc | 2 +-
+ src/minisat/core/Main.C | 4 ++--
+ src/minisat/simp/Main.C | 4 ++--
+ src/minisat/utils/System.h | 2 +-
+ src/parallel/opensmtSplitter.cc | 4 ++--
+ 6 files changed, 10 insertions(+), 10 deletions(-)
+
+diff --git a/bin/opensmt.C b/bin/opensmt.C
+index cb9c8943b..898a8fdd3 100644
+--- a/bin/opensmt.C
++++ b/bin/opensmt.C
+@@ -44,7 +44,7 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ #include <csignal>
+ #include <iostream>
+
+-#if defined(__linux__)
++#if defined(__GLIBC__)
+ #include <fpu_control.h>
+ #endif
+
+@@ -84,7 +84,7 @@ int main( int argc, char * argv[] )
+ // the repeatability of experiments that might be compromised
+ // by the floating point unit approximations on doubles
+ //
+-#if defined(__linux__) && !defined( SMTCOMP )
++#if defined(__GLIBC__) && !defined( SMTCOMP )
+ fpu_control_t oldcw, newcw;
+ _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
+ #endif
+diff --git a/src/bin/opensmt.cc b/src/bin/opensmt.cc
+index 6db12ffd8..67bfcd712 100644
+--- a/src/bin/opensmt.cc
++++ b/src/bin/opensmt.cc
+@@ -47,7 +47,7 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ #endif
+ #endif // ENABLE_LINE_EDITING
+
+-#if defined(__linux__)
++#if defined(__GLIBC__)
+ #include <fpu_control.h>
+ #endif
+
+diff --git a/src/minisat/core/Main.C b/src/minisat/core/Main.C
+index acef32cd5..2c232b71b 100644
+--- a/src/minisat/core/Main.C
++++ b/src/minisat/core/Main.C
+@@ -74,7 +74,7 @@ static inline uint64_t memUsed(void) {
+ static inline uint64_t memUsed() { return 0; }
+ #endif
+
+-#if defined(__linux__)
++#if defined(__GLIBC__)
+ #include <fpu_control.h>
+ #endif
+
+@@ -287,7 +287,7 @@ int main(int argc, char** argv)
+
+
+ reportf("This is MiniSat 2.0 beta\n");
+-#if defined(__linux__)
++#if defined(__GLIBC__)
+ fpu_control_t oldcw, newcw;
+ _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
+ reportf("WARNING: for repeatability, setting FPU to use double precision\n");
+diff --git a/src/minisat/simp/Main.C b/src/minisat/simp/Main.C
+index b6d194631..a3f22fb4f 100644
+--- a/src/minisat/simp/Main.C
++++ b/src/minisat/simp/Main.C
+@@ -74,7 +74,7 @@ static inline uint64_t memUsed(void) {
+ static inline uint64_t memUsed() { return 0; }
+ #endif
+
+-#if defined(__linux__)
++#if defined(__GLIBC__)
+ #include <fpu_control.h>
+ #endif
+
+@@ -244,7 +244,7 @@ const char* hasPrefix(const char* str, const char* prefix)
+ int main(int argc, char** argv)
+ {
+ reportf("This is MiniSat 2.0 beta\n");
+-#if defined(__linux__)
++#if defined(__GLIBC__)
+ fpu_control_t oldcw, newcw;
+ _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
+ reportf("WARNING: for repeatability, setting FPU to use double precision\n");
+diff --git a/src/minisat/utils/System.h b/src/minisat/utils/System.h
+index 5f9dc3f53..4b7f9c9f5 100644
+--- a/src/minisat/utils/System.h
++++ b/src/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/src/parallel/opensmtSplitter.cc b/src/parallel/opensmtSplitter.cc
+index 05246e187..4b8c01a1a 100644
+--- a/src/parallel/opensmtSplitter.cc
++++ b/src/parallel/opensmtSplitter.cc
+@@ -27,7 +27,7 @@
+ #endif
+ #endif // ENABLE_LINE_EDITING
+
+-#if defined(__linux__)
++#if defined(__GLIBC__)
+ #include <fpu_control.h>
+ #endif
+
+@@ -55,7 +55,7 @@ int main( int argc, char * argv[] )
+ // the repeatability of experiments that might be compromised
+ // by the floating point unit approximations on doubles
+ //
+-#if defined(__linux__)
++#if defined(__GLIBC__)
+ fpu_control_t oldcw, newcw;
+ _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
+ #endif
diff --git a/sci-mathematics/opensmt/opensmt-2.4.3-r1.ebuild b/sci-mathematics/opensmt/opensmt-2.4.3-r1.ebuild
index b1e67e45cbad..d02cd8ed4430 100644
--- a/sci-mathematics/opensmt/opensmt-2.4.3-r1.ebuild
+++ b/sci-mathematics/opensmt/opensmt-2.4.3-r1.ebuild
@@ -36,6 +36,8 @@ BDEPEND="
test? ( dev-cpp/gtest )
"
+PATCHES=( "${FILESDIR}"/${P}-musl.patch )
+
src_prepare() {
cmake_src_prepare
diff --git a/sci-mathematics/opensmt/opensmt-2.4.3.ebuild b/sci-mathematics/opensmt/opensmt-2.4.3.ebuild
deleted file mode 100644
index 089f834988bc..000000000000
--- a/sci-mathematics/opensmt/opensmt-2.4.3.ebuild
+++ /dev/null
@@ -1,70 +0,0 @@
-# Copyright 1999-2023 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=8
-
-inherit cmake
-
-DESCRIPTION="Compact and open-source SMT-solver written in C++"
-HOMEPAGE="http://verify.inf.usi.ch/opensmt/
- https://github.com/usi-verification-and-security/opensmt/"
-
-if [[ ${PV} == *9999* ]] ; then
- inherit git-r3
- EGIT_REPO_URI="https://github.com/usi-verification-and-security/${PN}.git"
-else
- SRC_URI="https://github.com/usi-verification-and-security/${PN}/archive/v${PV}.tar.gz
- -> ${P}.tar.gz"
- KEYWORDS="~amd64 ~x86"
-fi
-
-LICENSE="MIT"
-SLOT="0/${PV}"
-IUSE="debug libedit +readline test"
-REQUIRED_USE="?? ( libedit readline )"
-RESTRICT="!test? ( test )"
-
-RDEPEND="
- dev-libs/gmp:=
- readline? ( sys-libs/readline:= )
- libedit? ( dev-libs/libedit:= )
-"
-DEPEND="${RDEPEND}"
-BDEPEND="
- sys-devel/bison
- sys-devel/flex
- test? ( dev-cpp/gtest )
-"
-
-src_prepare() {
- cmake_src_prepare
-
- echo "add_subdirectory(unit)" > "${S}"/test/CMakeLists.txt || die
- echo "add_subdirectory(unit)" > "${S}"/parallel-test/CMakeLists.txt || die
-}
-
-src_configure() {
- local CMAKE_BUILD_TYPE
- if use debug ; then
- CMAKE_BUILD_TYPE=Debug
- else
- CMAKE_BUILD_TYPE=Release
- fi
-
- local -a mycmakeargs=(
- -DPACKAGE_TESTS=$(usex test)
- -DUSE_READLINE=$(usex readline)
- )
- if use readline || use libedit ; then
- mycmakeargs+=( -DENABLE_LINE_EDITING=ON )
- fi
- cmake_src_configure
-}
-
-src_install() {
- cmake_src_install
-
- rm "${ED}"/usr/lib/libopensmt.a || die
- dodir /usr/$(get_libdir)
- mv "${ED}"/usr/lib/libopensmt.* "${ED}"/usr/$(get_libdir)/ || die
-}