gentoo auto-resync : 03:11:2023 - 03:56:37

10 files changed, 134 insertions, 15 deletions

diff --git a/sci-mathematics/Manifest.gz b/sci-mathematics/Manifest.gz
index 77561a8da19e..b333828c89f1 100644
--- a/sci-mathematics/Manifest.gz
+++ b/sci-mathematics/Manifest.gz
diff --git a/sci-mathematics/boolector/Manifest b/sci-mathematics/boolector/Manifest
index c6641a13e4ad..434335e9b6a9 100644
--- a/sci-mathematics/boolector/Manifest
+++ b/sci-mathematics/boolector/Manifest
@@ -1,3 +1,6 @@
+AUX boolector-3.2.3-cmake-std.patch 350 BLAKE2B bcdc394f1f1c9ef17605f0c12c2279d7842a4c106d70132760ed7c3fe215d41ba25551ae18e9d29f5697fb2c7546cef96b3a1c3ebb5b79da6c6ed4ada98d1dbb SHA512 6345feda413d4959cd95af0708f522d3569bea66ceab524b6f2378e473f1a64417b5fbcfbd865c10c14c0dfb0cd11c585db6ffa7c79d930b90aaf47693d47aa8
 DIST boolector-3.2.2_p20220110.tar.gz 1567668 BLAKE2B 6816f0434d88c790a27b9afe4c3b63c18a55b14f9f13b092f2940309e34842fe4868bf8d378bad130c4561d25e7d79b356fc27d9422bd42ba1b74ff98be36f72 SHA512 b1b964c155c8227e631025cf6bff69cf54728b1d875c2bd44a5a1ddb2857de2ab8fefc96d194faa5f98015e730b417d46a415ea601740e890df07ad5e50ad656
+DIST boolector-3.2.3.tar.gz 1566566 BLAKE2B 1c9adb1272c2289af6afce0149b11ce36a42aef47f1b3353f5f9dbaf12287718f29e45415b82b723bd37fb0438517c48d64a12f0c038105edeb6036f49189ac7 SHA512 a85c10edf05455e2911614f9d8f2b214a136470852b31a631c96247416dab822efcc6d9047f3a85c85aff499e8eb62fb36e52f2633511c5b42d287c4962c4239
 EBUILD boolector-3.2.2_p20220110.ebuild 1900 BLAKE2B 2a99565257a782a5c198ef8661f8c51aa734ef3987213db1c4010ebe5f083a5f9f71525d66217ec32cb1edd4ef34d89bc386a1d21b91c277336493368ffdd3d7 SHA512 c588c5c8e821d6dd62c77c1f9c291761d9c8d30d415e7634a8fb64460e40a2abe9eb03e873c309218fc34e4105c6b597f7e09c77f0faa51afc10b68b9f754d46
+EBUILD boolector-3.2.3.ebuild 1853 BLAKE2B 05e5a5f5db0b4e5feb28bf988db1cce1f3e0f9c1bff7f54da15726ce866ed7aa450d73ae28ad451fa66aa933935f3bc39a49b6105ba33a88e086aa2d089691f1 SHA512 1e607523c31111a5e9db0588d44b64b4a3a9cbadb6bfd6879f655bce25d19c74ad7e4d07f7c8f7d2c03747e5b6c034bdd8347dee0eaaa07239bd8bb7c735f53d
 MISC metadata.xml 1245 BLAKE2B a04e1e5a6af857100b8b569f57f4d2610593e9eb741513e4e6405a8fa9828471b92aaa1ad57a3163dc2f251b5664493692f92477b7191621ff8fd76eed9f57e7 SHA512 81257f7be3b21bf10caad654d5747ef2d978c0df5a05049b890420e2d170b7a4fa06151da0604a8b1b6e7daf2fb01344003c9243205a94b4040c580beb414836
