gentoo auto-resync : 16:07:2023 - 04:41:57

22 files changed, 20 insertions, 977 deletions

diff --git a/sci-mathematics/Manifest.gz b/sci-mathematics/Manifest.gz
index 1ccfbfd918db..24016bf7d1b2 100644
--- a/sci-mathematics/Manifest.gz
+++ b/sci-mathematics/Manifest.gz
diff --git a/sci-mathematics/coq-mathcomp/Manifest b/sci-mathematics/coq-mathcomp/Manifest
index f8edfb9d239c..d077c66292e6 100644
--- a/sci-mathematics/coq-mathcomp/Manifest
+++ b/sci-mathematics/coq-mathcomp/Manifest
@@ -1,5 +1,3 @@
-DIST coq-mathcomp-1.15.0.tar.gz 1359283 BLAKE2B 7a575e49f93c6527da877a4044ae97d82fa48f242c29b5ed22bc58154f422e14716cb481aa4de96963cfd3cf1aad5dcd76608d85ec4b68ce1a5601b13e3add3e SHA512 96d3bc53ab83740675e6d0bd6e31479e16d986994d1725e9a0466ef46cd517e4ced966d6b1e34b3ff1b15327a2058afcc914b91dba3c5354021d4ef224b8348c
 DIST coq-mathcomp-1.16.0.tar.gz 1377232 BLAKE2B f9246ff2a6e583facc31278728b0865fdfb4d9cb6422687643321712b22d7fa61e40dd95e7782ba8443f66b61f9f6a82caead767a6985c87e6fe731a04494713 SHA512 80dc82e0deea4b3e05811b9dca3cf7c0169387288a5cc5c7e95c452c7aa041a37df34d93546c6597c6717106e20dc98400c7b0bbb8d1d1915e2063cfe6fd300b
-EBUILD coq-mathcomp-1.15.0-r1.ebuild 603 BLAKE2B 7c7c32093a78718bdfe6565ae49fe2e7055db9aa90da82b149e940e5ae512f5a8f71cccf79607fdcc080eba03fd6a0245271445621da150b32f241e53f4890d7 SHA512 86f744bf686403ffe75651175479da7b70fa006a5c92290a8badea44a26105f3fa1d5bc0e62569f5286a12a6231fed2ba3759337525103dec1e73be1f80fc18d
 EBUILD coq-mathcomp-1.16.0-r1.ebuild 627 BLAKE2B 14853b4eedc1d123b7d5d16da9f16883a6c4e614d09ae3411c217e72a77f3b00719d48375c13708dbc264142aa8e50270251365a97c80d09487851a41d2b8d58 SHA512 9beef42e82af16d3e006cdd9062dafbcfdbd37260f0048413fe4632b624280d153e2cc6dbf8d5edae220f2ce778bf5d524ca9b6561857982da980791d28a0544
 MISC metadata.xml 511 BLAKE2B 3936f96cbf938fb9de97b080566d7fdde222d7dd303ccf842c76e7bd113b31c05136aea043c354bbd2ac6d4f61e2cba4e738f9f325059d36b7bae4feaed1ae89 SHA512 af2a4cfded0990d95e0a4b77ba69aebea09dee075f9eb4023b14c4788cd4118a78b3b5a4349fed11fff347061ab4bf59a4c63c8f43b22f8513054f1b3817af2f
diff --git a/sci-mathematics/coq-mathcomp/coq-mathcomp-1.15.0-r1.ebuild b/sci-mathematics/coq-mathcomp/coq-mathcomp-1.15.0-r1.ebuild
deleted file mode 100644
index bb3f88518455..000000000000
--- a/sci-mathematics/coq-mathcomp/coq-mathcomp-1.15.0-r1.ebuild
+++ /dev/null
@@ -1,23 +0,0 @@
-# Copyright 1999-2023 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=8
-
-DESCRIPTION="Mathematical Components for the Coq proof assistant"
-HOMEPAGE="https://github.com/math-comp/math-comp/"
-SRC_URI="https://github.com/math-comp/math-comp/archive/mathcomp-${PV}.tar.gz
-	-> ${P}.tar.gz"
-S="${WORKDIR}"/math-comp-mathcomp-${PV}/mathcomp
-
-LICENSE="CeCILL-B"
-SLOT="0/${PV}"
-KEYWORDS="~amd64"
-
-RDEPEND="
-	dev-lang/ocaml:=
-	>=sci-mathematics/coq-8.16.0:=
-"
-DEPEND="${RDEPEND}"
-
-# Do not complain about CFLAGS etc since ML projects do not use them.
-QA_FLAGS_IGNORED='.*'
diff --git a/sci-mathematics/coq-serapi/Manifest b/sci-mathematics/coq-serapi/Manifest
index 9259038546bc..64f3ef42c26e 100644
--- a/sci-mathematics/coq-serapi/Manifest
+++ b/sci-mathematics/coq-serapi/Manifest
@@ -1,11 +1,5 @@
 AUX 50sertop-gentoo.el 85 BLAKE2B d06e7c0823a3bedbf5f9c91ea8ea26bc9ed9d2ea44030316a1f3d65c19e51d874f03c845af5ae8237a9562cff7c81e24196c5ae29e54d79d1ba322f51904ba5d SHA512 42e61d798800d2e4c7e0702bdff53401a06ff6def54a1c7c0a8a6fd3e6a2f502c48bc84a04356818aa2ec5241bdd63b407837df123bfad76fafb78cf8a5a6cca
 AUX coq-serapi-sertop.el-path.patch 319 BLAKE2B 272eca8af934e10e978d149f90ee702fba443db7506468dda344242c5fe8a336f3ba3836c536bfac9ec6e540e1ee2f4c1a031d69e42901fbea92441b64e4c2a5 SHA512 5d228659e7c07e8fae69ffbff9d6a9de3113aa444c467194ce9e238a0db86c59c2be45b3e14683e47c2453c701b869e53647c9b051652af5ced8f4b3b5a15e73
-DIST coq-serapi-0.16.1.tar.gz 271068 BLAKE2B 5e832f4b2d2627938f2399b3eff111a15987d7733e30ba6f6328dc0110631a1c42a212c5ed464037f8c521c11c46bf8bb8665bfdd93b5969949cdec584a42e18 SHA512 348a984897f99dd4f08a409251eaf50f792aa1fe96d71d5f895f3153c05131b2d6b15f10a18cf704e978676562547d0869a310e8d6969ffe69d5bdf1c212b756
-DIST coq-serapi-0.16.2.tar.gz 272807 BLAKE2B 20a04ae8b18fba7c6d8346515d4f610750e32e6a521dc65afd7a624ae07ddea75b4f8aed237ba95ed16667f3867b35dd914b35eab966187f6f41f547f3bac8d6 SHA512 f7aba7009f14302246eabe595af7cb72103b8904e45c647783326f46d51b1331b30dd515364c4b909f02c42c5bf7bd367dc0fe64eb9c88b062cd79113b53306b
-DIST coq-serapi-0.16.3.tar.gz 272910 BLAKE2B e3e5e070e98d9dd41d3b7ef589abcb57137925ed637be7c94aaa387dbe996ce72d4c98f37b6e8ee9ca196af6deb291afbb326ac6aeb8c1809331bbc1824a0786 SHA512 fccc946d87de4fbe797df6a898704ead04708323bdf3b799ced074ba1539d7d5b54d3cc439f7641fe3bf289069ca42278137a10c8de211b1563df9b6a61ad8c5
 DIST coq-serapi-0.17.0.tar.gz 273903 BLAKE2B 155d865650f773d71e0ddd10869852916de5e539b3b3f4d03d58259790482be45d668035975d5be768776f7ef5947f0d7227f0f6624bc7f64cefd009e9a83ecb SHA512 d9085b4215c233c47f78386d8771348768c9cbbf0716dfa4da3ff8c8c96d2e78b203098314175ef2bb9959096f8b0ec03a9fb5d696d0451eeee0713bd48afa2b
