summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMaciej Barć <xgqt@gentoo.org>2024-09-30 19:47:18 +0200
committerMaciej Barć <xgqt@gentoo.org>2024-09-30 20:22:53 +0200
commitea3edb5ee8118107e5cd048b9708c08cb5560027 (patch)
tree64757b3016f78e87368d561f9ee5a82b68cb5c12 /sci-mathematics
parentdev-build/bazelisk: bump to 1.22.0 (diff)
downloadgentoo-ea3edb5ee8118107e5cd048b9708c08cb5560027.tar.gz
gentoo-ea3edb5ee8118107e5cd048b9708c08cb5560027.tar.bz2
gentoo-ea3edb5ee8118107e5cd048b9708c08cb5560027.zip
sci-mathematics/vampire: bump to 4.9
Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Diffstat (limited to 'sci-mathematics')
-rw-r--r--sci-mathematics/vampire/Manifest1
-rw-r--r--sci-mathematics/vampire/vampire-4.9.ebuild63
2 files changed, 64 insertions, 0 deletions
diff --git a/sci-mathematics/vampire/Manifest b/sci-mathematics/vampire/Manifest
index 34007ddf898b..502fd0cb9da9 100644
--- a/sci-mathematics/vampire/Manifest
+++ b/sci-mathematics/vampire/Manifest
@@ -1 +1,2 @@
DIST vampire-4.8-casc2023.tar.gz 1527236 BLAKE2B fb6ce26bb31996529e2b4d76173a1cb8d2c796aa6a5a2581515c516b5f07e9d4efc6040db1ac7f65388d723ee5080d62fb9c2b6ec88f58babd892fd96c0bf0ba SHA512 d6349ab23a289101a0d9f3caa5190df065dfbbe4e2e999e7d5b97ff738c8355b35848d93423ec3a0b0f88d4ac806173493f9a2de4e31945bb09c500c64eb5028
+DIST vampire-4.9-casc2023.tar.gz 1502934 BLAKE2B 399ca20578d30e6cca74e7e46a97d87975ebcc9cd18e61fc125b99eec008a46df7e12b8e3c5e448f1e112429a8f79d7d7b9866811d2cce1c523bd0fb322278c4 SHA512 f37ca777da8dad719e3072d6c0ff31b67152ed699a1f21ccb5f004398d6472ab8105f16bfd21ec8a42cf65f8aca4a197e9c4557724e2d1a38bed291b2c5aeef3
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
+}