summaryrefslogtreecommitdiff
path: root/sci-mathematics
diff options
context:
space:
mode:
Diffstat (limited to 'sci-mathematics')
-rw-r--r--sci-mathematics/Manifest.gzbin18375 -> 18365 bytes
-rw-r--r--sci-mathematics/bertini/Manifest3
-rw-r--r--sci-mathematics/bertini/bertini-1.6.ebuild65
-rw-r--r--sci-mathematics/minisat/Manifest3
-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
-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
-rw-r--r--sci-mathematics/vampire/Manifest5
-rw-r--r--sci-mathematics/vampire/files/vampire-4.6.1-musl.patch40
-rw-r--r--sci-mathematics/vampire/vampire-4.6.1-r2.ebuild4
-rw-r--r--sci-mathematics/vampire/vampire-4.7-r1.ebuild10
14 files changed, 308 insertions, 84 deletions
diff --git a/sci-mathematics/Manifest.gz b/sci-mathematics/Manifest.gz
index 0f5ee0cb9de3..45787f7306fa 100644
--- a/sci-mathematics/Manifest.gz
+++ b/sci-mathematics/Manifest.gz
Binary files differ
diff --git a/sci-mathematics/bertini/Manifest b/sci-mathematics/bertini/Manifest
index cdba6fd2df4b..62327b14000b 100644
--- a/sci-mathematics/bertini/Manifest
+++ b/sci-mathematics/bertini/Manifest
@@ -1,3 +1,6 @@
DIST BertiniSource_v1.4.tar.gz 1827401 BLAKE2B 4869ef0b73a3688df504bff84dc36682700c4916dcfdca68ae3a1bf87ceda2f664c35e2b5fe4b5d0859bbab110a2fa1e474361847db897859c3d5d17c48f122f SHA512 bb53f8ed24a0f21e95b4e373be36039b69ea0ddb11ad8240bcf52ce64436a56c1f2057a5d733d017fdf68cfb3598a473e1f12b4659308890e2e2575b7d8143f6
+DIST BertiniSource_v1.6.tar.gz 4957384 BLAKE2B 395ca96c52b167eaefe672d31c79c5791d92b1375059c0e6244042f2e987d011d0c9b5d6590555654e0b23d15aec2dcdcb2c1fa23fec73fb5c0e307c960c334b SHA512 04e0964e714ede697d49aeecd4008102d653472664d22fc2f491e93d8a5cc18a9db2980d57a23a8ea88f1fab9b98aeb2d36fc112c0a0aa3510e152a8edcb1f95
+DIST BertiniUsersManual.pdf 1188567 BLAKE2B d940e95a86ec2b81d5afff3ade9fe28f5c3034e9250a844d3b8ad4de5ded1b4b98a68d2da1f61e17fd7f25ed481522805505850fc011f2a5642ca7cee4e86c8f SHA512 f206645cf20eb4da9e00b62440e612e0037fe02882167cdb48074d4532b913a940b551f4624fd00309c8f5d2a9775350430b143277b1dfe8064fd899a58408d9
EBUILD bertini-1.4.ebuild 1323 BLAKE2B 91903ca89a071f3f011a047b8d5a37d140f9665d74d1f17ebc3678f86d65cea5642ba266c83ca1a3b435d5d1783eb54c7afc503c3366182c81e4097eacb4c006 SHA512 cebc05cb552daa75e8959dc6d0bf5fd0890fdda00d1bb6c4d502ef2bd32bc5c12bdd7660a1b89a2dcab1839ac2fcc9b6ab5d560371815688ecd7387d94763011
+EBUILD bertini-1.6.ebuild 1401 BLAKE2B ed9b252c03a4670b0b30919a208c47f97ca9597685f020c36241ac43bf5546de10d78dfc78b5aea3d89e3e9401d15d3c8f8ec69df8ca2c72862b6fe944930c99 SHA512 077dbcf4287b84c8bac9d2bba6ba85a57c271cd2792c1af3cebc59435b55391bae6a9432697c1d334f84f19c2ac61a6ede416935f20eda4fde0d403269e0d690
MISC metadata.xml 824 BLAKE2B 7151b5c87b9366cf0d67f70239ecb9f19403ccb1dbe3d2ac2238d8676417acbfc9fdef79ed5030ed7004e6f6e71c7384ed68e6e11319e82ae29532aa64e4ac46 SHA512 6be583a25b2a6c52dfa8c24e48a3055c29b8f9db64879e28b968de2e62e843a40d2cab8eef58911bc6fadaeaaa3f05f32a5525f2ef30f092880281dd848142e9
diff --git a/sci-mathematics/bertini/bertini-1.6.ebuild b/sci-mathematics/bertini/bertini-1.6.ebuild
new file mode 100644
index 000000000000..5fe2bd594d0f
--- /dev/null
+++ b/sci-mathematics/bertini/bertini-1.6.ebuild
@@ -0,0 +1,65 @@
+# Copyright 1999-2023 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+MYP=BertiniSource_v${PV}
+
+inherit toolchain-funcs flag-o-matic
+
+DESCRIPTION="Software for Numerical Algebraic Geometry"
+HOMEPAGE="http://bertini.nd.edu"
+SRC_URI="https://bertini.nd.edu/${MYP}.tar.gz
+ doc? ( https://bertini.nd.edu/BertiniUsersManual.pdf )"
+S="${WORKDIR}"/${MYP/./}
+
+LICENSE="bertini"
+SLOT="0"
+KEYWORDS="~amd64 ~x86"
+IUSE="doc examples +optimization"
+
+RDEPEND="
+ dev-libs/gmp
+ dev-libs/mpfr
+"
+DEPEND="${RDEPEND}"
+BDEPEND="
+ sys-devel/bison
+ sys-devel/flex
+"
+
+DOCS=( AUTHORS ChangeLog NEWS README )
+
+src_prepare() {
+ default
+
+ # bug #723328
+ append-cflags -fcommon
+
+ # Ensure this is before the CFLAGS sed
+ # or breakage occurs if 'gcc' is in your CFLAGS
+ sed -i -e "s/gcc/$(tc-getCC)/" src/Makefile || die
+
+ if ! use optimization ; then
+ sed -i -e "s/\$(OPT)/ ${CFLAGS} ${CXXFLAGS} ${LDFLAGS}/" src/Makefile || die
+ else
+ # If people want the optimisation offered by upstream,
+ # let's ensure they don't accidentally override it.
+ filter-flags -O?
+ sed -i -e "s/\$(OPT)/ \$(OPT) ${CFLAGS} ${LDFLAGS}/" src/Makefile || die
+ fi
+}
+
+src_configure() {
+ econf --prefix=/usr --includedir=/usr/include/${PN}
+
+ use doc && DOCS+=( "${DISTDIR}"/BertiniUsersManual.pdf )
+}
+
+src_install() {
+ emake DESTDIR="${D}" install
+
+ find "${ED}" -name "*.la" -delete || die
+
+ einstalldocs
+}
diff --git a/sci-mathematics/minisat/Manifest b/sci-mathematics/minisat/Manifest
index ed887b8cb2cf..71b43cad19ff 100644
--- a/sci-mathematics/minisat/Manifest
+++ b/sci-mathematics/minisat/Manifest
@@ -1,5 +1,6 @@
AUX minisat-2.2.1-cmake.patch 1971 BLAKE2B f194354706bafb51111648221b9ccb03c808caf245a45a0cc00bfd06d5167e46963bfe3c66164dd9df34373cc74ea36e4b11b69b9806363decc925b4db469d07 SHA512 5ceb69491e6a5dd6d7438f567a9c92f7c39e7e93fae776f901e6df1b855d2242941df3bf34e8e147992a9ed5b5120704172c4c9502db5f8baf962c058d26679e
+AUX minisat-2.2.1-musl.patch 1602 BLAKE2B 8eb10efbb7227548fa7024fb520d31389be7883bb719a0ac8737f5bf926484383d64cef22a97e8bafadb474174392f1eaeb9971d5f5b7da6b8e2713c26988174 SHA512 d6affc70cae105991b739a3ebdae22da6eb74cda8878d4e64fb1b96287ae40c530ec7b73199f11ecaf9403edf1e1fbe9b8b8ccc1a691db6ac326c4d28368b070
DIST MiniSat.pdf 327416 BLAKE2B 77f77d763c9554680b4c5e1688801e8462102e8ddbcc3b53badccee17a98f935ef0e971a636abeb04021a2b3a3e9d6acfe4828b5dd20e6ef8733d71788cc31b0 SHA512 94e70c721740c0b7fd52621c7a5e43dd9207eed92e60a1c64ee63b541b9861d2580d14ba64c49c6c4f273ac028ded43bc944c71131e51693cdd7d1763af582f6
DIST minisat-2.2.1.tar.gz 50485 BLAKE2B 58c292f0b90dd459fa29fadbf9e2b20106406c08df9ce98f40138b12a8f001b4ab72f661815d1254c6c90158c3d6e3df339c784552605a935ebc5e703b2d8768 SHA512 a69734e1a70fe056f9dfd479fe4e6e25bc418d3631c1c2d0dea1190ffe9f86b1fc5e9aabaf3772a752fe654551f1e84e47fcb8655f6fe25176efc8d8bc96c663
-EBUILD minisat-2.2.1-r1.ebuild 639 BLAKE2B 651b93daea22d747fb472004c0f48643490ee8c15f1e1de43aa73f4df848309b610b01c8e79530f64517a78e5720c6c22b94e95b87871ea63a600a67ee09a8e7 SHA512 5adda43272e97882dcff9df129e18720eeb6e2dd7ead21a86f3448af08300699ed2ba01e0d53951dfd27ac7d7e4031766fd3c0a9c5139a1b1d60882493556286
+EBUILD minisat-2.2.1-r1.ebuild 705 BLAKE2B e20e83162ab6943b437341322c69ed9df7897cbea6246c9df4e1379e73f21190b6e8337d70c51e9f64561306c97957a2fe0706818d2b11b07527c913ba3bd236 SHA512 3bd870cf2709c3f75d17f7d43f8bc9fd45cab9ea95589674772448511b2c2602b7ebbabcac25448dd181eafbd785ff2e60565f0cc7518cf5acc1fa8706877664
MISC metadata.xml 1244 BLAKE2B 7ef490fc9e45d1f9af7e5b40028614d71557e055fea15289dffcf4afc16fe72ecfa48b4dc7508ee042f603bd7035ccdc529b3640f33d67e96b3b5ede433455c4 SHA512 e6dbcbc2433da6491c94eefbcdf78d5634ca17c4c2e6174a832b46b75a6771cb1b7d92a3fe14d739dc9215a78126e40fe8447b2b3a65c355f9addcf4084ffe3d
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
}
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
-}
diff --git a/sci-mathematics/vampire/Manifest b/sci-mathematics/vampire/Manifest
index 23eeb3307578..6bacda87b101 100644
--- a/sci-mathematics/vampire/Manifest
+++ b/sci-mathematics/vampire/Manifest
@@ -1,5 +1,6 @@
+AUX vampire-4.6.1-musl.patch 1538 BLAKE2B 50162dd493cc004643b895a62b6a07abc08e3d8ac5e53e8f523bcf6fc3d7f0847f0f1dfa25107aadff7bbc4d51bd9299e5f11cdfa7f3247254c7d6c2847026f6 SHA512 b94095925b55ce17aae299c7259bab3b062cae7640a24600f6dd0da02da2cff7d3e505abfe08816363c5a27bd4346536dcf6a33975490b9a6a037c3bf617d862
DIST vampire-4.6.1.tar.gz 1511760 BLAKE2B 52ede8ac009379b15bc57b2ffe45965cbaf772f0e90bc619d859b85b77ce81eadbdd7ddae7c5e0e9cc69564a07f0abefa17109f7192e6afe634a5a929817fe92 SHA512 7ffeee64e9e4666344c0f9155c7e980920666813388416062cee89e43003fef5a8a54b8656cc42d2fa58b6fb3b87ef7f2c671bfc6787075df4058dcc3a1d46e1
DIST vampire-4.7.tar.gz 1462358 BLAKE2B 10fdf4076bbcd7113da575d19890634a5142dd6917c028eb7ae0e94405df9e6915fc6127956d39b6f9f97242958b0fa04fa9e835853f09cec381786862009ef5 SHA512 978169a9b4d561dce1d55aa9a61a8b302657ff758036309d9c5f58a5d9271b874ac020d110fbb2a16d34f2ccdd10a497eb469829c91d58530dba5e1cd8978d78
-EBUILD vampire-4.6.1-r2.ebuild 1291 BLAKE2B 030e21c423d15f868d605b509bc8028c0f11503535f0bbdf0e454d4cd375a1feb57ef898d0a38c9a2e7fa38efb48766aac024517b1d221020b510f7a8aff300b SHA512 a9df850052becd4b3093a24a26d6b598207db8513de7364636e89a0d3de9ed88cf66c50c6cc64e314bac0fc6bcb51f2ce55624ecaa8d720276a51a178c3e82e4
-EBUILD vampire-4.7-r1.ebuild 1379 BLAKE2B 24300b4f4dddc1755a28a4d08ced379050da9c7c10a4bb5900d4e8d44a865d73929b8729723c243ab2e37ffe17ba79c46e7fbe535c6d8f5279c8c27bfe5d7181 SHA512 8af44550e1b69848d883236b07713efb4bb0f4718aecf77eb3c05f8e7adbe5207fb01de5552e831bb2d18b32046c6431416dfdd37e225e6f7dc9d03a7a360e1b
+EBUILD vampire-4.6.1-r2.ebuild 1334 BLAKE2B c60fe0a9b8b030f3888aa88dfffb0a8626448dfa1957e3a87896d13bce97f451f16e136539141a5e86710e6e82719594c79bfee8f0a040207c79310c583e0055 SHA512 6c7f5fd966b8d15af8ab8db7c51d2873dba52e00555cf0e5490228bed16ba871cbf36d1131921ee48f7b17b6e03defb5cceed684f684c55c2f1a6d3444595e8c
+EBUILD vampire-4.7-r1.ebuild 1466 BLAKE2B 6b0dfdd8976d71f7a6d20821a9e42e3e93e0fc10dcd9e650ef589fe38077c335137b3667e11c742ce2ec327c5929eed447019def81c83fa40561a9c39a9d8a76 SHA512 8ae1f1bc249627085a8aa58f778a9a826fc9d5a1a703bc1fc7e84c3d66c960974705ca069a5674c669c908b728d91859b3e79d8067a07f15b703392a25532977
MISC metadata.xml 1020 BLAKE2B 6e798243e207d09fac240c73cda8918b300706a19d53918b3ce78e847146ad3676a39d9be8e020b678c20d7fe02da0eab57519ea2c5841eeeea0b8a680045928 SHA512 dc82a586070c97db278ef17a24384436548b2a968d18ead7d148f654bab4ad846e685ac2ae2f7db8048b25115b673bcf8223fa2813b370f9d6b6ac01dcf9040e
diff --git a/sci-mathematics/vampire/files/vampire-4.6.1-musl.patch b/sci-mathematics/vampire/files/vampire-4.6.1-musl.patch
new file mode 100644
index 000000000000..4d3d4c56041e
--- /dev/null
+++ b/sci-mathematics/vampire/files/vampire-4.6.1-musl.patch
@@ -0,0 +1,40 @@
+From 48733f4e2d9500b3bdc54563cf117c7fa07193ed Mon Sep 17 00:00:00 2001
+From: =?UTF-8?q?Maciej=20Bar=C4=87?= <xgqt@gentoo.org>
+Date: Mon, 6 Feb 2023 14:34:05 +0100
+Subject: [PATCH] Minisat/utils/System.*: 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>
+---
+ 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 942ddb712..2936faa5d 100644
+--- a/Minisat/utils/System.cc
++++ b/Minisat/utils/System.cc
+@@ -104,7 +104,7 @@ double Minisat::memUsedPeak(bool) {
+
+ 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 ecdde991b..fd501eeec 100644
+--- a/Minisat/utils/System.h
++++ b/Minisat/utils/System.h
+@@ -26,7 +26,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/vampire/vampire-4.6.1-r2.ebuild b/sci-mathematics/vampire/vampire-4.6.1-r2.ebuild
index d5579bce688d..0d3a66debc59 100644
--- a/sci-mathematics/vampire/vampire-4.6.1-r2.ebuild
+++ b/sci-mathematics/vampire/vampire-4.6.1-r2.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
@@ -32,6 +32,8 @@ RDEPEND="
"
DEPEND="${RDEPEND}"
+PATCHES=( "${FILESDIR}"/${P}-musl.patch )
+
src_configure() {
# -Werror=strict-aliasing warnings, bug #863269
filter-lto
diff --git a/sci-mathematics/vampire/vampire-4.7-r1.ebuild b/sci-mathematics/vampire/vampire-4.7-r1.ebuild
index 69e581237127..975da65ac817 100644
--- a/sci-mathematics/vampire/vampire-4.7-r1.ebuild
+++ b/sci-mathematics/vampire/vampire-4.7-r1.ebuild
@@ -1,9 +1,9 @@
-# Copyright 1999-2022 Gentoo Authors
+# Copyright 1999-2023 Gentoo Authors
# Distributed under the terms of the GNU General Public License v2
EAPI=8
-H=2d02e4655e1b08d1ca9ee7c0aade40f59f046460 # "bump to 4.7"
+[[ ${PV} == 4.7 ]] && COMMIT=2d02e4655e1b08d1ca9ee7c0aade40f59f046460 # "bump to 4.7"
inherit flag-o-matic cmake
@@ -15,9 +15,9 @@ if [[ ${PV} == *9999* ]] ; then
EGIT_REPO_URI="https://github.com/vprover/${PN}.git"
EGIT_SUBMODULES=()
else
- SRC_URI="https://github.com/vprover/${PN}/archive/${H}.tar.gz
+ SRC_URI="https://github.com/vprover/${PN}/archive/${COMMIT}.tar.gz
-> ${P}.tar.gz"
- S="${WORKDIR}"/${PN}-${H}
+ S="${WORKDIR}"/${PN}-${COMMIT}
KEYWORDS="~amd64 ~x86"
fi
@@ -36,6 +36,8 @@ RDEPEND="
"
DEPEND="${RDEPEND}"
+PATCHES=( "${FILESDIR}"/${PN}-4.6.1-musl.patch )
+
src_configure() {
# -Werror=strict-aliasing warnings, bug #863269
filter-lto
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 02:16:05 +0000