summaryrefslogtreecommitdiff
path: root/sci-mathematics
diff options
context:
space:
mode:
Diffstat (limited to 'sci-mathematics')
-rw-r--r--sci-mathematics/Manifest.gzbin19522 -> 19515 bytes
-rw-r--r--sci-mathematics/lean/Manifest2
-rw-r--r--sci-mathematics/lean/files/lean-3.50.3-gcc-13.patch10
-rw-r--r--sci-mathematics/lean/files/lean-CMakeLists-fix_flags.patch23
-rw-r--r--sci-mathematics/prover9/Manifest4
-rw-r--r--sci-mathematics/prover9/files/LADR-2009-11A-c99.patch25
-rw-r--r--sci-mathematics/prover9/files/LADR-2009-11A-stable-ordering.patch91
-rw-r--r--sci-mathematics/prover9/prover9-2009.11a-r2.ebuild (renamed from sci-mathematics/prover9/prover9-2009.11a-r1.ebuild)9
8 files changed, 124 insertions, 40 deletions
diff --git a/sci-mathematics/Manifest.gz b/sci-mathematics/Manifest.gz
index 42372d7d8f78..4950bb5753f5 100644
--- a/sci-mathematics/Manifest.gz
+++ b/sci-mathematics/Manifest.gz
Binary files differ
diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 91688109ddd1..a34e05dd0f47 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,6 +1,4 @@
-AUX lean-3.50.3-gcc-13.patch 263 BLAKE2B cf589616f4612319bbe1d21e798787a72da3d0f319cef3ef0042b8baa89d87066867311fd804862d43599a262c64e2b747a6c21415bb69137a3e8e59dd332155 SHA512 013fe4ec983c8ca612621319fad5fe66e081516979e4dace71f24ec72cac8d7fe2a021e701b2bcae1e87209783330c02b799cdb6c1274f7f8d3dc51efaf130b6
AUX lean-4.14.0-src-cmakelists.patch 1084 BLAKE2B d236998224c99aec69248b59f314e3347ac21acf3bcbe99e006004a67d985ee899db0ff3a7f920a477066085707813fd908fba8cbc4d6b0f7a43f1c1525263c7 SHA512 8dff3962980cf06526d83d10f5175eac8505cc365d50f816a3690c68029e3f2ce69356b8f963adcdad2b06cc936fbd99a9fccb6d7ec24ebbdcad4519e9274ea9
-AUX lean-CMakeLists-fix_flags.patch 1285 BLAKE2B 0507e553c1acf2a53c5267932127117d5ae5ba9015a08c88748b3d82c041f8d904d15cd033dd7934ac55c474fa75a5d4a46f680cc887fee37c05c3f5f3832839 SHA512 11a5918847e45aac7bf79e48d8f881ef5cd3e6b09dbb0979f3f0b88fd36458be21ebeb530158da801399a0cdc8fe382444ff338cd793cd9f1bfced90c5d5a71b
DIST lean-4.11.0.tar.gz 25790812 BLAKE2B d9a4eb15199f81c6757acf35fb17c795bb9d69158c7e7deb11d98a45bebf569dcda5f7733b2effd2be0eea879a6c7c24b270d97159e5898215e82e853320918c SHA512 2314659910b4d872c4ae0dda648a9cab9e1cc44cd4c55486a494b65b20fdae236ab9db99a42d7fb1a80030e300e95606065ee7dd27578b12a4c47fc8c102e2bb
DIST lean-4.14.0.tar.gz 28508743 BLAKE2B 692972402726a77ca9255edbecfc2bd30033d5c7137b00e85821d5bb74f7ed77398b19e7e3098eeecf6812ad9ca568a4076b11a91456b84f4ad78be8f6441286 SHA512 871169b3d7951934990a86a2b5d1741b00f4559c53c69ecdf0ca1c091426f1d7a6baa5ce69029dbecfc4a9dc9da9ee36b327cbef0ab28e80a9f64d34a2666c78
EBUILD lean-4.11.0.ebuild 1395 BLAKE2B 9dea5026d1cef60c08d7de76061cdd7401f3c49e551df397a02b61cc5ce4fa34dddd636a339013ac424b090635196d0b94142fa2af895f43d8a0dcfc2a5c009b SHA512 e336e331fafbaa6b658007e5e6b1fd726044bde52fbdda56935c9c65ff47b1942bc721365be74118a62c9439e2bb395bdca160e906237374e3c235cb62c17825
diff --git a/sci-mathematics/lean/files/lean-3.50.3-gcc-13.patch b/sci-mathematics/lean/files/lean-3.50.3-gcc-13.patch
deleted file mode 100644
index 273dd5161080..000000000000
--- a/sci-mathematics/lean/files/lean-3.50.3-gcc-13.patch
+++ /dev/null
@@ -1,10 +0,0 @@
---- a/shell/lean_js_main.cpp
-+++ b/shell/lean_js_main.cpp
-@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
-
- Author: Leonardo de Moura
- */
-+#include <cstdint>
- #include <iostream>
- #include <string>
- #include "shell/lean_js.h"
diff --git a/sci-mathematics/lean/files/lean-CMakeLists-fix_flags.patch b/sci-mathematics/lean/files/lean-CMakeLists-fix_flags.patch
deleted file mode 100644
index 1fd788fd79be..000000000000
--- a/sci-mathematics/lean/files/lean-CMakeLists-fix_flags.patch
+++ /dev/null
@@ -1,23 +0,0 @@
-index f0efdf425..4cd461986 100644
---- a/CMakeLists.txt
-+++ b/CMakeLists.txt
-@@ -194,7 +194,7 @@ set(CMAKE_CXX_FLAGS_DEBUG "-DLEAN_DEBUG -DLEAN_TRACE")
- set(CMAKE_CXX_FLAGS_MINSIZEREL "-DNDEBUG")
- set(CMAKE_CXX_FLAGS_RELEASE "-DNDEBUG")
- set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-DLEAN_DEBUG")
--set(CMAKE_CXX_FLAGS_GPROF "-O2 -g -pg")
-+set(CMAKE_CXX_FLAGS_GPROF "-g -pg")
-
- # OSX .dmg generation (this is working in progress)
- set(CPACK_DMG_BACKGROUND_IMAGE "${LEAN_SOURCE_DIR}/../images/lean.png")
-@@ -264,8 +264,8 @@ if (NOT MSVC)
- set(CMAKE_CXX_FLAGS "-Wall -Wextra -std=c++11 ${CMAKE_CXX_FLAGS}")
- set(CMAKE_CXX_FLAGS_DEBUG "-g3 ${CMAKE_CXX_FLAGS_DEBUG}")
- set(CMAKE_CXX_FLAGS_MINSIZEREL "-Os ${CMAKE_CXX_FLAGS_MINSIZEREL}")
-- set(CMAKE_CXX_FLAGS_RELEASE "-O3 ${CMAKE_CXX_FLAGS_RELEASE}")
-- set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-O2 -g3 ${CMAKE_CXX_FLAGS_RELWITHDEBINFO}")
-+ set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE}")
-+ set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-g3 ${CMAKE_CXX_FLAGS_RELWITHDEBINFO}")
- elseif (MULTI_THREAD)
- set(CMAKE_CXX_FLAGS_DEBUG "/MTd ${CMAKE_CXX_FLAGS_DEBUG}")
- set(CMAKE_CXX_FLAGS_MINSIZEREL "/MT ${CMAKE_CXX_FLAGS_MINSIZEREL}")
diff --git a/sci-mathematics/prover9/Manifest b/sci-mathematics/prover9/Manifest
index 2870eb375b49..dc6ac6fb21cb 100644
--- a/sci-mathematics/prover9/Manifest
+++ b/sci-mathematics/prover9/Manifest
@@ -1,5 +1,7 @@
+AUX LADR-2009-11A-c99.patch 609 BLAKE2B 8b547b98189c46e57d5c382a55f7c7ae681703139bbd5f90820e69207df50292e308b76a6953e5a172159d75dea1572d85844c036e2af75d0518c37a502d1dbf SHA512 dc188bf71ee16a7da12f4e32934fdd871f77312e2340cc8c08e3bf6b3609595b15cf55431d982f7e13f56538c666f828a8fda27be0610a1a057898e9d10c442d
AUX LADR-2009-11A-manpages.patch 13832 BLAKE2B dfd8d0ba6722d788b4e7662c0c4113cc06c32f2f45cdd32327896147435d3f730b464189ee1766a1c162a90cd730d917d8b29c3c241a94d65a3fc5833f3bbca1 SHA512 4c9f862b33d7b6b33b5e4a82b38418c6ae41b7adae565d376cc741608eb989e3846c1e98589dea62f7cadeb0b1f0f5814afe95ee6cf0da63c6961620d8b2677c
+AUX LADR-2009-11A-stable-ordering.patch 2632 BLAKE2B f2562676db9ec0d9dfbb85dc3f58acf30e793222c01bb57fbebc26bdb70a7fdc8d4d49037117fb666e61a3fe245630ca9f2123e53eb6deb525892d24ef4be062 SHA512 d641afa22b8f5cc7e605a3373885100a4d1518c2894d74b3b781aeba895eec4f59ad0ef3df435ed8076ec854b933dd9bce6baec25c82ce60dd1ef4f85f1a2103
DIST LADR-2009-11A-makefile.patch.xz 4300 BLAKE2B 3ea0860901876c43aeadcee7cf7eca02c31c88ca6670c867ef4a41b9adc2aa13edf36f45807713f7b200355f5086b43a17722071be81f58af1bc5d70327e3e41 SHA512 c1d2e27d991036af24a29deb4401fbf9687415d2a37bebabb9cfc77d8672e0804d974f92cbd7b8e16c0a0c10b75831847f7b8ddb94244d7e632de7b1be5081f1
DIST LADR-2009-11A.tar.gz 1795750 BLAKE2B ed44b1d0f5f5f3c9846ff578af10914421c79f580db9f9002f105b87d7af49fb6f2956b70d2ebfbd17b3a230d1065aadb1cc798ef7ebdad8749e66cea41120b6 SHA512 f26d3713eb2ba809fb3d55ce179e9d91555ab9166e075aa0843bafe57ce00f153cfed178b61993d4fd471655840e4f40775d75dac9fb5242a67e5d59c970dfc7
-EBUILD prover9-2009.11a-r1.ebuild 2579 BLAKE2B d865851dcefac71e1299db441c76b72663b4561b16a4ce20532dd4bca2881a4a4a59fdddc620b52fc2dbc5e5cdd0bcdca71473eddf0a0cad03f17d71600866f1 SHA512 18dd15a04f7e20570cde9fb3fd158db81858b6cab048111c515cd08d088147ee7cfe3bce665e0d744cb8f89824c10c8742f095b5e7ca5d8ec5e22b8ba9bba335
+EBUILD prover9-2009.11a-r2.ebuild 2643 BLAKE2B 042bcb063558a69ddcab0d84910f68f2af1a7bb580ebc4404590fca20d19626e985ce0540e7958f7f1fd757ad31c48fdbf7f1ea37d8fce2252eb790484384bae SHA512 5e5b413975ac4a8b00cd37a9885d5bb6758a170906891204510efd8044e36787d4b6633c8471fdf9306efbafaa11da87d9fc33a2184d15c1ec2e8c2d669fb1ff
MISC metadata.xml 535 BLAKE2B ba8d67e5b87bd740d24e591b21fdd1214ef0fcb2bb9442722c973fe1344b3d638b5aedbc332e74e82eb58fb16458343d22c752abaf2c913d49de89cf7b76e2f4 SHA512 f48643b65797eaa9f06513f41a54f857e349ef7ed111fb5611ef2741e4785dc33bb96be9405b6331b0a9c569e08eb1e6e0f104b8b6c8a0eb2593694ae3d6803d
diff --git a/sci-mathematics/prover9/files/LADR-2009-11A-c99.patch b/sci-mathematics/prover9/files/LADR-2009-11A-c99.patch
new file mode 100644
index 000000000000..a4da6e4fbbf6
--- /dev/null
+++ b/sci-mathematics/prover9/files/LADR-2009-11A-c99.patch
@@ -0,0 +1,25 @@
+Explicitly declare int values as ints.
+https://bugs.gentoo.org/886597
+https://bugs.gentoo.org/871261
+--- a/mace4.src/msearch.c
++++ b/mace4.src/msearch.c
+@@ -847,7 +847,7 @@
+ *************/
+
+ static
+-int next_domain_size(n)
++int next_domain_size(int n)
+ {
+ int top = (parm(Opt->end_size) == -1 ? INT_MAX : parm(Opt->end_size));
+
+--- a/mace4.src/select.c
++++ b/mace4.src/select.c
+@@ -233,7 +233,7 @@
+ *
+ *************/
+
+-int select_concentric_band(min_id, max_id, max_constrained)
++int select_concentric_band(int min_id, int max_id, int max_constrained)
+ {
+ int max = -1;
+ int id_of_max = -1;
diff --git a/sci-mathematics/prover9/files/LADR-2009-11A-stable-ordering.patch b/sci-mathematics/prover9/files/LADR-2009-11A-stable-ordering.patch
new file mode 100644
index 000000000000..9bf5154f05ae
--- /dev/null
+++ b/sci-mathematics/prover9/files/LADR-2009-11A-stable-ordering.patch
@@ -0,0 +1,91 @@
+Do not call clean in the middle of build. We start with clean tree, we build
+stuff with all the same flags, every time, we don't remove files from under
+make while it's in the process of building things with large jobs number
+or with shuffle.
+Pipe CFLAGS (and, transitively, LDFLAGS) to last place where they were missing
+https://bugs.gentoo.org/881475
+https://bugs.gentoo.org/911554
+https://bugs.gentoo.org/887409
+https://bugs.gentoo.org/728030
+--- a/ladr/Makefile
++++ b/ladr/Makefile
+@@ -36,7 +36,7 @@
+ $(INFE_OBJ) $(MODL_OBJ) $(MISC_OBJ)
+
+ libladr.la: $(OBJECTS)
+- libtool --tag=CC --mode=link $(CC) -shared -rpath /usr/lib -version-info 4:0:0 -o libladr.la $(OBJECTS) -lm
++ libtool --tag=CC --mode=link $(CC) $(CFLAGS) -shared -rpath /usr/lib -version-info 4:0:0 -o libladr.la $(OBJECTS) -lm
+
+ %.lo: %.c
+ libtool --tag=CC --mode=compile $(CC) -c $(CFLAGS) $(XFLAGS) -o $@ $<
+--- a/apps.src/Makefile
++++ b/apps.src/Makefile
+@@ -13,7 +13,7 @@
+
+ PROGRAMS = latfilter olfilter clausefilter idfilter renamer unfast clausetester rewriter isofilter0 isofilter isofilter2 dprofiles interpfilter upper-covers miniscope interpformat prooftrans mirror-flip perm3 sigtest directproof test_clause_eval test_complex complex gen_trc_defs
+
+-all: ladr apps install realclean
++all: ladr apps install
+
+ ladr:
+ cd ../ladr && $(MAKE) libladr.la
+@@ -24,7 +24,7 @@
+ realclean:
+ libtool --tag=CC --mode=clean /bin/rm -f *.o $(PROGRAMS)
+
+-install:
++install: apps
+ libtool --tag=CC --mode=install /bin/cp $(PROGRAMS) `pwd`/../bin
+
+ tags:
+--- a/mace4.src/Makefile
++++ b/mace4.src/Makefile
+@@ -27,7 +27,6 @@
+
+ ladr:
+ cd ../ladr && $(MAKE) libladr.la
+- $(MAKE) clean
+
+ mace4: libmace4.a mace4.o $(OBJECTS)
+ libtool --tag=CC --mode=link $(CC) $(CFLAGS) -o mace4 mace4.o libmace4.a ../ladr/libladr.la
+@@ -42,5 +42,5 @@
+ realclean:
+ libtool --tag=CC --mode=clean /bin/rm -f *.o *.a mace4
+
+-install:
++install: mace4
+ libtool --tag=CC --mode=install /bin/cp mace4 `pwd`/../bin
+--- a/provers.src/Makefile
++++ b/provers.src/Makefile
+@@ -28,19 +28,17 @@
+
+ ##############################################################################
+
+-all: libs $(PROGRAMS) install clean
++all: libs $(PROGRAMS) install
+
+ libs: ladr libmace4
+
+ ladr libladr:
+ cd ../ladr && $(MAKE) libladr
+- $(MAKE) clean
+
+ libmace libmace4:
+ cd ../mace4.src && $(MAKE) libmace4
+- $(MAKE) clean
+
+-install:
++install: libs $(PROGRAMS)
+ libtool --tag=CC --mode=install /bin/cp -p $(PROGRAMS) `pwd`/../bin
+
+ clean:
+--- a/test.src/Makefile
++++ b/test.src/Makefile
+@@ -16,7 +16,6 @@
+ all: ladr apps
+
+ ladr:
+- make clean
+ cd ../ladr && $(MAKE) libladr.la
+
+ clean:
diff --git a/sci-mathematics/prover9/prover9-2009.11a-r1.ebuild b/sci-mathematics/prover9/prover9-2009.11a-r2.ebuild
index 63b9fad1839f..e33ec50b07da 100644
--- a/sci-mathematics/prover9/prover9-2009.11a-r1.ebuild
+++ b/sci-mathematics/prover9/prover9-2009.11a-r2.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2024 Gentoo Authors
+# Copyright 1999-2025 Gentoo Authors
# Distributed under the terms of the GNU General Public License v2
EAPI=8
@@ -26,6 +26,8 @@ IUSE="examples"
PATCHES=(
"${WORKDIR}/${MY_PN}-2009-11A-makefile.patch"
"${FILESDIR}/${MY_PN}-2009-11A-manpages.patch"
+ "${FILESDIR}/${MY_PN}-2009-11A-c99.patch"
+ "${FILESDIR}/${MY_PN}-2009-11A-stable-ordering.patch"
)
src_prepare() {
@@ -33,16 +35,15 @@ src_prepare() {
sed -e "/^CC =/s:gcc:$(tc-getCC):g" -i */Makefile || die
- export MAKEOPTS+=" -j1 "
tc-export AR CC
}
src_compile() {
- emake CFLAGS="${CFLAGS} ${LDFLAGS}" -j1 all
+ emake CFLAGS="${CFLAGS} ${LDFLAGS}" all
}
src_test() {
- LD_LIBRARY_PATH="${S}/ladr/.libs/" emake -j1 test1 test2 test3
+ LD_LIBRARY_PATH="${S}/ladr/.libs/" emake test1 test2 test3
}
src_install() {
generated by cgit v1.2.3 (git 2.25.1) at 2025-03-04 16:19:48 +0000