From 95ce69d324747e9aa715e1761abab42204529b28 Mon Sep 17 00:00:00 2001 From: V3n3RiX Date: Tue, 1 Oct 2024 01:26:02 +0100 Subject: gentoo auto-resync : 01:10:2024 - 01:26:02 --- sci-mathematics/Manifest.gz | Bin 19344 -> 19340 bytes sci-mathematics/boolector/Manifest | 2 + sci-mathematics/boolector/boolector-3.2.4.ebuild | 86 +++++++++++++++++++++++ sci-mathematics/coq/Manifest | 2 +- sci-mathematics/coq/coq-8.19.2.ebuild | 2 +- sci-mathematics/vampire/Manifest | 2 + sci-mathematics/vampire/vampire-4.9.ebuild | 63 +++++++++++++++++ 7 files changed, 155 insertions(+), 2 deletions(-) create mode 100644 sci-mathematics/boolector/boolector-3.2.4.ebuild create mode 100644 sci-mathematics/vampire/vampire-4.9.ebuild (limited to 'sci-mathematics') diff --git a/sci-mathematics/Manifest.gz b/sci-mathematics/Manifest.gz index afc93632f807..7885c0128237 100644 Binary files a/sci-mathematics/Manifest.gz and b/sci-mathematics/Manifest.gz differ 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 +} -- cgit v1.2.3