-EBUILD coq-serapi-0.16.1.ebuild 1472 BLAKE2B 5c0465c49866d234a30137572b01d55a43e9284f20487922e20341821095dcd144b377f7ec06f4d51395c23bd15f6d86bc022581fff14dabf0fdc20be136be95 SHA512 438a5770a640de6ae277f780ee5794509c031eacc637a5461d8cdf95d9403d47ecaaccc20aa6e09dc0a2b55f3163eb8445a3189235de0e09f04bfd7b27e10242
-EBUILD coq-serapi-0.16.2-r1.ebuild 1442 BLAKE2B 04cc83c611cd63bbee704cf575a8a8ba3713902c7182ebeee5b638ff50c14b51f2ec95939a9920eae353ec93656dcfb8c45c5e8808c489e15fff0fc47d91cc17 SHA512 4d4549fcf593184102ff3162a228c123f74bd13163d2c2831bbec094e5850e23b6be0d01d28ff19c84368bb98dc5ef16fd07e3061a14122ba970700ba1ebbc75
-EBUILD coq-serapi-0.16.3.ebuild 1488 BLAKE2B d5e1e072d30e2a3704d0309fb93f96df7113843e3cb94f2338bb16e284941de4d594d74b87c3e69813772b20193982a89d6464e6471f96f9f1a3d56afc47517b SHA512 377641d6d27b9e7386b130feed16071f3d928321d48b0fdf54eafb135642dd480bbf91608454472c7714f9eb89d714e4452d8eb39cb9d57a6f6fabe061011a4c
 EBUILD coq-serapi-0.17.0.ebuild 1488 BLAKE2B 00bb0f1f7e3fdd53fbe77847638647a7aabc3f50da29bad4c684bf753b6f154116c44502e7d173b5cd5783b3ab7482aed71acd9f51c9529e105b799c80b94b22 SHA512 dde7170b0334dcd5298aa1f6a629c77b2fcc6de5d3f2d92bc23d36c068878a9b19415340138e26c7c5b8db1e3c7b7733f419e0d9162fb8548325960f12a5f163
 MISC metadata.xml 935 BLAKE2B e1444df414ce499df466597f5e0949e8ebf2d6da23d77028546324109659f58c5f0284a315ea062410a2f2e4631aac8d3564664719e89d76ad6ded9bb8ba7a5f SHA512 172fedbb2aa42e2be9aff426d64fcd69d2dfa206bb0e6072c6ecdc14a1923a2f0676303d8d8aebfe9a3e96e0a1e89185d2d4952bdb9ba1fff44b3891f26d6bf7
diff --git a/sci-mathematics/coq-serapi/coq-serapi-0.16.1.ebuild b/sci-mathematics/coq-serapi/coq-serapi-0.16.1.ebuild
deleted file mode 100644
index fed96a12b2dc..000000000000
--- a/sci-mathematics/coq-serapi/coq-serapi-0.16.1.ebuild
+++ /dev/null
@@ -1,66 +0,0 @@
-# Copyright 1999-2022 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=8
-
-COQV=8.16.0
-
-inherit elisp-common dune
-
-DESCRIPTION="Serialization library and protocol for interaction with the Coq proof assistant"
-HOMEPAGE="https://github.com/ejgallego/coq-serapi/"
-# The tarball in SRC_URI is comprised of <supported coq>+<package version>
-SRC_URI="https://github.com/ejgallego/${PN}/archive/${COQV}+${PV}.tar.gz
-		-> ${P}.tar.gz"
-S="${WORKDIR}"/${PN}-${COQV}-${PV}
-
-LICENSE="GPL-3+"
-SLOT="0/${PV}"
-KEYWORDS="~amd64"
-IUSE="emacs +ocamlopt test"
-RESTRICT="!test? ( test )"
-
-RDEPEND="
-	>=sci-mathematics/coq-${COQV}:= <sci-mathematics/coq-8.17:=
-	>=dev-ml/ppx_sexp_conv-0.13.0:= <dev-ml/ppx_sexp_conv-0.15.0:=
-	dev-ml/cmdliner:=
-	dev-ml/ppx_compare:=
-	dev-ml/ppx_deriving:=
-	dev-ml/ppx_deriving_yojson:=
-	dev-ml/ppx_hash:=
-	dev-ml/ppx_import:=
-	dev-ml/sexplib:=
-	dev-ml/yojson:=
-"
-DEPEND="${RDEPEND}"
-BDEPEND="
-	emacs? ( >=app-editors/emacs-23.1:* )
-	test? ( sci-mathematics/coq-mathcomp )
-"
-
-PATCHES=( "${FILESDIR}"/${PN}-sertop.el-path.patch )
-SITEFILE="50sertop-gentoo.el"
-
-src_compile() {
-	dune_src_compile
-
-	use emacs && elisp-compile sertop.el
-}
-
-src_install() {
-	dune_src_install
-
-	rm -r "${D}"/usr/share/emacs || die
-	if use emacs ; then
-		elisp-install ${PN} sertop.el{,c}
-		elisp-site-file-install "${FILESDIR}/${SITEFILE}"
-	fi
-}
-
-pkg_postinst() {
-	use emacs && elisp-site-regen
-}
-
-pkg_postrm() {
-	use emacs && elisp-site-regen
-}
diff --git a/sci-mathematics/coq-serapi/coq-serapi-0.16.2-r1.ebuild b/sci-mathematics/coq-serapi/coq-serapi-0.16.2-r1.ebuild
deleted file mode 100644
index 44a2d0a9b186..000000000000
--- a/sci-mathematics/coq-serapi/coq-serapi-0.16.2-r1.ebuild
+++ /dev/null
@@ -1,67 +0,0 @@
-# Copyright 1999-2023 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=8
-
-COQV=8.16.0
-
-inherit elisp-common dune
-
-DESCRIPTION="Serialization library and protocol for interaction with the Coq proof assistant"
-HOMEPAGE="https://github.com/ejgallego/coq-serapi/"
-
-# The tarball in SRC_URI is comprised of <supported coq>+<package version>
-SRC_URI="https://github.com/ejgallego/${PN}/archive/${COQV}+${PV}.tar.gz
-		-> ${P}.tar.gz"
-S="${WORKDIR}"/${PN}-${COQV}-${PV}
-
-LICENSE="GPL-3+"
-SLOT="0/${PV}"
-KEYWORDS="~amd64"
-IUSE="emacs +ocamlopt test"
-RESTRICT="!test? ( test )"
-
-RDEPEND="
-	>=sci-mathematics/coq-${COQV}:= <sci-mathematics/coq-8.17:=
-	>=dev-ml/ppx_sexp_conv-0.13.0:=
-	dev-ml/cmdliner:=
-	dev-ml/ppx_compare:=
-	dev-ml/ppx_deriving:=
-	dev-ml/ppx_deriving_yojson:=
-	dev-ml/ppx_hash:=
-	dev-ml/ppx_import:=
-	dev-ml/sexplib:=
-	dev-ml/yojson:=
-"
-DEPEND="${RDEPEND}"
-BDEPEND="
-	emacs? ( >=app-editors/emacs-23.1:* )
-	test? ( sci-mathematics/coq-mathcomp )
-"
-
-PATCHES=( "${FILESDIR}"/${PN}-sertop.el-path.patch )
-SITEFILE="50sertop-gentoo.el"
-
-src_compile() {
-	dune_src_compile
-
-	use emacs && elisp-compile sertop.el
-}
-
-src_install() {
-	dune_src_install
-
-	rm -r "${D}"/usr/share/emacs || die
-	if use emacs ; then
-		elisp-install ${PN} sertop.el{,c}
-		elisp-site-file-install "${FILESDIR}/${SITEFILE}"
-	fi
-}
-
-pkg_postinst() {
-	use emacs && elisp-site-regen
-}
-
-pkg_postrm() {
-	use emacs && elisp-site-regen
-}
diff --git a/sci-mathematics/coq-serapi/coq-serapi-0.16.3.ebuild b/sci-mathematics/coq-serapi/coq-serapi-0.16.3.ebuild
deleted file mode 100644
index 1c0727491cf7..000000000000
--- a/sci-mathematics/coq-serapi/coq-serapi-0.16.3.ebuild
+++ /dev/null
@@ -1,70 +0,0 @@
-# Copyright 1999-2023 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=8
-
-COQ_MIN_V=8.16.0
-COQ_MAX_V=8.17.0
-
-inherit elisp-common dune
-
-DESCRIPTION="Serialization library and protocol for interaction with the Coq proof assistant"
-HOMEPAGE="https://github.com/ejgallego/coq-serapi/"
-
-# The tarball in SRC_URI is comprised of <supported coq>+<package version>
-SRC_URI="https://github.com/ejgallego/${PN}/archive/${COQ_MIN_V}+${PV}.tar.gz
-	-> ${P}.tar.gz"
-S="${WORKDIR}"/${PN}-${COQ_MIN_V}-${PV}
-
-LICENSE="GPL-3+"
-SLOT="0/${PV}"
-KEYWORDS="~amd64"
-IUSE="emacs +ocamlopt test"
-RESTRICT="!test? ( test )"
-
-RDEPEND="
-	>=sci-mathematics/coq-${COQ_MIN_V}:= <sci-mathematics/coq-${COQ_MAX_V}:=
-	>=dev-ml/ppx_sexp_conv-0.13.0:=
-	dev-ml/cmdliner:=
-	dev-ml/ppx_compare:=
-	dev-ml/ppx_deriving:=
-	dev-ml/ppx_deriving_yojson:=
-	dev-ml/ppx_hash:=
-	dev-ml/ppx_import:=
-	dev-ml/sexplib:=
-	dev-ml/yojson:=
-"
-DEPEND="${RDEPEND}"
-BDEPEND="
-	emacs? ( >=app-editors/emacs-23.1:* )
-	test? ( sci-mathematics/coq-mathcomp )
-"
-
-SITEFILE="50sertop-gentoo.el"
-
-PATCHES=( "${FILESDIR}"/${PN}-sertop.el-path.patch )
-
-src_compile() {
-	dune_src_compile
-
-	use emacs && elisp-compile sertop.el
-}
-
-src_install() {
-	dune_src_install
-
-	rm -r "${D}"/usr/share/emacs || die
-
-	if use emacs ; then
-		elisp-install ${PN} sertop.el{,c}
-		elisp-site-file-install "${FILESDIR}/${SITEFILE}"
-	fi
-}
-
-pkg_postinst() {
-	use emacs && elisp-site-regen
-}
-
-pkg_postrm() {
-	use emacs && elisp-site-regen
-}
diff --git a/sci-mathematics/coq/Manifest b/sci-mathematics/coq/Manifest
index 39975aa757ac..4db5821070a8 100644
--- a/sci-mathematics/coq/Manifest
+++ b/sci-mathematics/coq/Manifest
@@ -1,11 +1,7 @@
 DIST coq-8.12.0.tar.gz 6774001 BLAKE2B dc1d6adf9d4bd50d46007fbf5fd43d1ea97b6b226d89ad943419d4cb7df1439950c94b5e3cc614eb789103d1ab50535909d4ba2079eafc2caa4fd91db30e747d SHA512 8a64624c578ce0ab781fb3b1f162bd8b095735ad891fdad2fb7c40849afbdc7c1360187c6b62a5ef2982566f4c6c78029240c611ae769943a5250af300eb1240
