sci-mathematics/z3: Bump to 4.8.11b

Signed-off-by: Michał Górny <mgorny@gentoo.org>

2 files changed, 97 insertions, 0 deletions

diff --git a/sci-mathematics/z3/Manifest b/sci-mathematics/z3/Manifest
index 2ea1e4443086..b8a5715375dc 100644
--- a/sci-mathematics/z3/Manifest
+++ b/sci-mathematics/z3/Manifest
@@ -1,2 +1,3 @@
 DIST z3-4.8.10.tar.gz 4731869 BLAKE2B 92487f71a0c8d961949dc23032d8fa3ff157fe7acc29b41d0d79326f8b59c60e19f43527cccf4e51872c0f0664598f9063876b04cc581f918aa48c37a13c4f3f SHA512 d2741d7ad3e1d5ee3fec92095b061a96a700c3327b2eb2090d4162bdcaeaebca8c072ef79c5daac1f6de3456165c2cc38e13f1045bc707779d1027b943837c5b
 DIST z3-4.8.11.tar.gz 4799940 BLAKE2B 5478f9f45f2dc8ea5d2b781e79d886e77eed5ae034498b434dae349aa76f05836d8fd3134a08b381830b57acb3896ac51337d5bbe480dcce4770f2cd4fbee841 SHA512 ceab703d0413d0135e0f4e6c3ba2bb58d6a4823385edb0bf7ecc96949a3073b687d415a2674c86c9f876adb52823f98f9fbbc107d799ed756dc16292f9864894
+DIST z3-4.8.11b.tar.gz 4801435 BLAKE2B 903a04246fe4dedc96fda653fa9e3a57a80b951d20b992306bd07bc778cf0a94cf36fe4ed3f178bb26196a1ca294834c784a117fe906d52b82f874a43869d110 SHA512 dfcfc85209dd00aa5f07de0a7e7186a33442b72b94b05c01f53350b9281551be2a2c21ad5e7814bc2c52a3329be8df578e6be8c387cbfdc3a9d3bef0611d6613
diff --git a/sci-mathematics/z3/z3-4.8.11b.ebuild b/sci-mathematics/z3/z3-4.8.11b.ebuild
new file mode 100644
index 000000000000..985b483904f9
--- /dev/null
+++ b/sci-mathematics/z3/z3-4.8.11b.ebuild
@@ -0,0 +1,96 @@
+# Copyright 1999-2021 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=7
+
+CMAKE_ECLASS=cmake
+PYTHON_COMPAT=( python3_{8..10} )
+
+inherit cmake-multilib python-single-r1 toolchain-funcs
+
+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}
+
+SLOT="0/4.8"
+LICENSE="MIT"
+KEYWORDS="~amd64 ~arm ~arm64 ~ppc ~ppc64 ~riscv ~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-doc/doxygen )"
+
+CMAKE_BUILD_TYPE=RelWithDebInfo
+
+multilib_src_configure() {
+	local mycmakeargs=(
+		-DCMAKE_INSTALL_DOCDIR="${EPREFIX}/usr/share/doc/${P}"
+		-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
+	)
+
+	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 RELEASE_NOTES
+	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
+}