[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/opensmt/, sci-mathematics/opensmt/files/

2023-11-07 Thread Maciej Barć
commit: de122ee20e5f4b74dd53fbe68fcc25de0de8dbe3
Author: Kostadin Shishmanov  tutanota  com>
AuthorDate: Tue Nov  7 17:45:28 2023 +
Commit: Maciej Barć  gentoo  org>
CommitDate: Tue Nov  7 18:50:12 2023 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=de122ee2

sci-mathematics/opensmt: fix build with gcc 14

Closes: https://bugs.gentoo.org/916855
Signed-off-by: Kostadin Shishmanov  tutanota.com>
Closes: https://github.com/gentoo/gentoo/pull/33708
Signed-off-by: Maciej Barć  gentoo.org>

 .../opensmt/files/opensmt-2.5.2-gcc-14.patch   | 68 ++
 sci-mathematics/opensmt/opensmt-2.5.2.ebuild   |  4 +-
 2 files changed, 71 insertions(+), 1 deletion(-)

diff --git a/sci-mathematics/opensmt/files/opensmt-2.5.2-gcc-14.patch 
b/sci-mathematics/opensmt/files/opensmt-2.5.2-gcc-14.patch
new file mode 100644
index ..c5957641fff7
--- /dev/null
+++ b/sci-mathematics/opensmt/files/opensmt-2.5.2-gcc-14.patch
@@ -0,0 +1,68 @@
+From f30e983f876df3bd34571f9d554b3ebe226dd4bd Mon Sep 17 00:00:00 2001
+From: Kostadin Shishmanov 
+Date: Tue, 7 Nov 2023 16:38:39 +0200
+Subject: [PATCH] Add include  to fix building with gcc 14
+
+Gentoo bug:
+https://bugs.gentoo.org/916855
+
+Upstream PR:
+https://github.com/usi-verification-and-security/opensmt/pull/653
+
+Signed-off-by: Kostadin Shishmanov 
+---
+ src/logics/Logic.cc   | 1 +
+ src/pterms/PtStore.cc | 1 +
+ src/simplifiers/BoolRewriting.cc  | 1 +
+ src/tsolvers/egraph/EnodeStore.cc | 2 ++
+ 4 files changed, 5 insertions(+)
+
+diff --git a/src/logics/Logic.cc b/src/logics/Logic.cc
+index 2619df1fd..84b04d515 100644
+--- a/src/logics/Logic.cc
 b/src/logics/Logic.cc
+@@ -21,6 +21,7 @@
+ #include 
+ #include 
+ #include 
++#include 
+ 
+ using namespace std;
+ 
+diff --git a/src/pterms/PtStore.cc b/src/pterms/PtStore.cc
+index 377642947..63c6f56f3 100644
+--- a/src/pterms/PtStore.cc
 b/src/pterms/PtStore.cc
+@@ -29,6 +29,7 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE 
SOFTWARE.
+ #include "OsmtApiException.h"
+ 
+ #include 
++#include 
+ 
+ const int PtStore::ptstore_vec_idx = 1;
+ const int PtStore::ptstore_buf_idx = 2;
+diff --git a/src/simplifiers/BoolRewriting.cc 
b/src/simplifiers/BoolRewriting.cc
+index e2aa52b2c..196a642c4 100644
+--- a/src/simplifiers/BoolRewriting.cc
 b/src/simplifiers/BoolRewriting.cc
+@@ -5,6 +5,7 @@
+ #include "BoolRewriting.h"
+ #include "Logic.h"
+ #include 
++#include 
+ 
+ // Replace subtrees consisting only of ands / ors with a single and / or term.
+ // Search a maximal section of the tree consisting solely of ands / ors.  The
+diff --git a/src/tsolvers/egraph/EnodeStore.cc 
b/src/tsolvers/egraph/EnodeStore.cc
+index 2bed3302b..de2216410 100644
+--- a/src/tsolvers/egraph/EnodeStore.cc
 b/src/tsolvers/egraph/EnodeStore.cc
+@@ -28,6 +28,8 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE 
SOFTWARE.
+ #include "Symbol.h"
+ #include "Logic.h"
+ 
++#include 
++
+ EnodeStore::EnodeStore(Logic& l)
+   : logic(l)
+   , ea(1024*1024)

diff --git a/sci-mathematics/opensmt/opensmt-2.5.2.ebuild 
b/sci-mathematics/opensmt/opensmt-2.5.2.ebuild
index 04e39c2ae269..73c64f7b50df 100644
--- a/sci-mathematics/opensmt/opensmt-2.5.2.ebuild
+++ b/sci-mathematics/opensmt/opensmt-2.5.2.ebuild
@@ -36,7 +36,9 @@ BDEPEND="
test? ( dev-cpp/gtest )
 "
 
-# PATCHES=( "${FILESDIR}"/${PN}-2.4.3-musl.patch )
+PATCHES=(
+   "${FILESDIR}/${PN}-2.5.2-gcc-14.patch"
+)
 
 src_prepare() {
cmake_src_prepare



[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/opensmt/, sci-mathematics/opensmt/files/

2023-02-06 Thread Maciej Barć
commit: d7cebc801072df5274120a7f38644474e1168ed1
Author: Maciej Barć  gentoo  org>
AuthorDate: Mon Feb  6 16:46:59 2023 +
Commit: Maciej Barć  gentoo  org>
CommitDate: Mon Feb  6 17:23:18 2023 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=d7cebc80

sci-mathematics/opensmt: fix build on musl

Bug: https://github.com/usi-verification-and-security/opensmt/pull/590
Closes: https://bugs.gentoo.org/890794
Signed-off-by: Maciej Barć  gentoo.org>

 .../opensmt/files/opensmt-2.4.3-musl.patch | 132 +
 sci-mathematics/opensmt/opensmt-2.4.3-r1.ebuild|   2 +
 2 files changed, 134 insertions(+)

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 ..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?= 
+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ć 
+---
+ 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 
+ #include 
+ 
+-#if defined(__linux__)
++#if defined(__GLIBC__)
+ #include 
+ #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 
+ #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 
+ #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 
+ #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 
+ #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 
+ #endif
+ 
+@@ -55,7 +55,7 @@ int main( int argc, char * argv[] )
+ // the repeatability of experiments that might be compromised
+