7 files changed, 114 insertions, 5 deletions
diff --git a/sci-mathematics/Manifest.gz b/sci-mathematics/Manifest.gz
index 08dd00a25a4b..c057328f300d 100644
--- a/sci-mathematics/Manifest.gz
+++ b/sci-mathematics/Manifest.gz
diff --git a/sci-mathematics/cadical/Manifest b/sci-mathematics/cadical/Manifest
index ef1b6ae5df21..e0428a9c14b0 100644
--- a/sci-mathematics/cadical/Manifest
+++ b/sci-mathematics/cadical/Manifest
@@ -4,5 +4,5 @@ AUX cadical-makefile.in-ar.patch 323 BLAKE2B 226618745824824d8d7ccea53a3435abed9
 DIST cadical-1.9.5.tar.gz 691268 BLAKE2B 68c7fcc35ef0ad5082d5bbc828363ee45c2e637f281f1829ffb34047fff73775d34615e0ac37b8b49ff20b941db85b72c0dd6de0ab5ec5a690fd80fb5489b212 SHA512 b40727847ba0217f8d24e5468874264065c5ec9cbf0600d2e2395b8396a9d5f892127018ab9d1b930599a16a0817de5b0d29136c5dc74f2a72fb0f726e825271
 DIST cadical-2.0.0.tar.gz 709136 BLAKE2B 76b738aef8063b96b11098be132bd9921cc6e4f39efe4c14916e1b9fb9517f464771a8f4fcc116a1a37fcd44b71513bb94516b3c81699f4d5417dde0e69ddb0c SHA512 5ec4d43751e36844afcfc9102e71a2fc1e5b1112506eb654e3aef7f2ba425738264b73b88b0400ec15222c8a9d2f4d37a1f60da69a0c061303904b7ad0a93885
 EBUILD cadical-1.9.5.ebuild 923 BLAKE2B 654e146a46b3ab80d4f718bab69f5c930146f15dfeb9bcf47ec5d59e64b422064443e2ec964a8077e9818c12cae0412324f43ca8f97c0c81ff1164af529a7280 SHA512 694c7c5ab8c8b69ad9bd0d962382377900658e2da4f53563c3ffb52ec1dd2ad24ce1676f33a58bae4136a41ebb5f0a4306b2dfe3a3c9756765a11f86fd2220ea
-EBUILD cadical-2.0.0.ebuild 978 BLAKE2B 9c9846b75db3e01737ef024a276b4960f304f5feaf9e6bd14cd03c3d378ce93dcae164e046175af42eace5baddaaa69f60716b302dfc93cf7ef725ed234773cf SHA512 565058dbd8dac6b62071b581fbc95ec579df9c399e579d428786b80ea58a0b71308e366ea69cf4e305b89cba4ad10d1726863aaab374d5d2342de37512bfcd0f
+EBUILD cadical-2.0.0.ebuild 977 BLAKE2B 0f2dc4ae201edcb5fc7102ede4c37eb62d5438478017a3429a466979f57147f5e5b9a454778f94078a2aa525eb143e8abb9abb1cd32a341a5e2fb3a832cfba43 SHA512 c554c37d8176a43e789c6676f913ad60493a3299c4dc25f74b09e763bb9b4d1ed48fd53bee160bb28485b5f6c7547dc4ebab9333c5b282a1592c99d6e10d9d07
 MISC metadata.xml 613 BLAKE2B 6d7e0c1b5eae3803aa0981b195457cdcc6d2ffa2af655837e615da6ed6914ac5bec7a831ced6703ff67476561cf67139ea5519d98cdc2bd8d5781108496046e2 SHA512 b04ad6ae6e2626cea18049e3e20eb227b5580853b8ad77179ea693ed61f12d042b7ea505eb8cfafaa0121564ab0a4b6c7dcdf84f78fa2f47c465e6f61fb1a3f0
diff --git a/sci-mathematics/cadical/cadical-2.0.0.ebuild b/sci-mathematics/cadical/cadical-2.0.0.ebuild
index 0d4bf08a816c..3b7621fcdf1e 100644
--- a/sci-mathematics/cadical/cadical-2.0.0.ebuild
+++ b/sci-mathematics/cadical/cadical-2.0.0.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
@@ -18,7 +18,7 @@ else
 		-> ${P}.tar.gz"
 	S="${WORKDIR}/${PN}-rel-${PV}"
 
-	KEYWORDS="~amd64 ~x86"
+	KEYWORDS="amd64 ~x86"
 fi
 
 LICENSE="MIT"
diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index b8168fc8a953..91688109ddd1 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -4,5 +4,5 @@ AUX lean-CMakeLists-fix_flags.patch 1285 BLAKE2B 0507e553c1acf2a53c5267932127117
 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