diff --git a/sci-mathematics/boolector/boolector-3.2.3.ebuild b/sci-mathematics/boolector/boolector-3.2.3.ebuild
new file mode 100644
index 000000000000..1497adc7c225
--- /dev/null
+++ b/sci-mathematics/boolector/boolector-3.2.3.ebuild
@@ -0,0 +1,84 @@
+# Copyright 1999-2023 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+PYTHON_COMPAT=( python3_{10..12} )
+
+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
+
+	dodir "/usr/$(get_libdir)"
+	mv "${ED}/usr/lib"/*.so "${ED}/usr/$(get_libdir)/" || die
+
+	if use examples ; then
+		dodoc -r examples
+	fi
+}
diff --git a/sci-mathematics/boolector/files/boolector-3.2.3-cmake-std.patch b/sci-mathematics/boolector/files/boolector-3.2.3-cmake-std.patch
new file mode 100644
index 000000000000..fd0d840fc64c
--- /dev/null
+++ b/sci-mathematics/boolector/files/boolector-3.2.3-cmake-std.patch
@@ -0,0 +1,10 @@
+--- a/CMakeLists.txt
++++ b/CMakeLists.txt
+@@ -196,7 +196,6 @@ set_option(USE_PICOSAT ON)
+ #       btorconfig.h and they are else not yet added to CMAKE_C(XX)_FLAGS at
+ #       file generation time (configure_file).
+ add_required_c_flag("-std=gnu99")
+-add_required_cxx_flag("-std=gnu++11")
+ 
+ add_check_c_cxx_flag("-W")
+ add_check_c_cxx_flag("-Wall")
diff --git a/sci-mathematics/btor2tools/Manifest b/sci-mathematics/btor2tools/Manifest
index 73dde492fd6c..4e1de159f735 100644
--- a/sci-mathematics/btor2tools/Manifest
+++ b/sci-mathematics/btor2tools/Manifest
@@ -1,4 +1,5 @@
+AUX btor2tools-1.0.0_pre20220518-btorsplit-cstdint.patch 235 BLAKE2B ba9c0136c7c95dea4a39023ac614c129cc1e0fd7ea95ad6cbf6b18e1345d9c04a42235d36448d7867c16f5eaa240b43b3715ebd612c378a557e4dde8edc5a1e1 SHA512 450d46949abfae1aaccd08545c102dcf8d6172cfc655be7e80760d57e30211f1861638cf5f27b4603dbde6ac7eecc6bb5a52ee41c10748132b001870c5d30c00
 AUX btor2tools-1.0.0_pre20220518-cmake-clfags.patch 551 BLAKE2B 8cc8c427a2ec7defc4bd7f251b2a2a6484bc321b0f0d88a7099e8a69963cfbf6b69d13dbce4f54874d8138ec01ae870752a947a01c93c3cf996456c546ce012e SHA512 a6c446440405ab44b9bffb8316d170782241d77334c5837820ee0ea1e6da5ff97121b966a49af9c15e8e0e2a184ae3781166eb9c0ba07c4319dd92fed105ae2d
 DIST btor2tools-1.0.0_pre20220518.tar.gz 87420 BLAKE2B df8ddc8f286c32c580a8feaf0c7e90dff113d2b0303e3da0a378f2906cd34134ea91707cd40c95c38782990bf4d815416b3a566680f4d6668ddca46321ae530a SHA512 96e17327de311b3d16e086031038a8248431d0dda75b83ce137d6526a096b69fc062290f92ec5b58fffb56aa25437835f97a96bd15f0044d4d52263bf386d928
-EBUILD btor2tools-1.0.0_pre20220518-r1.ebuild 783 BLAKE2B ee38ed21c306323f3876201094b4d27de0133a3bc183ff95876851615428d92c66747db4bacc702641d394dcf1c8b5905726324454a8adde8d7c3ce1fb58b1bf SHA512 10d381a2aabd2d015caaf84b04b892bff00b997bc14fa537b112ae9ce56efc3d8a0670c781a611342a3ef736f5a6a795fc6fa0d3db1d9947789e74b82214d11d
+EBUILD btor2tools-1.0.0_pre20220518-r1.ebuild 875 BLAKE2B 208de5c4db336917c059efa6ecd814813ee504a212e7ad93355ee810c9ad6673182c01b9ea135db43387fed295149908b2ae020b90b2948961606f59d151f196 SHA512 a0de1782e095a5db9bb5a7df70202f0edf997ae916f753076ea4836135ed624a9f929b3f031b7a3eb15902caef3e31d8db6f506c25454521e57237c872abe0b5
 MISC metadata.xml 437 BLAKE2B 93f1e3a98b8dd3edd95de3bd8f830427a9e05dcfc73690899ed16ec49be25bfd524d86fcaa9735d15c22515b98d13ded8a95c7a39e4970e3035c72e4cbe7d544 SHA512 39b7bd39e597f6d3086358738cb2d668f0317af3a8674eb4c032f59c64de0ceada799900bd193f244f049f51e1a91dcd9bb4474db39ac88967086206f3090a62
diff --git a/sci-mathematics/btor2tools/btor2tools-1.0.0_pre20220518-r1.ebuild b/sci-mathematics/btor2tools/btor2tools-1.0.0_pre20220518-r1.ebuild
index 58780bf5c440..c2cee9e4d4ea 100644
--- a/sci-mathematics/btor2tools/btor2tools-1.0.0_pre20220518-r1.ebuild
+++ b/sci-mathematics/btor2tools/btor2tools-1.0.0_pre20220518-r1.ebuild
@@ -3,20 +3,22 @@
 
 EAPI=8
 
-[[ ${PV} == *_pre20220518 ]] && COMMIT=b8456dda4780789e882f5791eb486f295ade4da4
-
 inherit cmake
 
 DESCRIPTION="Generic parser and tools for the BTOR2 format"
 HOMEPAGE="https://github.com/Boolector/btor2tools/"
 
-if [[ ${PV} == *9999* ]] ; then
+if [[ "${PV}" == *9999* ]] ; then
 	inherit git-r3
+
 	EGIT_REPO_URI="https://github.com/Boolector/${PN}.git"
 else
+	[[ "${PV}" == *_pre20220518 ]] && COMMIT=b8456dda4780789e882f5791eb486f295ade4da4
+
 	SRC_URI="https://github.com/Boolector/${PN}/archive/${COMMIT}.tar.gz
 		-> ${P}.tar.gz"
-	S="${WORKDIR}"/${PN}-${COMMIT}
+	S="${WORKDIR}/${PN}-${COMMIT}"
+
 	KEYWORDS="~amd64 ~x86"
 fi
 
@@ -24,13 +26,16 @@ LICENSE="MIT"
 SLOT="0"
 IUSE="examples"
 
-PATCHES=( "${FILESDIR}"/${P}-cmake-clfags.patch )
+PATCHES=(
+	"${FILESDIR}/${PN}-1.0.0_pre20220518-btorsplit-cstdint.patch"
+	"${FILESDIR}/${PN}-1.0.0_pre20220518-cmake-clfags.patch"
+)
 
 src_install() {
 	cmake_src_install
 
 	if use examples ; then
-		insinto /usr/share/${PN}
+		insinto "/usr/share/${PN}"
 		dodoc -r examples
 	fi
 }
diff --git a/sci-mathematics/btor2tools/files/btor2tools-1.0.0_pre20220518-btorsplit-cstdint.patch b/sci-mathematics/btor2tools/files/btor2tools-1.0.0_pre20220518-btorsplit-cstdint.patch
new file mode 100644
index 000000000000..50ebb98fcf98
--- /dev/null
+++ b/sci-mathematics/btor2tools/files/btor2tools-1.0.0_pre20220518-btorsplit-cstdint.patch
@@ -0,0 +1,10 @@
+--- a/src/btorsplit.cpp
++++ b/src/btorsplit.cpp
+@@ -19,6 +19,7 @@
+ #include <sstream>
+ #include <unordered_set>
+ #include <vector>
++#include <cstdint>
+ 
+ /*--------------------------------------------------------------------------*/
+ 
diff --git a/sci-mathematics/proverif/Manifest b/sci-mathematics/proverif/Manifest
index ea85697f9072..58872446201a 100644
--- a/sci-mathematics/proverif/Manifest
+++ b/sci-mathematics/proverif/Manifest
@@ -1,5 +1,5 @@
 AUX 50proverif-gentoo.el 650 BLAKE2B d31acd5c6aeeb2b938b0a475c896f0345149abc500bc98e889a89b2b241b8e59890544b64997eb7f029fe048de3fc696a2290bf1a707d9898b166458065f4d22 SHA512 44e6058ffc609a6475b21350148d677dfc0cd8846b7441541ed33b9f10bc789c4f1177ad517e684cc19f9e1ac34066a023cb003197be8c376f3c3cf99e7ff937
 DIST proverif-v2.04.tar.bz2 61001112 BLAKE2B 03364d315bfa3d6cc8dfb68819be6b92301f554cf7ae4db0c4b9d8190a7d7576b79295dd536bf1356e12679028c100e6040d8c4e4299cf137c15114caf0216d2 SHA512 dbfafa62f4df72044b05563e10219b034ad49dd972598bf72eba616f2a88ff1cb85c3ee7bb9235050d0f35dbde750bffddbc93897b9ca2101dc6d153d3ea5575
