From d4653056cc74d97f24bef0d56b4ebe11c53c8b76 Mon Sep 17 00:00:00 2001 From: V3n3RiX Date: Mon, 24 Feb 2025 19:24:56 +0000 Subject: gentoo auto-resync : 24:02:2025 - 19:24:56 --- sci-mathematics/prover9/Manifest | 4 +- .../prover9/files/LADR-2009-11A-c99.patch | 25 +++++ .../files/LADR-2009-11A-stable-ordering.patch | 91 +++++++++++++++ sci-mathematics/prover9/prover9-2009.11a-r1.ebuild | 124 -------------------- sci-mathematics/prover9/prover9-2009.11a-r2.ebuild | 125 +++++++++++++++++++++ 5 files changed, 244 insertions(+), 125 deletions(-) create mode 100644 sci-mathematics/prover9/files/LADR-2009-11A-c99.patch create mode 100644 sci-mathematics/prover9/files/LADR-2009-11A-stable-ordering.patch delete mode 100644 sci-mathematics/prover9/prover9-2009.11a-r1.ebuild create mode 100644 sci-mathematics/prover9/prover9-2009.11a-r2.ebuild (limited to 'sci-mathematics/prover9') 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-r1.ebuild deleted file mode 100644 index 63b9fad1839f..000000000000 --- a/sci-mathematics/prover9/prover9-2009.11a-r1.ebuild +++ /dev/null @@ -1,124 +0,0 @@ -# Copyright 1999-2024 Gentoo Authors -# Distributed under the terms of the GNU General Public License v2 - -EAPI=8 - -inherit toolchain-funcs - -MY_PN="LADR" -typeset -u MY_PV -MY_PV="$(ver_rs 1 '-')" -MY_P="${MY_PN}-${MY_PV}" - -DESCRIPTION="Automated theorem prover for first-order and equational logic" -HOMEPAGE="https://www.cs.unm.edu/~mccune/mace4/" -SRC_URI=" - https://www.cs.unm.edu/~mccune/mace4/download/${MY_P}.tar.gz - https://dev.gentoo.org/~jlec/distfiles/${MY_PN}-2009-11A-makefile.patch.xz -" -S="${WORKDIR}/${MY_P}/" - -LICENSE="GPL-2" -SLOT="0" -KEYWORDS="~amd64 ~x86" -IUSE="examples" - -PATCHES=( - "${WORKDIR}/${MY_PN}-2009-11A-makefile.patch" - "${FILESDIR}/${MY_PN}-2009-11A-manpages.patch" -) - -src_prepare() { - default - - 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 -} - -src_test() { - LD_LIBRARY_PATH="${S}/ladr/.libs/" emake -j1 test1 test2 test3 -} - -src_install() { - dobin \ - bin/attack \ - bin/autosketches4 \ - bin/clausefilter \ - bin/clausetester \ - bin/complex \ - bin/directproof \ - bin/dprofiles \ - bin/fof-prover9 \ - bin/gen_trc_defs \ - bin/get_givens \ - bin/get_interps \ - bin/get_kept \ - bin/gvizify \ - bin/idfilter \ - bin/interpfilter \ - bin/interpformat \ - bin/isofilter \ - bin/isofilter0 \ - bin/isofilter2 \ - bin/ladr_to_tptp \ - bin/latfilter \ - bin/looper \ - bin/mace4 \ - bin/miniscope \ - bin/mirror-flip \ - bin/newauto \ - bin/newsax \ - bin/olfilter \ - bin/perm3 \ - bin/proof3fo.xsl \ - bin/prooftrans \ - bin/prover9 \ - bin/renamer \ - bin/rewriter \ - bin/sigtest \ - bin/test_clause_eval \ - bin/test_complex \ - bin/tptp_to_ladr \ - bin/unfast \ - bin/upper-covers - - doman \ - manpages/interpformat.1 \ - manpages/isofilter.1 \ - manpages/prooftrans.1 \ - manpages/mace4.1 \ - manpages/prover9.1 \ - manpages/clausefilter.1 \ - manpages/clausetester.1 \ - manpages/interpfilter.1 \ - manpages/rewriter.1 \ - manpages/prover9-apps.1 - - docinto html - dodoc -r ladr/index.html.master ladr/html/* - - insinto "/usr/$(get_libdir)" - dolib.so ladr/.libs/libladr.so.4.0.0 - - dosym libladr.so.4.0.0 "/usr/$(get_libdir)/libladr.so.4" - dosym libladr.so.4.0.0 "/usr/$(get_libdir)/libladr.so" - - insinto /usr/include/ladr - doins ladr/*.h - - if use examples ; then - insinto "/usr/share/${PN}/examples" - doins prover9.examples/* - - # The prover9-mace4 script is installed as an example script - # to avoid confusion with the GUI sci-mathematics/p9m4 prover9mace4.py - insinto "/usr/share/${PN}/scripts" - doins bin/prover9-mace4 - fi -} diff --git a/sci-mathematics/prover9/prover9-2009.11a-r2.ebuild b/sci-mathematics/prover9/prover9-2009.11a-r2.ebuild new file mode 100644 index 000000000000..e33ec50b07da --- /dev/null +++ b/sci-mathematics/prover9/prover9-2009.11a-r2.ebuild @@ -0,0 +1,125 @@ +# Copyright 1999-2025 Gentoo Authors +# Distributed under the terms of the GNU General Public License v2 + +EAPI=8 + +inherit toolchain-funcs + +MY_PN="LADR" +typeset -u MY_PV +MY_PV="$(ver_rs 1 '-')" +MY_P="${MY_PN}-${MY_PV}" + +DESCRIPTION="Automated theorem prover for first-order and equational logic" +HOMEPAGE="https://www.cs.unm.edu/~mccune/mace4/" +SRC_URI=" + https://www.cs.unm.edu/~mccune/mace4/download/${MY_P}.tar.gz + https://dev.gentoo.org/~jlec/distfiles/${MY_PN}-2009-11A-makefile.patch.xz +" +S="${WORKDIR}/${MY_P}/" + +LICENSE="GPL-2" +SLOT="0" +KEYWORDS="~amd64 ~x86" +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() { + default + + sed -e "/^CC =/s:gcc:$(tc-getCC):g" -i */Makefile || die + + tc-export AR CC +} + +src_compile() { + emake CFLAGS="${CFLAGS} ${LDFLAGS}" all +} + +src_test() { + LD_LIBRARY_PATH="${S}/ladr/.libs/" emake test1 test2 test3 +} + +src_install() { + dobin \ + bin/attack \ + bin/autosketches4 \ + bin/clausefilter \ + bin/clausetester \ + bin/complex \ + bin/directproof \ + bin/dprofiles \ + bin/fof-prover9 \ + bin/gen_trc_defs \ + bin/get_givens \ + bin/get_interps \ + bin/get_kept \ + bin/gvizify \ + bin/idfilter \ + bin/interpfilter \ + bin/interpformat \ + bin/isofilter \ + bin/isofilter0 \ + bin/isofilter2 \ + bin/ladr_to_tptp \ + bin/latfilter \ + bin/looper \ + bin/mace4 \ + bin/miniscope \ + bin/mirror-flip \ + bin/newauto \ + bin/newsax \ + bin/olfilter \ + bin/perm3 \ + bin/proof3fo.xsl \ + bin/prooftrans \ + bin/prover9 \ + bin/renamer \ + bin/rewriter \ + bin/sigtest \ + bin/test_clause_eval \ + bin/test_complex \ + bin/tptp_to_ladr \ + bin/unfast \ + bin/upper-covers + + doman \ + manpages/interpformat.1 \ + manpages/isofilter.1 \ + manpages/prooftrans.1 \ + manpages/mace4.1 \ + manpages/prover9.1 \ + manpages/clausefilter.1 \ + manpages/clausetester.1 \ + manpages/interpfilter.1 \ + manpages/rewriter.1 \ + manpages/prover9-apps.1 + + docinto html + dodoc -r ladr/index.html.master ladr/html/* + + insinto "/usr/$(get_libdir)" + dolib.so ladr/.libs/libladr.so.4.0.0 + + dosym libladr.so.4.0.0 "/usr/$(get_libdir)/libladr.so.4" + dosym libladr.so.4.0.0 "/usr/$(get_libdir)/libladr.so" + + insinto /usr/include/ladr + doins ladr/*.h + + if use examples ; then + insinto "/usr/share/${PN}/examples" + doins prover9.examples/* + + # The prover9-mace4 script is installed as an example script + # to avoid confusion with the GUI sci-mathematics/p9m4 prover9mace4.py + insinto "/usr/share/${PN}/scripts" + doins bin/prover9-mace4 + fi +} -- cgit v1.2.3