-EBUILD lean-4.14.0-r1.ebuild 1797 BLAKE2B 592a520a4ee85bdea58e0da5294eb68b0d13ca7d5d32d70a4003294a2e944f50fa7b3648da47a36f81fe32f5cc399ca9ed7dc77c0704de543512c65cc1084c14 SHA512 86c446e89816ddf89c4ebfbb8b8dc49004dcb954f726aac35f606f10f76769fbab56e09b41bbc463ccfd14ba6494ebaaecd9d8d0f8b0073a3c6363147d598259
+EBUILD lean-4.14.0-r1.ebuild 1796 BLAKE2B 9173650dcdf5204151592d87e5a3615f2d9c947943c2e5069766487076bfa0ce02eb80a631f13760f2daa3b37ec8143fb52e887a04915851bf4c87a43d1ef1b6 SHA512 9d9577a95160ec2a12399d9790c8a4f130e2f9cd3aa2b6d364cc77924a94639b202637f64959d59cc967a651b5d6f68a293dca6413dd69e924b786b8f4ca9bdf
 MISC metadata.xml 954 BLAKE2B 338f64bbe848dca10f77fb7d5b7503684d36742139a4fd45f7a4c48250a11af6a78e40f5304d44166ce56f7fe4d22c6f980b55cab411bb7be93cc279694e9b66 SHA512 ec7c25a75237d2d54704e2d7b1811489a95780885c748a832643760d012eaceaeb5bfec9fc80509d5699940e749e770e841880cca1361848244b5031636e48b2
diff --git a/sci-mathematics/lean/lean-4.14.0-r1.ebuild b/sci-mathematics/lean/lean-4.14.0-r1.ebuild
index 153bf8d286fb..bbb780629319 100644
--- a/sci-mathematics/lean/lean-4.14.0-r1.ebuild
+++ b/sci-mathematics/lean/lean-4.14.0-r1.ebuild
@@ -23,7 +23,7 @@ else
 		-> ${P}.tar.gz"
 	S="${WORKDIR}/${PN}${MAJOR}-${PV/_/-}"
 
-	KEYWORDS="~amd64"
+	KEYWORDS="amd64"
 fi
 
 LICENSE="Apache-2.0"
diff --git a/sci-mathematics/z3/Manifest b/sci-mathematics/z3/Manifest
index 21d40d1ab1a1..2c212476e25c 100644
--- a/sci-mathematics/z3/Manifest
+++ b/sci-mathematics/z3/Manifest
@@ -1,3 +1,5 @@
 DIST z3-4.13.4.tar.gz 5766645 BLAKE2B 99e22754a7b7333868b713d78677de5d8c8ed7fdf15f0a60c224cca49bd89022e80dee86aa23f96cb7ec052ef1286ec6e2d025a6e336001d4c0d09cfce50ac55 SHA512 fd554122f3bb65e5d6622e2e331546d24892dfd3e5310bc4e041bd1c61fecfe53dbb487e4b125d87367338cacc9e06f28c71f380aac5fe8a74f4b45aaa27b6ce
+DIST z3-4.14.0.tar.gz 5841848 BLAKE2B fc56ab4538a8fa07fd7ea34fdd403a13941f93fee500e90686cfc827b5094d83662ad02fda0c9ff146cb425603a3d65aadc1c006d26dd40c8cbd91462381670a SHA512 5a3de3207b5c05f77f8369d7fdbb9e13a7db850f8c3edaa8f2adfcf58b186d34409e4a56d44646f853027850941135be5042e67a53ddf3302dc3b645c1ab3db4
 EBUILD z3-4.13.4.ebuild 2606 BLAKE2B 4d1558de478d4cde52c6202ce2dabb22645a71cee0782daf78bf36ca879b8bd539f9a95a9cbbfa9b7a0b0b08d780239bba50b5eb83c876071d5a993fb30c599b SHA512 210add2e050e469860ced42ddd316061646fcc8e9cba78cfc1ef0b6c9ad4ca9cc82ecee73a291c0fa290ed879b5b09c81b3b61afaf90dd2431700d8a7944a337
+EBUILD z3-4.14.0.ebuild 2612 BLAKE2B 2199cfdeaa07a1dc9a22a3a07bdb77645b65632b70a520b966d74ba56beb8499b50f95b6608b48b3cea2f548186217c46fc3d9394980904b875fb01837fd4878 SHA512 88bdeb3290537b666e5453de807e466a6020f7f5dc76fb804b9b635006d1e9300980ef2405377b6b4a90152ee5720bdf68d12d092ae2272932ed2f1fe2df840b
 MISC metadata.xml 1718 BLAKE2B a94783909c12aa7dd2d5fd1f9d2fc75e20ca91b6abffd6dc020f602e57ef698f7184acaf14def4b6e21bb659e595abd44956ba37a679134d11b523103b0461df SHA512 ed375986a8010a7ae1eadab3107342126194a5513cbb22ce2064ffeff42c7184ea94f4f69017204c73bd61236847475cd1f0d8b3ba369236b26630dc8b2f46a2