-EBUILD proverif-2.04.ebuild 1184 BLAKE2B d160905bd90e94312dac9d5ba1964cec592cdab92b4f07dea474975134f9e10b5b60c4f512b5addf2e1a29a98064cbe762ca0b7c25d72e160697352fbaadd396 SHA512 b60d6a944a92f35c1768f0539357bf964c5e3418c1cd9886d208156735e1d16767256b49a5d55eb65e1172017dec0d6662dd6bbd5ecc17e4acc4d91de4e65600
-EBUILD proverif-9999.ebuild 1184 BLAKE2B d160905bd90e94312dac9d5ba1964cec592cdab92b4f07dea474975134f9e10b5b60c4f512b5addf2e1a29a98064cbe762ca0b7c25d72e160697352fbaadd396 SHA512 b60d6a944a92f35c1768f0539357bf964c5e3418c1cd9886d208156735e1d16767256b49a5d55eb65e1172017dec0d6662dd6bbd5ecc17e4acc4d91de4e65600
+EBUILD proverif-2.04-r1.ebuild 1215 BLAKE2B 96842c9a3971326e7dbe1d49060a0bd6f1449375b0a4054153ad23922978084711b78f4a595cc578b2a6015ea7e6a0da128917e36f3d784cdcf07adba7d03475 SHA512 bb68fb16e894a32ad8d1071b63fcd98b2697e2cc2745dd843dc66f7c3cfe45d00a1f6c393d0a86c576fc97f430a465e26c68b9029fdfcf644132667a2a9d15ca
+EBUILD proverif-9999.ebuild 1215 BLAKE2B 96842c9a3971326e7dbe1d49060a0bd6f1449375b0a4054153ad23922978084711b78f4a595cc578b2a6015ea7e6a0da128917e36f3d784cdcf07adba7d03475 SHA512 bb68fb16e894a32ad8d1071b63fcd98b2697e2cc2745dd843dc66f7c3cfe45d00a1f6c393d0a86c576fc97f430a465e26c68b9029fdfcf644132667a2a9d15ca
 MISC metadata.xml 1638 BLAKE2B 61f7bbf62117942baa127c9cabb9f15ea797b8ea8b313ed720a15a6d96dba1e78e8ad9921739a277175eb008b8c697bdd4b424f472e984d9a01ee63e75ced6f2 SHA512 9bbd77f4247eb5c210e0f1424100541b16235701dc048c2a7ca1485fcdbcbf5a5ab598c8f5a11e234c77f74560e2312f4496af598f07cb504561f60acc2558f9