-DIST coq-8.15.2.tar.gz 7222794 BLAKE2B 2f187982a56cb0a512af838ee321b245f9a44b0c32f5413aafcef8e5b7f933e9b05ba521c3e681a6c6973ca2b7ec5965a8b69b2febb978ce7cf246755187f656 SHA512 6a5487912dedb6e54145bf3f177a091cffe13429ba2f73db7c1cc241fe10e86340c968e19cefba7d680facce55f4e914cbd16a317264b109a6f9a01ec822a8c5
-DIST coq-8.16.1.tar.gz 7401345 BLAKE2B fa6bbcd6b4ee29feaf7475f58193209afeae0bf8b6e3640f2f1cf40dfcee7d7f1fb3f371e8790b8d11c993b5f234e9175f1f5036a7286b7c6569720ddd3985f7 SHA512 e9c82f1a180c2e3946628e8e039999a1841397a5b4cd77f158de69876fa43b5c0f61ce76c510cc2b2f646a489110aea59da452b88ddd7850d1eab4105f1382f5
 DIST coq-8.17.0.tar.gz 7504612 BLAKE2B 90ff0e187e13a6501580733f0e92dbaba0ddc520b418246c743f0c282e74cee3e1d69ad0249cddfd5b8f3ba363bc58cb91aad33d0936ae38afde0f4c97d47a72 SHA512 2f77bcb5211018b5d46320fd39fd34450eeb654aca44551b28bb50a2364398c4b34587630b6558db867ecfb63b246fd3e29dc2375f99967ff62bc002db9c3250
 DIST coq-8.17.1.tar.gz 7506035 BLAKE2B 29b5b11666185ec293f50264f5a8ad66433c3ce05d74128b524f6fc3c6810551fe76d11d6f9db7d3741b829ac8bacb66948aad522d0cd2c487692c3df8b563ff SHA512 9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b
 EBUILD coq-8.12.0-r2.ebuild 1854 BLAKE2B 96a5bc026d7cef8218fa0f10401c697df908487a2a510f349a57d080e2c59c6fc6237223fbe82f5114c6ee70ebdfd9fffc9812bc2e8981febac635efd94b3035 SHA512 3936eafb537044833b310fafc9ba4595bb6deba71679177fbb807c59e3bfcd44f8a98c26077fda791619479b5efdefd64f6235ce2ae7c599489c4f0e8f8e003b
-EBUILD coq-8.15.2.ebuild 2402 BLAKE2B a1f9f44c17ea51c1a0536d02eaddbeba7eb5e441ec8562da3b9776dbafafbd30c50beb821d248e0a51dc56b3a5bec7feb36811d92277609d405b01229bdda17f SHA512 45c64aa13323c97c29dd4eeccc5b4e228b6abf51a3717bf62dee0c102df13c9a809073150d82be8ae7a07d43f62f52b4b7d2a69908f0ffed646b64a44d46c7e3
-EBUILD coq-8.16.1.ebuild 2418 BLAKE2B 09538efce3b1ba1b96141fe56b4328ed5fdd9a2c3aeeabb94ab35af59027748e4e75f456edd6ea81d97f8a7cd2ace7c6a89af1c815139168bd2728ad8ceafc7e SHA512 37dd16c4b7d7ebb9c380f47e24c25bbdf361db401d593f1a0d21cd0842dc4a1c6ebfd1bafd1d6c661885811f2b00c3d1665e78efcc385c478216b832e7889a51
-EBUILD coq-8.17.0.ebuild 2317 BLAKE2B ff2958b7e82400115ab634dd00bac13df99ba088d8d2ec48ad61663ba0aa3690e3cad26badedad5fd12958df4c7a343b5c9d2d827a2a7aac3ba35e9ddfe3f222 SHA512 4c04bb4aa2d97dfa21868e6246d8a35d96b55e80c7bf6206ce1c67f46102c449cad25f7062c93c7defdb0e118be57c8f86d3c3323df53ce3c794617a7d4ed6d5
-EBUILD coq-8.17.1.ebuild 2318 BLAKE2B 43895300c1c9b754f5c1d1cfc2140318f8ef32014bcfa59e47e21931efe8d9d115637791b0ddad99c6ecea9fefc172bfddaaef048cffe99ae769fdb807cef8eb SHA512 6f9149a727109283ec4f4ca883016478f0e77464542ca3798e068d3eea2d682eba1b226b37bdc1bc9e4c35c8c19997e1720f3abf2d42c6fc790d148137e0f8a4
+EBUILD coq-8.17.0.ebuild 2557 BLAKE2B 33c12f0cb8461ebe6489b4e28fb5816dfe7a879404c0de24ff9f151872c7c1838c58536302589d86efe50a200dae3495d5c816aa95936cadf59ee0dea778a83e SHA512 d8384bf764906ff5f621cd0fc5380d34ecbfdc2f801b0ffd152ffd67621e7f80af5cf4c4637dcdceb1e34e38cda979316c2e0f5ca2c059e316deabf266207c01
+EBUILD coq-8.17.1.ebuild 2558 BLAKE2B 9a66cc04a21af88972bfdcbd11af4e469a929a62d488ca3c18cbde8d31b23ee55c95a424032ce0060bd3eac3101d9541c7fb765b15364f85cf863ba793716c53 SHA512 b71e8e58c91f2dfb937b2e70637181ebcca2f3c255f216f27482eb863ab123b33eb887b105e57d04a8b18413b9b129f54bf475775f4cbf6e6074599eda164981
 MISC metadata.xml 1047 BLAKE2B 9f6defdf213139ee6549bc8f3b36ce5e8f53ea73bd5aad9262932cbaea7e90bd97c9ffc9dbbd03ac50097c5a6f19f5ddf00dd2b74cc6a5349faf1b597244fb67 SHA512 0f5bfbdd9ffd6f64379e697ed7cf90c2d9257cd1815e520aa14235f1cb399d20fc863221a0cae803cc88e5975be964b9debc3d750a6378ea157146f2e567c5dc
