gentoo auto-resync : 01:10:2024 - 01:26:02

7 files changed, 155 insertions, 2 deletions

diff --git a/sci-mathematics/Manifest.gz b/sci-mathematics/Manifest.gz
index afc93632f807..7885c0128237 100644
--- a/sci-mathematics/Manifest.gz
+++ b/sci-mathematics/Manifest.gz
diff --git a/sci-mathematics/boolector/Manifest b/sci-mathematics/boolector/Manifest
index 95ae96a2b6dc..35495146d492 100644
--- a/sci-mathematics/boolector/Manifest
+++ b/sci-mathematics/boolector/Manifest
@@ -1,4 +1,6 @@
 AUX boolector-3.2.3-cmake-std.patch 350 BLAKE2B bcdc394f1f1c9ef17605f0c12c2279d7842a4c106d70132760ed7c3fe215d41ba25551ae18e9d29f5697fb2c7546cef96b3a1c3ebb5b79da6c6ed4ada98d1dbb SHA512 6345feda413d4959cd95af0708f522d3569bea66ceab524b6f2378e473f1a64417b5fbcfbd865c10c14c0dfb0cd11c585db6ffa7c79d930b90aaf47693d47aa8
 DIST boolector-3.2.3.tar.gz 1566566 BLAKE2B 1c9adb1272c2289af6afce0149b11ce36a42aef47f1b3353f5f9dbaf12287718f29e45415b82b723bd37fb0438517c48d64a12f0c038105edeb6036f49189ac7 SHA512 a85c10edf05455e2911614f9d8f2b214a136470852b31a631c96247416dab822efcc6d9047f3a85c85aff499e8eb62fb36e52f2633511c5b42d287c4962c4239
+DIST boolector-3.2.4.tar.gz 1567983 BLAKE2B c74e6b7be2931ae164b3cde5ff3c9b60b12ad49b4be23ddb2931f5a71ffbfb5bb98a29ea46780275414bbe2e3e65b6108e489254251f8fd820a89162dc6eaae5 SHA512 57ba34264abd1d4350403b45995b040bd792dbea7d07a1c64d067ddbddeb3944d8515ce667ae4ffef70d35b5be68cfc5938acd6a8a7b242a09f218474024b821
 EBUILD boolector-3.2.3.ebuild 1899 BLAKE2B 0856b67a9ce86a78b00b556d087c8d2ccfecddf25899e57da146d3698233c8edd773d8d553d77741afa3488fa8669bc042ee787e7d0a89c2b889238b4d9b0982 SHA512 642e7323639f49f97a613ed9f15ebabcd51969b0b5b75fc2530fe73cb36000b5baf7adb30a000d143de14d8957f78cce506d9f0bd92d50b3ff4da4a401b08839
+EBUILD boolector-3.2.4.ebuild 1899 BLAKE2B 4b5db04d6c7739096eea5baa44040a68e9b1d9c74da3fb273fe4277956c63e7d5da66b379452101636f6afb3b05bdc7563ed08ee5251dab689a3cbc245abca4e SHA512 a9feb0a9f0c2c731dd04710d1c8ab9567463a66cea089b3c2e984fe73c805c65a8852b952aa7b653ff6d53519f97d95ae0d5652bc8c69e6ee657bbe034276805
 MISC metadata.xml 1245 BLAKE2B a04e1e5a6af857100b8b569f57f4d2610593e9eb741513e4e6405a8fa9828471b92aaa1ad57a3163dc2f251b5664493692f92477b7191621ff8fd76eed9f57e7 SHA512 81257f7be3b21bf10caad654d5747ef2d978c0df5a05049b890420e2d170b7a4fa06151da0604a8b1b6e7daf2fb01344003c9243205a94b4040c580beb414836