diff --git a/sci-mathematics/proverif/proverif-2.04.ebuild b/sci-mathematics/proverif/proverif-2.04-r1.ebuild
index 248a70edb9d2..a70d69a747de 100644
--- a/sci-mathematics/proverif/proverif-2.04.ebuild
+++ b/sci-mathematics/proverif/proverif-2.04-r1.ebuild
@@ -9,14 +9,16 @@ DESCRIPTION="Cryptographic protocol verifier in the formal model"
 HOMEPAGE="https://bblanche.gitlabpages.inria.fr/proverif/
 	https://gitlab.inria.fr/bblanche/proverif/"
 
-if [[ ${PV} == *9999* ]] ; then
+if [[ "${PV}" == *9999* ]] ; then
 	inherit git-r3
+
 	EGIT_REPO_URI="https://gitlab.inria.fr/bblanche/${PN}.git"
 	S="${WORKDIR}/${P}/${PN}"
 else
 	SRC_URI="https://gitlab.inria.fr/bblanche/${PN}/-/archive/v${PV}/${PN}-v${PV}.tar.bz2"
-	KEYWORDS="~amd64 ~x86"
 	S="${WORKDIR}/${PN}-v${PV}/${PN}"
+
+	KEYWORDS="~amd64 ~x86"
 fi
 
 LICENSE="GPL-2+"
@@ -24,9 +26,10 @@ SLOT="0"
 IUSE="emacs"
 
 RDEPEND="
+	dev-lang/ocaml:=[ocamlopt]
 	emacs? ( >=app-editors/emacs-25:* )
 "
-BDEPEND="
+DEPEND="
 	${RDEPEND}
 "
 
diff --git a/sci-mathematics/proverif/proverif-9999.ebuild b/sci-mathematics/proverif/proverif-9999.ebuild
index 248a70edb9d2..a70d69a747de 100644
--- a/sci-mathematics/proverif/proverif-9999.ebuild
+++ b/sci-mathematics/proverif/proverif-9999.ebuild
@@ -9,14 +9,16 @@ DESCRIPTION="Cryptographic protocol verifier in the formal model"
 HOMEPAGE="https://bblanche.gitlabpages.inria.fr/proverif/
 	https://gitlab.inria.fr/bblanche/proverif/"
 
-if [[ ${PV} == *9999* ]] ; then
+if [[ "${PV}" == *9999* ]] ; then
 	inherit git-r3
+
 	EGIT_REPO_URI="https://gitlab.inria.fr/bblanche/${PN}.git"
 	S="${WORKDIR}/${P}/${PN}"
 else
 	SRC_URI="https://gitlab.inria.fr/bblanche/${PN}/-/archive/v${PV}/${PN}-v${PV}.tar.bz2"
-	KEYWORDS="~amd64 ~x86"
 	S="${WORKDIR}/${PN}-v${PV}/${PN}"
+
+	KEYWORDS="~amd64 ~x86"
 fi
 
 LICENSE="GPL-2+"
@@ -24,9 +26,10 @@ SLOT="0"
 IUSE="emacs"
 
 RDEPEND="
+	dev-lang/ocaml:=[ocamlopt]
 	emacs? ( >=app-editors/emacs-25:* )
 "
-BDEPEND="
+DEPEND="
 	${RDEPEND}
 "