diff --git a/sci-mathematics/coq/coq-8.15.2.ebuild b/sci-mathematics/coq/coq-8.15.2.ebuild
deleted file mode 100644
index c94ce21f129a..000000000000
--- a/sci-mathematics/coq/coq-8.15.2.ebuild
+++ /dev/null
@@ -1,111 +0,0 @@
-# Copyright 1999-2023 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=8
-
-MY_PV=${PV/_p/pl}
-MY_P=${PN}-${MY_PV}
-
-inherit desktop dune
-
-DESCRIPTION="Proof assistant written in O'Caml"
-HOMEPAGE="http://coq.inria.fr/"
-SRC_URI="https://github.com/coq/coq/archive/V${MY_PV}.tar.gz -> ${P}.tar.gz"
-S="${WORKDIR}/${MY_P}"
-
-LICENSE="LGPL-2.1"
-SLOT="0/${PV}"
-KEYWORDS="~amd64 ~x86"
-IUSE="doc gtk debug +ocamlopt"
-RESTRICT="test"  # fails
-
-RDEPEND="
-	dev-ml/zarith:=
-	|| (
-		dev-ml/num
-		<dev-lang/ocaml-4.09.0[ocamlopt?]
-	)
-	gtk? (
-		dev-ml/lablgtk:3=[sourceview,ocamlopt?]
-		dev-ml/lablgtk-sourceview:3=[ocamlopt?]
-	)
-"
-DEPEND="${RDEPEND}"
-BDEPEND="
-	doc? (
-		>=dev-java/antlr-4.7:4
-		dev-python/antlr4-python3-runtime
-		dev-python/beautifulsoup4
-		dev-python/pexpect
-		dev-python/sphinx-rtd-theme
-		dev-python/sphinxcontrib-bibtex
-		dev-tex/latexmk
-		dev-texlive/texlive-fontsextra
-		dev-texlive/texlive-latexextra
-		dev-texlive/texlive-xetex
-		media-fonts/freefont
-	)
-"
-
-DOCS=( CODE_OF_CONDUCT.md CONTRIBUTING.md CREDITS INSTALL.md README.md )
-
-src_configure() {
-	local myconf=(
-		-prefix /usr
-		-libdir /usr/$(get_libdir)/coq
-		-mandir /usr/share/man
-		-docdir /usr/share/doc/${PF}
-		-datadir /usr/share/coq
-		-configdir /etc/xdg/${PN}
-		-with-doc $(usex doc)
-	)
-
-	use debug && myconf+=( -debug )
-	use ocamlopt || myconf+=( -byte-only )
-
-	if use gtk ; then
-		if use ocamlopt ; then
-			myconf+=( -coqide opt )
-		else
-			myconf+=( -coqide byte )
-		fi
-	else
-		myconf+=( -coqide no )
-	fi
-
-	export CAML_LD_LIBRARY_PATH="${S}/kernel/byterun/"
-
-	echo "Configure options: ${myconf[@]}"
-	sh ./configure ${myconf[@]} || die "configure failed"
-}
-
-src_compile() {
-	emake STRIP="true" VERBOSE=1 COQ_USE_DUNE="" world
-}
-
-src_test() {
-	emake STRIP="true" VERBOSE=1 COQ_USE_DUNE="" check
-}
-
-src_install() {
-	local sym
-	local syms=( coq-core coqide-server )
-
-	emake STRIP="true" VERBOSE=1 COQ_USE_DUNE="" DESTDIR="${D}" install-library
-	dune-install coq-core coqide-server
-
-	if use gtk ; then
-		dune-install coqide
-		make_desktop_entry "coqide" "Coq IDE" "${EPREFIX}/usr/share/coq/coq.png"
-		syms+=( coqide )
-	fi
-
-	use doc && emake DESTDIR="${D}" install-doc-all
-	einstalldocs
-
-	# Dune installs into /usr/<libdir>/ocaml/<coq> but
-	# Coq wants /usr/<libdir>/<coq> ; symlink those directories
-	for sym in ${syms[@]} ; do
-		dosym $(ocamlc -where)/${sym} /usr/$(get_libdir)/${sym}
-	done
-}
diff --git a/sci-mathematics/coq/coq-8.16.1.ebuild b/sci-mathematics/coq/coq-8.16.1.ebuild
deleted file mode 100644
index a8dc37656492..000000000000
--- a/sci-mathematics/coq/coq-8.16.1.ebuild
+++ /dev/null
@@ -1,111 +0,0 @@
-# Copyright 1999-2023 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=8
-
-MY_PV=${PV/_p/pl}
-MY_P=${PN}-${MY_PV}
-
-inherit desktop dune
-
-DESCRIPTION="Proof assistant written in O'Caml"
-HOMEPAGE="http://coq.inria.fr/"
-SRC_URI="https://github.com/coq/coq/archive/V${MY_PV}.tar.gz -> ${P}.tar.gz"
-S="${WORKDIR}/${MY_P}"
-
-LICENSE="LGPL-2.1"
-SLOT="0/${PV}"
-KEYWORDS="~amd64 ~x86"
-IUSE="doc gtk debug +ocamlopt"
-RESTRICT="test"  # fails
-
-RDEPEND="
-	dev-ml/zarith:=
-	|| (
-		dev-ml/num
-		<dev-lang/ocaml-4.09.0[ocamlopt?]
-	)
-	gtk? (
-		>=dev-ml/lablgtk-3.1.2:3=[sourceview,ocamlopt?]
-		>=dev-ml/lablgtk-sourceview-3.1.2:3=[ocamlopt?]
-	)
-"
-DEPEND="${RDEPEND}"
-BDEPEND="
-	doc? (
-		>=dev-java/antlr-4.7:4
-		dev-python/antlr4-python3-runtime
-		dev-python/beautifulsoup4
-		dev-python/pexpect
-		dev-python/sphinx-rtd-theme
-		dev-python/sphinxcontrib-bibtex
-		dev-tex/latexmk
-		dev-texlive/texlive-fontsextra
-		dev-texlive/texlive-latexextra
-		dev-texlive/texlive-xetex
-		media-fonts/freefont
-	)
-"
-
-DOCS=( CODE_OF_CONDUCT.md CONTRIBUTING.md CREDITS INSTALL.md README.md )
-
-src_configure() {
-	local myconf=(
-		-prefix /usr
-		-libdir /usr/$(get_libdir)/coq
-		-mandir /usr/share/man
-		-docdir /usr/share/doc/${PF}
-		-datadir /usr/share/coq
-		-configdir /etc/xdg/${PN}
-		-with-doc $(usex doc)
-	)
-
-	use debug && myconf+=( -debug )
-	use ocamlopt || myconf+=( -byte-only )
-
-	if use gtk ; then
-		if use ocamlopt ; then
-			myconf+=( -coqide opt )
-		else
-			myconf+=( -coqide byte )
-		fi
-	else
-		myconf+=( -coqide no )
-	fi
-
-	export CAML_LD_LIBRARY_PATH="${S}/kernel/byterun/"
-
-	echo "Configure options: ${myconf[@]}"
-	sh ./configure ${myconf[@]} || die "configure failed"
-}
-
-src_compile() {
-	emake STRIP="true" VERBOSE=1 COQ_USE_DUNE="" world
-}
-
-src_test() {
-	emake STRIP="true" VERBOSE=1 COQ_USE_DUNE="" check
-}
-
-src_install() {
-	local sym
-	local syms=( coq-core coqide-server )
-
-	emake STRIP="true" VERBOSE=1 COQ_USE_DUNE="" DESTDIR="${D}" install-library
-	dune-install coq-core coqide-server
-
-	if use gtk ; then
-		dune-install coqide
-		make_desktop_entry "coqide" "Coq IDE" "${EPREFIX}/usr/share/coq/coq.png"
-		syms+=( coqide )
-	fi
-
-	use doc && emake DESTDIR="${D}" install-doc-all
-	einstalldocs
-
-	# Dune installs into /usr/<libdir>/ocaml/<coq> but
-	# Coq wants /usr/<libdir>/<coq> ; symlink those directories
-	for sym in ${syms[@]} ; do
-		dosym $(ocamlc -where)/${sym} /usr/$(get_libdir)/${sym}
-	done
-}
diff --git a/sci-mathematics/coq/coq-8.17.0.ebuild b/sci-mathematics/coq/coq-8.17.0.ebuild
index 495f48055a82..45b99385ac67 100644
--- a/sci-mathematics/coq/coq-8.17.0.ebuild
+++ b/sci-mathematics/coq/coq-8.17.0.ebuild
@@ -110,3 +110,12 @@ src_install() {
 
 	einstalldocs
 }