diff --git a/sci-mathematics/z3/z3-4.14.0.ebuild b/sci-mathematics/z3/z3-4.14.0.ebuild
new file mode 100644
index 000000000000..759a8f720476
--- /dev/null
+++ b/sci-mathematics/z3/z3-4.14.0.ebuild
@@ -0,0 +1,107 @@
+# Copyright 1999-2025 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+PYTHON_COMPAT=( python3_{10..13} )
+
+inherit cmake-multilib java-pkg-opt-2 python-single-r1
+
+DESCRIPTION="An efficient theorem prover"
+HOMEPAGE="https://github.com/Z3Prover/z3/"
+SRC_URI="https://github.com/Z3Prover/z3/archive/${P}.tar.gz"
+S=${WORKDIR}/z3-${P}
+
+LICENSE="MIT"
+SLOT="0/$(ver_cut 1-2)"
+KEYWORDS="~amd64 ~arm ~arm64 ~loong ~mips ~ppc ~ppc64 ~riscv ~sparc ~x86"
+IUSE="doc examples gmp isabelle java python"
+REQUIRED_USE="${PYTHON_REQUIRED_USE}"
+
+RDEPEND="
+	${PYTHON_DEPS}
+	gmp? ( dev-libs/gmp:0=[cxx(+),${MULTILIB_USEDEP}] )
+"
+DEPEND="
+	${RDEPEND}
+	java? ( >=virtual/jdk-1.8 )
+"
+BDEPEND="
+	doc? ( app-text/doxygen[dot] )
+"
+
+CMAKE_BUILD_TYPE=RelWithDebInfo
+
+src_prepare() {
+	cmake_src_prepare
+	java-pkg-opt-2_src_prepare
+}
+
+multilib_src_configure() {
+	local mycmakeargs=(
+		-DCMAKE_INSTALL_DOCDIR="${EPREFIX}/usr/share/doc/${PF}"
+		-DZ3_USE_LIB_GMP=$(usex gmp)
+		-DZ3_ENABLE_EXAMPLE_TARGETS=OFF
+		-DZ3_BUILD_DOCUMENTATION=$(multilib_native_usex doc)
+		-DZ3_BUILD_PYTHON_BINDINGS=$(multilib_native_usex python)
+		-DZ3_BUILD_JAVA_BINDINGS=$(multilib_native_usex java)
+		-DZ3_INCLUDE_GIT_DESCRIBE=OFF
+		-DZ3_INCLUDE_GIT_HASH=OFF
+	)
+
+	multilib_is_native_abi && use java && mycmakeargs+=( -DJAVA_HOME="$(java-config -g JAVA_HOME )" )
+
+	cmake_src_configure
+}
+
+multilib_src_test() {
+	cmake_build test-z3
+	set -- "${BUILD_DIR}"/test-z3 /a
+	echo "${@}" >&2
+	"${@}" || die
+}
+
+multilib_src_install_all() {
+	dodoc README.md
+	use examples && dodoc -r examples
+	use python && python_optimize
+
+	if use isabelle; then
+		insinto /usr/share/Isabelle/contrib/${P}/etc
+		newins - settings <<-EOF
+			Z3_COMPONENT="\$COMPONENT"
+			Z3_HOME="${EPREFIX}/usr/bin"
+			Z3_SOLVER="${EPREFIX}/usr/bin/z3"
+			Z3_REMOTE_SOLVER="z3"
+			Z3_VERSION="${PV}"
+			Z3_INSTALLED="yes"
+			Z3_NON_COMMERCIAL="yes"
+		EOF
+	fi
+}
+
+pkg_postinst() {
+	if use isabelle; then
+		if [[ -f ${ROOT}/etc/isabelle/components ]]; then
+			sed -e "/contrib\/${PN}-[0-9.]*/d" \
+				-i "${ROOT}/etc/isabelle/components" || die
+			cat <<-EOF >> "${ROOT}/etc/isabelle/components" || die
+				contrib/${P}
+			EOF
+		fi
+	fi
+}
+
+pkg_postrm() {
+	if use isabelle; then
+		if [[ ! ${REPLACING_VERSIONS} ]]; then
+			if [[ -f "${ROOT}/etc/isabelle/components" ]]; then
+				# Note: this sed should only match the version of this ebuild
+				# Which is what we want as we do not want to remove the line
+				# of a new Isabelle component being installed during an upgrade.
+				sed -e "/contrib\/${P}/d" \
+					-i "${ROOT}/etc/isabelle/components" || die
+			fi
+		fi
+	fi
+}