diff --git a/sci-mathematics/boolector/boolector-3.2.4.ebuild b/sci-mathematics/boolector/boolector-3.2.4.ebuild
new file mode 100644
index 000000000000..2a1d832b43c3
--- /dev/null
+++ b/sci-mathematics/boolector/boolector-3.2.4.ebuild
@@ -0,0 +1,86 @@
+# Copyright 1999-2024 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+PYTHON_COMPAT=( python3_{10..13} )
+
+inherit python-single-r1 cmake
+
+DESCRIPTION="Fast SMT solver for bit-vectors, arrays and uninterpreted functions"
+HOMEPAGE="https://boolector.github.io/
+	https://github.com/Boolector/boolector/"
+
+if [[ "${PV}" == *9999* ]] ; then
+	inherit git-r3
+
+	EGIT_REPO_URI="https://github.com/Boolector/${PN}.git"
+else
+	SRC_URI="https://github.com/Boolector/${PN}/archive/${PV}.tar.gz
+		-> ${P}.tar.gz"
+
+	KEYWORDS="~amd64 ~x86"
+fi
+
+LICENSE="MIT"
+SLOT="0"
+IUSE="cryptominisat examples +gmp minisat +picosat python test"
+REQUIRED_USE="
+	python? ( ${PYTHON_REQUIRED_USE} )
+	|| ( cryptominisat minisat picosat )
+"
+RESTRICT="!test? ( test )"
+
+RDEPEND="
+	sci-mathematics/btor2tools:=
+	cryptominisat? ( sci-mathematics/cryptominisat:= )
+	gmp? ( dev-libs/gmp:= )
+	minisat? ( sci-mathematics/minisat:= )
+	picosat? ( sci-mathematics/picosat:= )
+	python? ( ${PYTHON_DEPS} )
+"
+DEPEND="
+	${RDEPEND}
+"
+BDEPEND="
+	test? ( dev-cpp/gtest )
+"
+
+PATCHES=( "${FILESDIR}/${PN}-3.2.3-cmake-std.patch" )
+
+pkg_setup() {
+	use python && python-single-r1_pkg_setup
+}
+
+src_configure() {
+	local -a mycmakeargs=(
+		-DBUILD_SHARED_LIBS=ON
+		-DBtor2Tools_LIBRARIES=/usr/$(get_libdir)/libbtor2parser.so
+		-DUSE_PYTHON2=OFF
+		-DPYTHON=$(usex python)
+		-DTESTING=$(usex test)
+		-DUSE_GMP=$(usex gmp)
+		-DUSE_PYTHON3=$(usex python)
+
+		# Integration with other SMT solvers
+		-DUSE_LINGELING=OFF  # Not packaged yet.
+		-DUSE_CADICAL=OFF  # Fails to link.
+		-DUSE_CMS=$(usex cryptominisat)
+		-DUSE_MINISAT=$(usex minisat)
+		-DUSE_PICOSAT=$(usex picosat)
+	)
+	cmake_src_configure
+}
+
+src_install() {
+	cmake_src_install
+
+	if use examples ; then
+		dodoc -r examples
+	fi
+
+	if [[ "$(get_libdir)" != lib ]] ; then
+		dodir "/usr/$(get_libdir)"
+		mv "${ED}/usr/lib"/*.so "${ED}/usr/$(get_libdir)/" || die
+	fi
+}
diff --git a/sci-mathematics/coq/Manifest b/sci-mathematics/coq/Manifest
index c46153b0b628..f655d2918323 100644
--- a/sci-mathematics/coq/Manifest
+++ b/sci-mathematics/coq/Manifest
@@ -4,6 +4,6 @@ DIST coq-8.19.2.tar.gz 7678311 BLAKE2B 5f9617fbe0127b0c8357c63f331ba3e9fb5a931be
 DIST coq-8.20.0.tar.gz 7839432 BLAKE2B 9b489db0cc6874b0a629f3bdb4b503201005ec95a3375441538cd7e51d371a39561b9d0ab23ac485652782fdc7ae8d90c97ca1ff4d9a85fb8727a39ed4a6f48c SHA512 1a7eac6e2f58724a3f9d68bbb321e4cfe963ba1a5551b9b011db4b3f559c79be433d810ff262593d753770ee41ea68fbd6a60daa1e2319ea00dff64c8851d70b
 EBUILD coq-8.19.0.ebuild 2491 BLAKE2B ee610273d5294b25e7aa48cfb048b99af86aef21fb8d3c21019da509c82912b4f6624ae5076a694d98eb3679e9eba7ef138cb12a8ba0f938ce7ecbe4aacf6027 SHA512 498a461e9bc69016aab3abc5578bbd2367322dc14f8c2db9293a246022a4d8065dd06966741db3ae45365b3c1049703f85a9cef42416a8be3ed469dc4d80233e
 EBUILD coq-8.19.1.ebuild 2492 BLAKE2B 1c1d296a61f57bf8e5120aa8e70dce382548cc55a8c1365c1e85b33080e3fd346ea1b904e9440af465c67416b83f4b4e538ec558ce0b8c10ec42a94efee7e0f8 SHA512 9783ef6098d6028dd207a239796916ed90d8eab01429c4fded5e25f0a1c776f1c9dc0bac9f15e4d0847ad5d915bb69760937347cb6f295806f61af95cec2199b
-EBUILD coq-8.19.2.ebuild 2484 BLAKE2B 54de05ac84bb2df76e6defa2f96014d3488a78129a6e1b480857ea04ccf1ca1d0c96deacbe544aec0dfffd53c51fc490bef2c9d22c64fdbe7cddd99833f63f75 SHA512 5a236fd48123fd32fe3f13ce964f0effca8ab3ef8a27d025c75bcdd10d7afd511cd506347eb889c59b3ac3fbe8838d6a3757f4c0fa82c277d6669cb926a2bdc4
+EBUILD coq-8.19.2.ebuild 2483 BLAKE2B ce2870e40fe70f113cb52eea1a7b5771bee4180d0a58e4bfb539feb0c499531b2dc1388066f33bb7024d77c5efc8541d3e545e86568e58cec12c48eaa9f8360d SHA512 49605fd89331d80ac24bd886f1b96ffbf9ad17c0ffec3dfe2ac0bda2176853f10e023708a02ccffbcda2c0f2a9443e921a44e2745446ac13181aada4c5aebb97
 EBUILD coq-8.20.0.ebuild 2896 BLAKE2B 0b241fec6dd165b83fa07c0708b03461ceebbf800fd6501936c8c36e7c9a0f42c6c01594c1ee48903b535dbd65a2fc389bd4bdb66e98ffe926a78fe302e4acec SHA512 5d4d0a01cf012f142cb341d63c2c19ea05be45c2605ca2a2ebe92a9773703d046927318371afc5804187546e0a60daa225b20df05428f721dd04e964a4dc1378
 MISC metadata.xml 1047 BLAKE2B 9f6defdf213139ee6549bc8f3b36ce5e8f53ea73bd5aad9262932cbaea7e90bd97c9ffc9dbbd03ac50097c5a6f19f5ddf00dd2b74cc6a5349faf1b597244fb67 SHA512 0f5bfbdd9ffd6f64379e697ed7cf90c2d9257cd1815e520aa14235f1cb399d20fc863221a0cae803cc88e5975be964b9debc3d750a6378ea157146f2e567c5dc
diff --git a/sci-mathematics/coq/coq-8.19.2.ebuild b/sci-mathematics/coq/coq-8.19.2.ebuild
index f61b2d0f54da..4be3a3484836 100644
--- a/sci-mathematics/coq/coq-8.19.2.ebuild
+++ b/sci-mathematics/coq/coq-8.19.2.ebuild
@@ -17,7 +17,7 @@ S="${WORKDIR}/${MY_P}"
 
 LICENSE="LGPL-2.1"
 SLOT="0/${PV}"
-KEYWORDS="~amd64 ~x86"
+KEYWORDS="amd64 ~x86"
 IUSE="debug doc gui +ocamlopt test"
 
 # TODO: Lots of failing tests. Maybe investigate later.
diff --git a/sci-mathematics/vampire/Manifest b/sci-mathematics/vampire/Manifest
index 98e6460d38b6..8dcef7cb9ae7 100644
--- a/sci-mathematics/vampire/Manifest
+++ b/sci-mathematics/vampire/Manifest
@@ -1,3 +1,5 @@
 DIST vampire-4.8-casc2023.tar.gz 1527236 BLAKE2B fb6ce26bb31996529e2b4d76173a1cb8d2c796aa6a5a2581515c516b5f07e9d4efc6040db1ac7f65388d723ee5080d62fb9c2b6ec88f58babd892fd96c0bf0ba SHA512 d6349ab23a289101a0d9f3caa5190df065dfbbe4e2e999e7d5b97ff738c8355b35848d93423ec3a0b0f88d4ac806173493f9a2de4e31945bb09c500c64eb5028
+DIST vampire-4.9-casc2023.tar.gz 1502934 BLAKE2B 399ca20578d30e6cca74e7e46a97d87975ebcc9cd18e61fc125b99eec008a46df7e12b8e3c5e448f1e112429a8f79d7d7b9866811d2cce1c523bd0fb322278c4 SHA512 f37ca777da8dad719e3072d6c0ff31b67152ed699a1f21ccb5f004398d6472ab8105f16bfd21ec8a42cf65f8aca4a197e9c4557724e2d1a38bed291b2c5aeef3
 EBUILD vampire-4.8.ebuild 1424 BLAKE2B 024de9192ad510aff6d79b79bbd41593ae5916efb012cae57df3425202dc9b4e971316d8774160c33ce81a3c1704d3bf2e6f647cd46be449c0266693d6397bb2 SHA512 c1a15a86f129361758303d0b834542b0cd6405574a2a7a611821bcade52929f06aef0f43fec1af5a3b0320651c8e06a51d4ff2e527a6b90eb1b0fa6559034eda
+EBUILD vampire-4.9.ebuild 1431 BLAKE2B 342fe7b4a0d5a82d3f433ad028fd8547252a82dc76e75ea823c7f3ac19128807124fbf17e023c96312e634f98504f516f21e90391251c0e79abfdb525d61c76b SHA512 37224e74ae2769e0e3f24b040e4fb8270577b8855df1a29e8781dfffa13411b3e594b80576aebc2647ba1a09466cbfc4f850df4d3b7d38e52040b178196ddda6
 MISC metadata.xml 1020 BLAKE2B 6e798243e207d09fac240c73cda8918b300706a19d53918b3ce78e847146ad3676a39d9be8e020b678c20d7fe02da0eab57519ea2c5841eeeea0b8a680045928 SHA512 dc82a586070c97db278ef17a24384436548b2a968d18ead7d148f654bab4ad846e685ac2ae2f7db8048b25115b673bcf8223fa2813b370f9d6b6ac01dcf9040e
diff --git a/sci-mathematics/vampire/vampire-4.9.ebuild b/sci-mathematics/vampire/vampire-4.9.ebuild
new file mode 100644
index 000000000000..523053c44f97
--- /dev/null
+++ b/sci-mathematics/vampire/vampire-4.9.ebuild
@@ -0,0 +1,63 @@
+# Copyright 1999-2024 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+inherit flag-o-matic cmake
+
+DESCRIPTION="The Vampire Prover, theorem prover for first-order logic"
+HOMEPAGE="https://vprover.github.io/
+	https://github.com/vprover/vampire/"
+
+if [[ ${PV} == *9999* ]] ; then
+	inherit git-r3
+	EGIT_REPO_URI="https://github.com/vprover/${PN}.git"
+	EGIT_SUBMODULES=()
+else
+	# v4.9casc2024 - "This is the 4.9 version submitted to CASC in 2024."
+	SRC_URI="https://github.com/vprover/${PN}/archive/v${PV}casc2024.tar.gz
+		-> ${P}-casc2023.tar.gz"
+	S="${WORKDIR}/${PN}-${PV}casc2024"
+
+	KEYWORDS="~amd64 ~x86"
+fi
+
+LICENSE="BSD"
+SLOT="0/${PV}"
+IUSE="debug +z3"
+# debug mode needs to be enabled for tests
+# https://github.com/vprover/vampire/blob/8197e1d2d86a0b276b5fcb6c02d8122f66b7277e/CMakeLists.txt#L38
+RESTRICT="!debug? ( test )"
+
+RDEPEND="
+	z3? (
+		dev-libs/gmp:=
+		>=sci-mathematics/z3-4.11.2:=
+	)
+"
+DEPEND="
+	${RDEPEND}
+"
+
+src_configure() {
+	# -Werror=strict-aliasing warnings, bug #863269
+	filter-lto
+	append-flags -fno-strict-aliasing
+
+	local CMAKE_BUILD_TYPE=$(usex debug Debug Release)
+
+	local -a mycmakeargs=(
+		-DZ3_DIR=$(usex z3 "/usr/$(get_libdir)/cmake/z3/" "")
+	)
+	cmake_src_configure
+}
+
+src_install() {
+	local bin_name=$(find "${BUILD_DIR}"/bin/ -type f -name "${PN}*")
+
+	exeinto /usr/bin
+	doexe "${bin_name}"
+	dosym $(basename "${bin_name}") "/usr/bin/${PN}"
+
+	einstalldocs
+}