+
+pkg_preinst() {
+	# bug https://bugs.gentoo.org/910236
+	if has_version "sci-mathematics/coq:0/8.12.0" && [[ ! -L /usr/lib64/coq ]]
+	then
+		einfo "Removing colliding directory from version 8.12: /usr/lib64/coq"
+		rm -rf /usr/lib64/coq
+	fi
+}
diff --git a/sci-mathematics/coq/coq-8.17.1.ebuild b/sci-mathematics/coq/coq-8.17.1.ebuild
index f634026e1cda..fb5c53f57eed 100644
--- a/sci-mathematics/coq/coq-8.17.1.ebuild
+++ b/sci-mathematics/coq/coq-8.17.1.ebuild
@@ -110,3 +110,12 @@ src_install() {
 
 	einstalldocs
 }
+
+pkg_preinst() {
+	# bug https://bugs.gentoo.org/910236
+	if has_version "sci-mathematics/coq:0/8.12.0" && [[ ! -L /usr/lib64/coq ]]
+	then
+		einfo "Removing colliding directory from version 8.12: /usr/lib64/coq"
+		rm -rf /usr/lib64/coq
+	fi
+}
diff --git a/sci-mathematics/easycrypt/Manifest b/sci-mathematics/easycrypt/Manifest
index 0ebe95902171..f9c321bc261a 100644
--- a/sci-mathematics/easycrypt/Manifest
+++ b/sci-mathematics/easycrypt/Manifest
@@ -1,5 +1,3 @@
-DIST easycrypt-2022.04_p20220505.tar.gz 1279876 BLAKE2B 10ae22e216b8a35973ad7d1dbffe1dba9ce328b67319577cd1a7fad957f08174d1651ee6c1bab8cdf12d8fda20cb85d5a334ad41dfb3e55f9ee8beb8a233a2eb SHA512 b1231e0be787a667c836d970236d47311e490443a66bc0a3834963557b32358ad9db2008e32d427d232f2a94c72afc65bd3330b6db1eb938335791ea997b4013
 DIST easycrypt-2022.04_p20230324.tar.gz 1296898 BLAKE2B 119cb10ad5c2cd50db9f70eb858e2779cae0350b9e5370060b8045f36684a9de87ad746e75c6a7e7fcc7ad93e40bde2164866bb16e67dd2ebc3409657760cbd8 SHA512 917d5ff2fe65a1fd02a19d700cfb77910290746023458b6ed9eb9dc1290faa5469571a3c77510caac8734ad7d2ada6c7fbfc75bb933d0a57e9c303a8cf207026
-EBUILD easycrypt-2022.04_p20220505.ebuild 1055 BLAKE2B 5ee8fd75157312e59bcf4389d4b8b766cbd4edac7b3ed463b0783dc3a4d713b04f372ce3eb59a000dd04c459e5a5e3729c44a03d3f0903557afc87a14f6226c6 SHA512 85543f45160df62c453279109ad065d80aeb3729951b8a1c4c778c116849f530572ad812c14d23dbd64862c47c15062d0fd430e943d6967d1419dde8b32456ed
 EBUILD easycrypt-2022.04_p20230324.ebuild 1197 BLAKE2B a3f363f547cea997bf3e49953df448d00cf72cbc828a2ab495e636d9903fce7bb72c7b047cb0001859faac6d30d369fd6a38905a537a057b26075b1e490fe546 SHA512 48b15f4bd30f8c47d39009a76e0094f480822d9f50d5015e87b94a9c2b661a59df6f8512352886cfb26730f7797cfd81cda8150590a2cc56528203c41105b644
 MISC metadata.xml 799 BLAKE2B 967a758171a2fe87b648a29bf2663beaae7834119e55a7619c98518c96cfe459e59fe5dc72a9faea071c0b488dc8144f1c0e43677ac63646f1ba12cf831f4a88 SHA512 411ff1acad400c3e70e546fd59b20db13b0f1db121aca9f1af23da708cd82340114bc966f64cfb5a35e84967c1131c660ab260f867639932c67edf47c859c4ca
diff --git a/sci-mathematics/easycrypt/easycrypt-2022.04_p20220505.ebuild b/sci-mathematics/easycrypt/easycrypt-2022.04_p20220505.ebuild
deleted file mode 100644
index 6757aa7a057b..000000000000
--- a/sci-mathematics/easycrypt/easycrypt-2022.04_p20220505.ebuild
+++ /dev/null
@@ -1,45 +0,0 @@
-# Copyright 1999-2023 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=8
-
-[[ ${PV} == *_p20220505 ]] && COMMIT=a49a0acf5f7e2776f6b10cd49f8a201ebab0cf03
-
-inherit dune
-
-DESCRIPTION="Computer-Aided Cryptographic Proofs"
-HOMEPAGE="https://github.com/EasyCrypt/easycrypt"
-
-if [[ ${PV} == *9999* ]] ; then
-	inherit git-r3
-	EGIT_REPO_URI="https://github.com/EasyCrypt/${PN}.git"
-else
-	SRC_URI="https://github.com/EasyCrypt/${PN}/archive/${COMMIT}.tar.gz -> ${P}.tar.gz"
-	S="${WORKDIR}"/${PN}-${COMMIT}
-fi
-
-LICENSE="MIT"
-SLOT="0/${PV}"
-KEYWORDS="~amd64"
-IUSE="+ocamlopt"
-
-RDEPEND="
-	>=dev-lang/ocaml-4.08.0:=[ocamlopt?]
-	>=sci-mathematics/why3-1.5:= <sci-mathematics/why3-1.6:=
-	dev-ml/batteries:=
-	dev-ml/camlzip:=
-	dev-ml/dune-build-info:=
-	dev-ml/dune-site:=
-	dev-ml/ocaml-inifiles:=
-	dev-ml/pcre-ocaml:=
-	dev-ml/yojson:=
-	dev-ml/zarith:=
-"
-DEPEND="${RDEPEND}"
-
-src_prepare() {
-	local theories="[\"$(ocamlc -where)/easycrypt/theories\"]"
-	sed -i "s|EcRelocate\.Sites\.theories|${theories}|g" src/ec.ml || die
-
-	default
-}
diff --git a/sci-mathematics/flint/Manifest b/sci-mathematics/flint/Manifest
index 5968fddbe7fe..98296ec88d84 100644
--- a/sci-mathematics/flint/Manifest
+++ b/sci-mathematics/flint/Manifest
@@ -1,8 +1,4 @@
 AUX flint-2.9.0-remove-hardcoded-CFLAGS.patch 2131 BLAKE2B f52fbcf321fd0f0beb302480c220b1f83e382ffe893e9b22a5eed839d02c2436ba101575c272cea0fbcbdd42110d5b9dde7cf6516403cb6dde1b0fa081dae63f SHA512 fa5c057cf664cd3ba83d3ec6b31a96c8a8e4a971a8f07b11a40150e22c1e55c7ad2d8b480f119213f867e502417c48741bb438b1724393b42da27d3577116fb5
-DIST flint-2.8.4.tar.gz 5212964 BLAKE2B ddd3b9dca76ddac2070d3e12dfc4c5ea1a3b505c7bf28e41489798798d65ed2a5db12e01059816d42e5d1209166d17ee6035dcf0a94d991f78df59c6ad06b271 SHA512 1f66574a5f2f27e1f3cd0a334712c0e64f4a4b8dd57179a71f9adba4c4faff23ba8da3993f51c4f44f52a588d0d1678b1e1a272e8fe3367f2abc88e9d86ad804
-DIST flint-2.8.5.tar.gz 5212805 BLAKE2B 8922a2925b68d93fd35aa5b78eb0b8cbc6aa609498b8846ce4ff036c2fece3932a0eabb0f04a5c152147d8df3eccd6570832f55dafe4f7a35de135246454a83d SHA512 849fb61612f3becfde0d8afc019a9312a7ea07d3000a6bc558eb82babecd737e3af894d3084e4a57d52f7db0403d7298cbfa277b08e2b1f5497897637ed4825f
 DIST flint-2.9.0.tar.gz 5283894 BLAKE2B a790437ee142d8acb5cec1e6c7d21812f8d83f5d30d1e8c07e799713e96791d87792f25fbd4ce2d0d68f6a8ee2f0cde2b8d9f8db8ab26922a48485e0e90394aa SHA512 4494cba6a4e215e817d7c74ef6834c4e05a832488f4808bbd7bea8b02a4a35d47ef3c63a4f213230c712b32842f5588c503fc1cf23e5e2ddc4a4a5a1627a02ba
-EBUILD flint-2.8.4.ebuild 1528 BLAKE2B 349b7cdc5033da4096b18ff8066fcd036a5f88a8f037f4bdea02128954f03885ee70b1ae71dd3cf027c7b7aecdffb72cbbfa0196c6eb2ac0df63dea0d8ab1756 SHA512 56b3b39d5508f5ca577d8b56a89977a3f7487cc3c6e6d6f94ee236c1b4457e5c46896eeb24b39c40603a639837817cb15c46218fbabee0cd81dd3d3584fa41b3
-EBUILD flint-2.8.5.ebuild 1646 BLAKE2B bd2043190463fab0c3e6618d7910630a582f4ba0df984b6555efa28816ed9994ef4d9bd574bea6a00b29a071ff3a21443e83f46224cc8a87c2d7d710a9553260 SHA512 8dbbe5d46cd1167cd524cd231a952b137a324881e397c60fe02d057b4bfc680e7e729888c45b0457ae9b685c629e92b1591aa345f82ac7f6d2b94110db77c197
 EBUILD flint-2.9.0.ebuild 1727 BLAKE2B 6939827103566aa3a9a1d806f474b9f0734b486324a176b076db7b63145376f9d5e029874b17f229da9ed7f74738e575145d320a7f83b12a56c5092e34f848a3 SHA512 45c2257823d384a0bf178dce2767161caf0664cc28515030dbd01a51bc4c9d672c294a0cd100aafb0aa51a7427c1d9a257d20b767b9b707a0d68e75fe0b5138c
 MISC metadata.xml 640 BLAKE2B b95d6f493564025e43604bffa340fffd88fcedf29c282fcc3c18e08ac089cdf1e10837787af664dd250a77a62237bf3665ff0a3045ca52680dd67aa0b39eeba7 SHA512 a9a64076e7f0df29e6a05a9d349c530a4ee4285b6a444425681eddf6ae1e8b41f610fda0bd7cc86b5177b36f34bc3072b67c7edac2cc8c0709a032b000576a14
diff --git a/sci-mathematics/flint/flint-2.8.4.ebuild b/sci-mathematics/flint/flint-2.8.4.ebuild
deleted file mode 100644
index 3e3f1fd68fe8..000000000000
--- a/sci-mathematics/flint/flint-2.8.4.ebuild
+++ /dev/null
@@ -1,74 +0,0 @@
-# Copyright 1999-2023 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=8
-
-# ninja doesn't like "-lcblas" so using make.
-CMAKE_MAKEFILE_GENERATOR="emake"
-PYTHON_COMPAT=( python3_{9..10} )
-inherit cmake python-any-r1
-
-DESCRIPTION="Fast Library for Number Theory"
-HOMEPAGE="http://www.flintlib.org/"
-
-# flintlib.org tarballs have been broken in the past, Bill Hart suggests
-# we get them from Github (which he has control over).
-SRC_URI="https://github.com/wbhart/flint2/archive/refs/tags/v${PV}.tar.gz
-	-> ${P}.tar.gz"
-
-LICENSE="LGPL-2.1+"
-
-# Based off the soname, e.g. /usr/lib64/libflint.so -> libflint.so.15
-SLOT="0/16"
-
-KEYWORDS="amd64 ~arm ~arm64 ~ppc ~riscv ~x86"
-IUSE="doc ntl test"
-
-RESTRICT="!test? ( test )"
-
-BDEPEND="doc? (
-	dev-python/sphinx
-	app-text/texlive-core
-	dev-texlive/texlive-latex
-	dev-texlive/texlive-latexextra
-	dev-tex/latexmk
-	)
-	${PYTHON_DEPS}"
-DEPEND="dev-libs/gmp:=
-	dev-libs/mpfr:=
-	ntl? ( dev-libs/ntl:= )
-	virtual/cblas"
-RDEPEND="${DEPEND}"
-
-S="${WORKDIR}/flint2-${PV}"
-
-src_configure() {
-	local mycmakeargs=(
-		-DWITH_NTL="$(usex ntl)"
-		-DBUILD_TESTING="$(usex test)"
-		-DBUILD_DOCS="$(usex doc)"
-		-DCBLAS_INCLUDE_DIRS="${EPREFIX}/usr/include"
-		-DCBLAS_LIBRARIES="-lcblas"
-	)
-
-	cmake_src_configure
-
-	if use doc ; then
-		HTML_DOCS="${BUILD_DIR}/html/*"
-		DOCS=(
-			"${S}"/README
-			"${S}"/AUTHORS
-			"${S}"/NEWS
-			"${BUILD_DIR}"/latex/Flint.pdf
-		)
-	fi
-}
-
-src_compile() {
-	cmake_src_compile
-
-	if use doc ; then
-		cmake_build html
-		cmake_build pdf
-	fi
-}
diff --git a/sci-mathematics/flint/flint-2.8.5.ebuild b/sci-mathematics/flint/flint-2.8.5.ebuild
deleted file mode 100644
index 0ba6c58b49ec..000000000000
--- a/sci-mathematics/flint/flint-2.8.5.ebuild
+++ /dev/null
@@ -1,80 +0,0 @@
-# Copyright 1999-2023 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=8
-
-# ninja doesn't like "-lcblas" so using make.
-CMAKE_MAKEFILE_GENERATOR="emake"
-PYTHON_COMPAT=( python3_{9..11} )
-inherit cmake python-any-r1
-
-DESCRIPTION="Fast Library for Number Theory"
-HOMEPAGE="http://www.flintlib.org/"
-
-# flintlib.org tarballs have been broken in the past, Bill Hart suggests
-# we get them from Github (which he has control over).
-SRC_URI="https://github.com/wbhart/flint2/archive/refs/tags/v${PV}.tar.gz
-	-> ${P}.tar.gz"
-
-LICENSE="LGPL-2.1+"
-
-# Based off the soname, e.g. /usr/lib64/libflint.so -> libflint.so.15
-SLOT="0/16"
-
-KEYWORDS="~amd64 ~arm ~arm64 ~ppc ~riscv ~x86"
-IUSE="doc ntl test"
-
-RESTRICT="!test? ( test )"
-
-BDEPEND="doc? (
-	dev-python/sphinx
-	app-text/texlive-core
-	dev-texlive/texlive-latex
-	dev-texlive/texlive-latexextra
-	dev-tex/latexmk
-	)
-	${PYTHON_DEPS}"
-DEPEND="dev-libs/gmp:=
-	dev-libs/mpfr:=
-	ntl? ( dev-libs/ntl:= )
-	virtual/cblas"
-RDEPEND="${DEPEND}"
-
-S="${WORKDIR}/flint2-${PV}"
-
-src_prepare() {
-	# https://github.com/wbhart/flint2/issues/1140
-	rm test/t-sdiv_qrnnd.c || die
-	cmake_src_prepare
-}
-
-src_configure() {
-	local mycmakeargs=(
-		-DWITH_NTL="$(usex ntl)"
-		-DBUILD_TESTING="$(usex test)"
-		-DBUILD_DOCS="$(usex doc)"
-		-DCBLAS_INCLUDE_DIRS="${EPREFIX}/usr/include"
-		-DCBLAS_LIBRARIES="-lcblas"
-	)
-
-	cmake_src_configure
-
-	if use doc ; then
-		HTML_DOCS="${BUILD_DIR}/html/*"
-		DOCS=(
-			"${S}"/README
-			"${S}"/AUTHORS
-			"${S}"/NEWS
-			"${BUILD_DIR}"/latex/Flint.pdf
-		)
-	fi
-}
-
-src_compile() {
-	cmake_src_compile
-
-	if use doc ; then
-		cmake_build html
-		cmake_build pdf
-	fi
-}
diff --git a/sci-mathematics/singular/Manifest b/sci-mathematics/singular/Manifest
index c3f8e0bbe472..5ce4a554c402 100644
--- a/sci-mathematics/singular/Manifest
+++ b/sci-mathematics/singular/Manifest
@@ -1,6 +1,4 @@
 AUX 60singular-gentoo.el 298 BLAKE2B 5b42e2083037e2ff2ace5597ddebfb079920e09ed91d1a359e058fc654c6778456174d6cee9242f7fcaf81bf1464f47f43604b9e4eb298f051c6a4daba4630ca SHA512 4c17a25d91c085e12f26441fcde858e61bf191bd7d9dcf63ff5b5a1dce1d63e3f7c4f78ce8afa4f2359ad4ba6eb51f3e224ae6c502b18f5f7a76738534337431
-DIST singular-4.3.1p3.tar.gz 14991986 BLAKE2B 0ae2585a362839914d3a134bfe637f6faa34d95f58937f2adcca0c5a35e3218eb36554bae8187f5bb3a423dcac445c836e9bfff2d0d1a19d4e14a4452b84d839 SHA512 f092683f4a92158d82a2e694f284662c6285bac5faaa7d5e5695a84a220012fb8a733b4bbc52820def3037e1596ea4c2ab3846f58a3a3fb19e01bf7595790462
 DIST singular-4.3.2p1.tar.gz 15013729 BLAKE2B 00276f2417cd9e2b71afcae66c2aeb7f9d4f434f5a90deeee56dded66e6d5e0020ab0b06b6561e41f5b196262993732ffeb9196f59315f1b6a081b0029fc99a1 SHA512 451054a0bf33b9d1c94a63f0946e1eb7b3e7b92bc025b6aa4f64e65183aeebd6354bac5f87f6e8b35cb713b30e97af5c66f92f02683144bb426f5e3a828db616
-EBUILD singular-4.3.1_p3.ebuild 2299 BLAKE2B e0a759150b1b90984d6ad694bac432a7790aee00756fcb932284ed2ce01046949bfd8fbfb4cbde9ffb1194c2326b9fc7d0697b9ecb1decc0f6d232cdf388a599 SHA512 325672260a966c22be4bba06531e50ee6f1866789439e9a1ee17eefea2c48956eac2821447957dbf79a6b95d0f9268dbdf900f60ab783f9727863ed4a9a1a9a4
 EBUILD singular-4.3.2_p1.ebuild 2375 BLAKE2B 7d0dcc306784361e9bf61236de6863db463de429fde5f954abf4223352409b6da3c32d6f800a197c2e84d0ba5698fdd10d805bd40daece0db701babb5c41b237 SHA512 95a143214cf28dbcf041bd1fd74d8770bd1452ff01bf5f19ddc912de00c6a2fba51f177ac05e8ae9c71d4203a32490ff75c568bd5af6b6c1610093c8d128c29e
 MISC metadata.xml 862 BLAKE2B a6e991149cb925158806177b1b4a76da2b747b3273b395c14455993a99f4cf83de141980303a068b9068983b8adf4da884b81e80546a3d2dd162f188dc759385 SHA512 9e40cf7b3841bcf8289f24903e392df2a812b6d815f71da41d95a81bb89f493ab1afcef749ef47960ba683dc3433d2c4488015990806dde0b560ffe3bb6ca545
diff --git a/sci-mathematics/singular/singular-4.3.1_p3.ebuild b/sci-mathematics/singular/singular-4.3.1_p3.ebuild
deleted file mode 100644
index 5bb8ebd002a2..000000000000
--- a/sci-mathematics/singular/singular-4.3.1_p3.ebuild
+++ /dev/null
@@ -1,103 +0,0 @@
-# Copyright 1999-2023 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=8
-
-inherit elisp-common
-
-MY_PN=Singular
-MY_PV=$(ver_rs 3 '')
-# Consistency is different...
-MY_DIR2=$(ver_cut 1-3 ${PV})
-MY_DIR=$(ver_rs 1- '-' ${MY_DIR2})
-
-DESCRIPTION="Computer algebra system for polynomial computations"
-HOMEPAGE="https://www.singular.uni-kl.de/ https://github.com/Singular/Singular"
-SRC_URI="https://www.singular.uni-kl.de/ftp/pub/Math/${MY_PN}/SOURCES/${MY_DIR}/${PN}-${MY_PV}.tar.gz"
-S="${WORKDIR}/${PN}-${MY_DIR2}"
-
-LICENSE="BSD GPL-2 GPL-3"
-SLOT="0"
-KEYWORDS="amd64 ~ppc ~riscv ~x86 ~x86-linux"
-IUSE="emacs examples polymake +readline static-libs"
-
-RDEPEND="
-	dev-lang/perl
-	dev-libs/gmp:0
-	dev-libs/ntl:=
-	sci-libs/cddlib
-	sci-mathematics/flint
-	emacs? ( >=app-editors/emacs-23.1:* )
-	polymake? ( sci-mathematics/polymake )
-	readline? ( sys-libs/readline )
-"
-DEPEND="${RDEPEND}"
-
-SITEFILE=60${PN}-gentoo.el
-
-src_configure() {
-	local myconf=(
-		--disable-debug
-		--disable-doc
-		--disable-optimizationflags
-		--disable-pyobject-module
-		--disable-python
-		--disable-python-module
-		--disable-python_module
-		--enable-factory
-		--enable-gfanlib
-		--enable-libfac
-		--with-flint
-		--with-gmp
-		--with-libparse
-		--with-ntl
-		--without-python
-		--without-pythonmodule
-		$(use_enable emacs)
-		$(use_enable polymake polymake-module)
-		$(use_enable static-libs static)
-		$(use_with readline)
-	)
-	econf "${myconf[@]}"
-}
-
-src_compile() {
-	default
-
-	if use emacs; then
-		pushd "${S}"/emacs
-		elisp-compile *.el || die "elisp-compile failed"
-		popd
-	fi
-}
-
-src_install() {
-	# Do not compress singular's info file (singular.hlp)
-	# some consumer of that file do not know how to deal with compression
-	docompress -x /usr/share/info
-
-	default
-
-	dosym Singular /usr/bin/"${PN}"
-
-	# purge .la file
-	find "${ED}" -name '*.la' -delete || die
-}
-
-src_test() {
-	# SINGULAR_PROCS_DIR need to be set to "" otherwise plugins from
-	# an already installed version of singular may be used and cause segfault
-	# See https://github.com/Singular/Sources/issues/980
-	SINGULAR_PROCS_DIR="" emake check
-}
-
-pkg_postinst() {
-	einfo "Additional functionality can be enabled by installing"
-	einfo "sci-mathematics/4ti2"
-
-	use emacs && elisp-site-regen
-}
-
-pkg_postrm() {
-	use emacs && elisp-site-regen
-}
diff --git a/sci-mathematics/why3/Manifest b/sci-mathematics/why3/Manifest
index 8f5ec61729f4..ed5979c08b8f 100644
--- a/sci-mathematics/why3/Manifest
+++ b/sci-mathematics/why3/Manifest
@@ -1,7 +1,3 @@
-DIST why3-1.4.1.tar.gz 6305011 BLAKE2B 2d916fbf333550f8021bff9e7ccf4ca5685763ca7f82ae133298feaf96f3e8b36290a103fd27224fb6fb2dc36c8d7ad5d93ffc92e8cf7fe1a61abb5a40aecb39 SHA512 7990519179c088be1bc9b5b6d469f6d6fbd683445e20cbf5edd5c97682f2931b2657a92b60e539d7647033bfdc5a63401f28af61fd9b14b41011144afa2016e0
-DIST why3-1.5.1.tar.gz 6727576 BLAKE2B db88dc011856bc779a917613adb20c14744f5491aba54e424909106a1133362ddf9eb22e4a05660cb3153bfddfa54c488e1f9df046e3c413732924e127975e82 SHA512 1452a21ea9191f57debcc082afe458aec503d6aa24f8bc83f734041cdd302c4f166c9c4fe5f9ec25369b6e83011bdd7b485d67b092efa71ff0c1b39447f4bdac
 DIST why3-1.6.0.tar.gz 6850062 BLAKE2B 91db6f67a9d0fe24b7d7d18e6c5e9cd362563a55702bfb28c478754f53e831beb3033adde251214facd8d64ab923389b0b9fe7b240b6cd09f0b4b3e6f8eca143 SHA512 60d61b8337ab9f2fd2e6c7174eb0bab063f122417738cd75990c5c53120dd535bcedccb670567f5753853d6bc9f8efebb563d079e4d368372a7687193f1346b1
-EBUILD why3-1.4.1-r1.ebuild 2158 BLAKE2B 6702941175fd4768951603bbeaa095a2e2cdc2181d8ac1f7cb3eb54269852510082ec35b26eafda6422d5b2f4ded36589d28010879b23a64868ad0b92297d44d SHA512 2baf6a0d90dd277922338645567dfe28a5eb159fc90e7991430b185171be5cf6cf1404cfd336c93b1ede56c4adda83268daab01b47f66961ad60da8b2f7cc19b
-EBUILD why3-1.5.1.ebuild 2340 BLAKE2B fb1e703be2a938d0b77eb7c3e32f4ee6a098df12dc933a7731697674e63e9f1878c0e87fd78f941e54002f97083fb7f8f9e100e40194e6deb41524b0ae358353 SHA512 a87f050be498502b7ff0b02948e37e1228cdba179aa7bf7908133af6c5c7123da3bf8be1c14b550ca0ff61fe745b5869d8b30c726cf2cad538230a09a381057d
 EBUILD why3-1.6.0.ebuild 2348 BLAKE2B 0b8f27f14bb7d2117a9f5f6451d12e57ae3123ac6f491c653fb762bdf2410b5af17f9f3d7c2655c56f6a2f3f198aad07411a7c07e4943e62e1673b66e4779e41 SHA512 7a4ff6be794f77a6a319ee5e39e0bb3c80c82777d45da510d54ab6ac1793c0d249ebf10516c4db4ad7bf27441a0ef37171c43c04295ae0bd757f34619ac6fd61
 MISC metadata.xml 1902 BLAKE2B 1868834e446b471f4b3f7b11fc987661dee83790110fa31c73f0060fd8340891ff85ec16591d1326977760c726ec04bd06a4cca46fb1a87f792340a002cba247 SHA512 4dc9408d44eafc037bfce9c996570e58c161e07c3ded2a052954c834fcf8c3a36cf8429493bc705ced7445d199eaf207cabb5df1b0ed6b625015af518e55d9e9
diff --git a/sci-mathematics/why3/why3-1.4.1-r1.ebuild b/sci-mathematics/why3/why3-1.4.1-r1.ebuild
deleted file mode 100644
index 6d1e01d9863c..000000000000
--- a/sci-mathematics/why3/why3-1.4.1-r1.ebuild
+++ /dev/null
@@ -1,98 +0,0 @@
-# Copyright 1999-2022 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=7
-
-inherit autotools findlib
-
-DESCRIPTION="Platform for deductive program verification"
-HOMEPAGE="https://why3.lri.fr/"
-SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz"
-
-LICENSE="LGPL-2"
-SLOT="0/${PV}"
-KEYWORDS="~amd64"
-IUSE="coq doc emacs gtk +ocamlopt re sexp +zarith zip"
-
-RDEPEND="
-	!sci-mathematics/why3-for-spark
-	>=dev-lang/ocaml-4.05.0:=[ocamlopt?]
-	>=dev-ml/menhir-20170418:=
-	dev-ml/num:=
-	coq? ( >=sci-mathematics/coq-8.6 )
-	emacs? ( app-editors/emacs:* )
-	gtk? ( dev-ml/lablgtk:=[sourceview,ocamlopt?] )
-	re? ( dev-ml/re:= )
-	sexp? (
-		dev-ml/ppx_deriving:=[ocamlopt?]
-		dev-ml/ppx_sexp_conv:=[ocamlopt?]
-		dev-ml/sexplib:=[ocamlopt?]
-	)
-	zarith? ( dev-ml/zarith:= )
-	zip? ( dev-ml/camlzip:= )
-"
-DEPEND="${RDEPEND}"
-BDEPEND="
-	doc? (
-		dev-python/sphinx
-		dev-python/sphinxcontrib-bibtex
-		media-gfx/graphviz
-		dev-texlive/texlive-latex
-		dev-texlive/texlive-fontsrecommended
-		dev-texlive/texlive-latexextra
-	)
-"
-
-DOCS=( CHANGES.md README.md )
-
-src_prepare() {
-	mv configure.in configure.ac || die
-	sed -i 's/configure\.in/configure.ac/g' Makefile.in || die
-	sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \
-		-e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \
-		-e '/\$(SPHINX)/s/ -d doc\/\.doctrees / /' \
-		-i Makefile.in || die
-
-	eautoreconf
-	default
-}
-
-src_configure() {
-	local myconf=(
-		--disable-hypothesis-selection
-		--disable-pvs-libs
-		--disable-isabelle-libs
-		--disable-frama-c
-		--disable-infer
-		--disable-web-ide
-		$(use_enable coq coq-libs)
-		$(use_enable doc)
-		$(use_enable emacs emacs-compilation)
-		$(use_enable gtk ide)
-		$(use_enable ocamlopt native-code)
-		$(use_enable re)
-		$(use_enable sexp pp-sexp)
-		$(use_enable zarith)
-		$(use_enable zip)
-	)
-	econf "${myconf[@]}"
-}
-
-src_compile() {
-	emake
-	emake plugins
-	use doc && emake doc
-}
-
-src_install(){
-	findlib_src_preinst
-	emake install install-lib DESTDIR="${ED}"
-
-	einstalldocs
-	docompress -x /usr/share/doc/${PF}/examples
-	dodoc -r examples
-	if use doc; then
-		dodoc doc/latex/manual.pdf
-		dodoc -r doc/html
-	fi
-}
diff --git a/sci-mathematics/why3/why3-1.5.1.ebuild b/sci-mathematics/why3/why3-1.5.1.ebuild
deleted file mode 100644
index 46885e778d78..000000000000
--- a/sci-mathematics/why3/why3-1.5.1.ebuild
+++ /dev/null
@@ -1,103 +0,0 @@
-# Copyright 1999-2022 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=8
-
-inherit autotools findlib
-
-DESCRIPTION="Platform for deductive program verification"
-HOMEPAGE="https://why3.lri.fr/"
-SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz"
-
-LICENSE="LGPL-2"
-SLOT="0/${PV}"
-KEYWORDS="~amd64"
-IUSE="coq doc emacs gtk +ocamlopt re sexp stackify +zarith zip"
-
-RDEPEND="
-	!sci-mathematics/why3-for-spark
-	>=dev-lang/ocaml-4.05.0:=[ocamlopt?]
-	>=dev-ml/menhir-20170418:=
-	dev-ml/num:=
-	coq? ( >=sci-mathematics/coq-8.7 )
-	emacs? ( app-editors/emacs:* )
-	gtk? ( dev-ml/lablgtk:=[sourceview,ocamlopt?] )
-	re? ( dev-ml/re:= )
-	sexp? (
-		dev-ml/ppx_deriving:=[ocamlopt?]
-		dev-ml/ppx_sexp_conv:=[ocamlopt?]
-		dev-ml/sexplib:=[ocamlopt?]
-	)
-	stackify? ( dev-ml/ocamlgraph:=[ocamlopt?] )
-	zarith? ( dev-ml/zarith:= )
-	zip? ( dev-ml/camlzip:= )
-"
-DEPEND="${RDEPEND}"
-BDEPEND="
-	doc? (
-		dev-python/sphinx
-		dev-python/sphinxcontrib-bibtex
-		media-gfx/graphviz
-		dev-texlive/texlive-latex
-		dev-texlive/texlive-fontsrecommended
-		dev-texlive/texlive-latexextra
-	)
-"
-
-DOCS=( CHANGES.md README.md )
-
-src_prepare() {
-	mv configure.in configure.ac || die
-	sed -i 's/configure\.in/configure.ac/g' Makefile.in || die
-	sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \
-		-e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \
-		-e '/\$(SPHINX)/s/ -d doc\/\.doctrees / /' \
-		-i Makefile.in || die
-
-	# remove QA warning about duplicated compressed file:
-	rm examples/mlcfg/basic/why3shapes.gz || die
-
-	eautoreconf
-	default
-}
-
-src_configure() {
-	local myconf=(
-		--disable-hypothesis-selection
-		--disable-pvs-libs
-		--disable-isabelle-libs
-		--disable-frama-c
-		--disable-infer
-		--disable-web-ide
-		$(use_enable coq coq-libs)
-		$(use_enable doc)
-		$(use_enable emacs emacs-compilation)
-		$(use_enable gtk ide)
-		$(use_enable ocamlopt native-code)
-		$(use_enable re)
-		$(use_enable sexp pp-sexp)
-		$(use_enable stackify)
-		$(use_enable zarith)
-		$(use_enable zip)
-	)
-	econf "${myconf[@]}"
-}
-
-src_compile() {
-	emake
-	emake plugins
-	use doc && emake doc
-}
-
-src_install(){
-	findlib_src_preinst
-	emake install install-lib DESTDIR="${ED}"
-
-	einstalldocs
-	docompress -x /usr/share/doc/${PF}/examples
-	dodoc -r examples
-	if use doc; then
-		dodoc doc/latex/manual.pdf
-		dodoc -r doc/html
-	fi
-}