11 files changed, 127 insertions, 156 deletions
diff --git a/sci-mathematics/Manifest.gz b/sci-mathematics/Manifest.gz
index 59af5bf92019..12be58c9fa65 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 cb92d93affa5..0a010a8bcbe5 100644
--- a/sci-mathematics/coq-mathcomp/Manifest
+++ b/sci-mathematics/coq-mathcomp/Manifest
@@ -1,5 +1,5 @@
-DIST coq-mathcomp-1.16.0.tar.gz 1377232 BLAKE2B f9246ff2a6e583facc31278728b0865fdfb4d9cb6422687643321712b22d7fa61e40dd95e7782ba8443f66b61f9f6a82caead767a6985c87e6fe731a04494713 SHA512 80dc82e0deea4b3e05811b9dca3cf7c0169387288a5cc5c7e95c452c7aa041a37df34d93546c6597c6717106e20dc98400c7b0bbb8d1d1915e2063cfe6fd300b
 DIST coq-mathcomp-1.17.0.tar.gz 1384329 BLAKE2B e77b509c49796af7a23a4f286a83516e40e28bc03a1f3b20ddeb54321de05bc5f3ddbe0632e7462c6619180276975727b49101253b07cc9a2ae54a6662d8e5ab SHA512 06b318e2973863b5acefdd01b39065987a93952fa5f2ce9ba68df7ff7bf701c5fc82b571f53e80eadaa293935a82e8d1f891cc555db7200a923ee986918a0c76
-EBUILD coq-mathcomp-1.16.0-r1.ebuild 627 BLAKE2B 14853b4eedc1d123b7d5d16da9f16883a6c4e614d09ae3411c217e72a77f3b00719d48375c13708dbc264142aa8e50270251365a97c80d09487851a41d2b8d58 SHA512 9beef42e82af16d3e006cdd9062dafbcfdbd37260f0048413fe4632b624280d153e2cc6dbf8d5edae220f2ce778bf5d524ca9b6561857982da980791d28a0544
+DIST coq-mathcomp-1.19.0.tar.gz 1407548 BLAKE2B 733d537736a19a3667a51bbfe0b0c09838670761d8dd33853bfa3f320e29b71ec5703ed7ed752823c3696e7fad97443adb20a56e39fc9ec92b2ef5ae3d41a400 SHA512 ca2a24679418e551b6c9caee9799b2773ea2fb9986adc01c8e98f078dacb70bac872531f8f91fcf57ac04d8484783fc12589ae50a078f6b38beeb01fba6adbba
 EBUILD coq-mathcomp-1.17.0.ebuild 627 BLAKE2B e022b6e2552b0a307ebe83e7d3861c0f45cbe1bbd3c69bc18a3bea71680aa74922bb20624e67bca89040ec72f51f9aeb90c2175d35b6e8fb3f54015c5986dff6 SHA512 50887be2fccf1aac5a224877c4b562d94ce41a0f1c35754968728a49f62a69b5d041366d7edd266d42d1ebf03080234f3f25a35725865f560a335a35442f8fc9
+EBUILD coq-mathcomp-1.19.0.ebuild 627 BLAKE2B a511adb713b52a1c268662e816917e1273769d53250172236c8914507a828a30d17d62bc30f9a94edf91f3dfe01d8e30e1911f49ce2d5585a5cad5047bd07f7e SHA512 2a7b76c304e15ab62481dd2a7538afaef60fb76fca28b6121eac228dff1269ad4cac68695dc77810b910cd1153a59cdb3978a5d52df32e4b91b3481e87b4cb17
 MISC metadata.xml 511 BLAKE2B 3936f96cbf938fb9de97b080566d7fdde222d7dd303ccf842c76e7bd113b31c05136aea043c354bbd2ac6d4f61e2cba4e738f9f325059d36b7bae4feaed1ae89 SHA512 af2a4cfded0990d95e0a4b77ba69aebea09dee075f9eb4023b14c4788cd4118a78b3b5a4349fed11fff347061ab4bf59a4c63c8f43b22f8513054f1b3817af2f
diff --git a/sci-mathematics/coq-mathcomp/coq-mathcomp-1.16.0-r1.ebuild b/sci-mathematics/coq-mathcomp/coq-mathcomp-1.19.0.ebuild
index f90ad15beb45..9e92c79ab419 100644
--- a/sci-mathematics/coq-mathcomp/coq-mathcomp-1.16.0-r1.ebuild
+++ b/sci-mathematics/coq-mathcomp/coq-mathcomp-1.19.0.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2023 Gentoo Authors
+# Copyright 1999-2024 Gentoo Authors
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=8
@@ -9,7 +9,7 @@ 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
+S="${WORKDIR}/math-comp-mathcomp-${PV}/mathcomp"
 
 LICENSE="CeCILL-B"
 SLOT="0/${PV}"
diff --git a/sci-mathematics/coq-serapi/Manifest b/sci-mathematics/coq-serapi/Manifest
index 3f537fee033f..38e2d4a2e925 100644
--- a/sci-mathematics/coq-serapi/Manifest
+++ b/sci-mathematics/coq-serapi/Manifest
@@ -1,7 +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.17.0.tar.gz 273903 BLAKE2B 155d865650f773d71e0ddd10869852916de5e539b3b3f4d03d58259790482be45d668035975d5be768776f7ef5947f0d7227f0f6624bc7f64cefd009e9a83ecb SHA512 d9085b4215c233c47f78386d8771348768c9cbbf0716dfa4da3ff8c8c96d2e78b203098314175ef2bb9959096f8b0ec03a9fb5d696d0451eeee0713bd48afa2b
 DIST coq-serapi-0.18.1.tar.gz 275040 BLAKE2B 9224505da004ff54c3d21c394e6049b5e15b91c3531cd0d80aae89ee6ce9e92bb626a43fdef8fad58fea4d017b3ed3f13d5d1735e7cfc1ae3bcebed2c70ce332 SHA512 a8eca10734a5b1aa5c6a890998f18d673050ca1e975b5e88643176bfd627b4c0d05cf0be1b75ccfd155b9e74f357ee61bf8225fd144b6a624a3bdd359396428c
-EBUILD coq-serapi-0.17.0.ebuild 1488 BLAKE2B 00bb0f1f7e3fdd53fbe77847638647a7aabc3f50da29bad4c684bf753b6f154116c44502e7d173b5cd5783b3ab7482aed71acd9f51c9529e105b799c80b94b22 SHA512 dde7170b0334dcd5298aa1f6a629c77b2fcc6de5d3f2d92bc23d36c068878a9b19415340138e26c7c5b8db1e3c7b7733f419e0d9162fb8548325960f12a5f163
 EBUILD coq-serapi-0.18.1.ebuild 1494 BLAKE2B 75d3ef68924782674d04ec8aacd8426a6d9715b868d1288ce71c6550aeb98b212c98ef4c454964c9f2031c5016eddca1cedb43fb9695a97bfbd250ef97126113 SHA512 252dd29a108ce468badff4beb35ac2697fa4eb7480184a37316eb4561f5c4330c023d0f95e5f384a98c612cb826a320c4b2bd1a21480d9728f168585c76e6b31
 MISC metadata.xml 935 BLAKE2B e1444df414ce499df466597f5e0949e8ebf2d6da23d77028546324109659f58c5f0284a315ea062410a2f2e4631aac8d3564664719e89d76ad6ded9bb8ba7a5f SHA512 172fedbb2aa42e2be9aff426d64fcd69d2dfa206bb0e6072c6ecdc14a1923a2f0676303d8d8aebfe9a3e96e0a1e89185d2d4952bdb9ba1fff44b3891f26d6bf7
diff --git a/sci-mathematics/coq-serapi/coq-serapi-0.17.0.ebuild b/sci-mathematics/coq-serapi/coq-serapi-0.17.0.ebuild
deleted file mode 100644
index 2485ac135a10..000000000000
--- a/sci-mathematics/coq-serapi/coq-serapi-0.17.0.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.17.0
-COQ_MAX_V=8.18.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/eprover/Manifest b/sci-mathematics/eprover/Manifest
index f8bc6843e9d2..d8d517a4c560 100644
--- a/sci-mathematics/eprover/Manifest
+++ b/sci-mathematics/eprover/Manifest
@@ -1,3 +1,5 @@
+DIST eprover-3.0.03.tar.gz 1523036 BLAKE2B fc58b4f99b4fcd8ef4b0704c6fb65e7ef235582d8e2cdef17fd178ec51b7655459dbbf9d0d20ef00edf15f893aefdd4dd07c7fe402e42a5378b4bf241af6c806 SHA512 3adce986eb0d6d6b8373b10d8104ca2a68c72c92cd5c8cb7416044b1ae67daa0b8da82c13e85129d0699217b26a98df15768a5b0dca927ab26920a26dbba9662
 DIST eprover-3.0_pre008.tar.gz 1512310 BLAKE2B 88533bd05b823155639df49d631f4fb339019f624ea6cb1c3c7c46f1db331183dac4285c70a7efa372cbf3f0e839ec41b7589b93e4599a6ed94f42734f361985 SHA512 81f1a1dfd77b685805c80f95b683489d8759acbb5b45ebaf123f1b0f7cb82f9e2d58731975e5286afa9a8bf9d2874cc5362edc0c0da92aea39830ac4b8b1c4ec
+EBUILD eprover-3.0.03.ebuild 1583 BLAKE2B 901b5e279a4394fa9f53e1b0c33867a741532576a862cb691182a9be4dc1cc360c5664d4ca0ab60f6969a45d7d31ba77ab60a57ca70bc576fcdf1ef85b927c3c SHA512 8faeb8033d341adeb2f6e93b3c47c36c79706c19d9e0e93bb52ffb1bc461765d31b916bfe4e8dc9b0c75f5e7d2312d1d98e6cc3ecaf6f9ce13239a485eff2db5
 EBUILD eprover-3.0_pre008.ebuild 1513 BLAKE2B 61b58f4bd5eb1a29a79c342a5b1d30c28a0de907005f9d039fec9e42c91fa5d6a7d429743a00b9075412bdb8464b3bd1bfd2e5305553542a50d7a2070a36f496 SHA512 ffe77b4d6160f63628d82b813bf331107292335d14b5cbe41489d3ff74aa2b3fa3894f20d33fb098c0259f7807876d39dd2810b9af200604fc56f19b0e711b63
 MISC metadata.xml 1534 BLAKE2B f53ad8e4eeccf361718ecbe735f72fbb0645478dd5a3c7b1e6baab718c1a15e9852c11d0074181b48b2402065b090fe95ba65cdc6bed4e84ff6e59aa6174446b SHA512 08caa0f223c5aa25935cba3cf12e11af77e59fc364b26a1aab9d622500245cd7a650143b1fe14bc3dc377e40f6b3018048c567dff40557e70738618a205e9743
diff --git a/sci-mathematics/eprover/eprover-3.0.03.ebuild b/sci-mathematics/eprover/eprover-3.0.03.ebuild
new file mode 100644
index 000000000000..ef6b9196aa7d
--- /dev/null
+++ b/sci-mathematics/eprover/eprover-3.0.03.ebuild
@@ -0,0 +1,76 @@
+# Copyright 1999-2024 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+inherit toolchain-funcs
+
+DESCRIPTION="Automated theorem prover for full first-order logic with equality"
+HOMEPAGE="https://www.eprover.org/
+	https://github.com/eprover/eprover/"
+
+if [[ "${PV}" == *9999* ]] ; then
+	inherit git-r3
+
+	EGIT_REPO_URI="https://github.com/eprover/${PN}.git"
+else
+	SRC_URI="https://github.com/eprover/${PN}/archive/E-${PV/_/}.tar.gz
+		-> ${P}.tar.gz"
+	S="${WORKDIR}/${PN}-E-${PV/_/}"
+
+	KEYWORDS="~amd64 ~x86"
+fi
+
+LICENSE="GPL-2+"
+SLOT="0"
+IUSE="+ho"
+
+BDEPEND="
+	sys-apps/help2man
+"
+
+src_prepare() {
+	default
+
+	sed -e "/^OPTFLAGS/s|= .*|= ${CFLAGS}|"			\
+		-e "/^LD/s|= .*|= $(tc-getCC) ${LDFLAGS}|"	\
+		-e "/^   AR/s|ar|$(tc-getAR)|"				\
+		-e "/^   CC/s|gcc|$(tc-getCC)|"				\
+		-i "${S}/Makefile.vars" || die
+
+	sed -e "s|ar rc|$(tc-getAR) rc|g"						\
+		-e "s|ranlib|$(tc-getRANLIB)|g"						\
+		-i "${S}/CONTRIB/picosat-965/makefile.in" || die
+}
+
+src_configure() {
+	local -a myconf=(
+		$(usex ho '--enable-ho' '')
+		--bindir=/usr/bin
+		--exec-prefix=/usr
+		--man-prefix=/usr/share/man/man1
+	)
+	sh ./configure "${myconf[@]}" || die
+}
+
+src_compile() {
+	default
+
+	if use ho ; then
+		ln -s "${S}/PROVER/${PN}-ho" "${S}/PROVER/${PN}" || die
+	fi
+
+	emake man
+}
+
+src_install() {
+	# Picosat (CONTRIB package) is available as separate package.
+	rm -r "${S}/CONTRIB" || die
+
+	emake EXECPATH="${ED}/usr/bin" MANPATH="${ED}/usr/share/man/man1" install
+	dodoc -r DOC EXAMPLE_PROBLEMS
+
+	if use ho ; then
+		dosym -r "/usr/bin/${PN}-ho" "/usr/bin/${PN}"
+	fi
+}
diff --git a/sci-mathematics/gappa/Manifest b/sci-mathematics/gappa/Manifest
index cca8a6a88b2a..0cb0e00606ea 100644
--- a/sci-mathematics/gappa/Manifest
+++ b/sci-mathematics/gappa/Manifest
@@ -1,3 +1,5 @@
 DIST gappa-1.4.1.tar.gz 388314 BLAKE2B 08bc38745fd33a892ef288315bb4eac730c96ddb379ec4689385b63a9f1f74a662bc303f8323bf3941875b6d38e988fe4114e0db84994a7e7a5858b178cc0026 SHA512 bae9788fdce92b04b011b9de207a1234215cbb68c8bd0a60d925fa5fb5e1cad014d60ed8b45d84e8fabd6b54a870a70af6dd24dd68f4dbb2e129f83dcf88fa11
+DIST gappa-1.4.2.tar.gz 395447 BLAKE2B 55d5e8a6376c3cce00fdf04c7e661ee14f5c04d883b445d1ff76e4ad8147a1d61fcbdd9685a882cfe7265841d4af90e21e1a315cf5ebdc656fd35f933b27c0f5 SHA512 aec04da1a478ecc876794b06a92a56ceb76ae2b1edd0da2a18cb509b3ae6f81437fe73777b7b05ef129edd8754528330f3f3a4713713c70934af3a6bdac4c7e5
 EBUILD gappa-1.4.1.ebuild 815 BLAKE2B 3c1549f5e47b6a322aabb9176acb61720709a69e28536623fab8c4bea6ab6fa62d5f1d6971eb8998fc1eb920bd6591d195ed5a09867086b8ac4aff84a44fb551 SHA512 73f07724979bb6272384fb519ebc37b11b733605dcbba3ee9389c3532865e3256010ff6f8b83726408194ba8430da0fa47383de5a0e75c7aa015ea52f40d832c
+EBUILD gappa-1.4.2.ebuild 815 BLAKE2B 943401765e74cedfb8d3b04ea5046135f6122beb217fcd60f8a164779a2daed6d1e206075a5bfb04d2a97f123ca547810515311a1afde38da2480fd939577161 SHA512 9e55451394f20c2c4e4b42cb60926e07f9c9a991a5a884fa4e41462987bc803d6c4a3b910c8d1e9d36f4afe2d6203dca301657f867f3f2551e2ba16856d4b8b9
 MISC metadata.xml 706 BLAKE2B 681b7e1a45b2b64fbcccf58bdb00ee058949ddc915fe056afa6e9aee12d6938b8740115c5431eb44415d0e46121d3543f7f8e8795b4112c64740e1ca806d079c SHA512 f93cc2afb547fd838215a22dc1dff148217927caef6f315716bdb0d7def9ddfa6026b1c7976d519ac4717ad0b70b58afcd8fbbfe42635c0bb1b2e608b5f95c62
diff --git a/sci-mathematics/gappa/gappa-1.4.2.ebuild b/sci-mathematics/gappa/gappa-1.4.2.ebuild
new file mode 100644
index 000000000000..7a69fe2ea262
--- /dev/null
+++ b/sci-mathematics/gappa/gappa-1.4.2.ebuild
@@ -0,0 +1,43 @@
+# Copyright 1999-2024 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+DOCS_BUILDER=doxygen
+DOCS_DIR=doc/doxygen
+
+inherit docs multiprocessing
+
+DESCRIPTION="Tool for verifying floating-point or fixed-point arithmetic"
+HOMEPAGE="https://gappa.gitlabpages.inria.fr/
+	https://gitlab.inria.fr/gappa/gappa/"
+SRC_URI="https://gappa.gitlabpages.inria.fr/releases/${P}.tar.gz"
+
+LICENSE="CeCILL-2 GPL-3+"
+SLOT="0"
+KEYWORDS="~amd64 ~x86"
+
+RDEPEND="
+	dev-libs/boost:=
+	dev-libs/gmp:0=
+	dev-libs/mpfr:0=
+"
+DEPEND="${RDEPEND}"
+
+DOCS=( AUTHORS INSTALL.md NEWS.md README.md )
+
+src_compile() {
+	./remake --jobs=$(makeopts_jobs) || die
+
+	docs_compile
+}
+
+src_test() {
+	./remake --jobs=$(makeopts_jobs) check || die
+}
+
+src_install() {
+	DESTDIR="${D}" ./remake install || die
+
+	einstalldocs
+}
diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 6a973396835d..70ad06adf01e 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -2,8 +2,6 @@ AUX lean-3.50.3-gcc-13.patch 263 BLAKE2B cf589616f4612319bbe1d21e798787a72da3d0f
 AUX lean-CMakeLists-fix_flags.patch 1285 BLAKE2B 0507e553c1acf2a53c5267932127117d5ae5ba9015a08c88748b3d82c041f8d904d15cd033dd7934ac55c474fa75a5d4a46f680cc887fee37c05c3f5f3832839 SHA512 11a5918847e45aac7bf79e48d8f881ef5cd3e6b09dbb0979f3f0b88fd36458be21ebeb530158da801399a0cdc8fe382444ff338cd793cd9f1bfced90c5d5a71b
 DIST lean-3.51.1.tar.gz 1918894 BLAKE2B 9a240fe73193794a57001582c0623052cfc1c08ef3b155cac2d9dfc029202cb79b85e844fdf068e454498a35522ec3e18330da8c644bba3c6f708cbde04816f7 SHA512 dccdf6c3fbcd98115e62b9944645af6a2ce21412d63baa9565871807862e8d83cc6f29d1fb687f19b802240a5f9c019443caa00412ecfabe621744dff900e3ee
 DIST lean-4.2.0.tar.gz 16382466 BLAKE2B 3a8770d92ae89041f3e12089c3bb9171a993e8a1c702162925b569e13ed8d8819b3e9aa3c00e314a80a118ff8e4b18fb6df8b8a0e85a21fcb1daa5c0bfc29d4f SHA512 b0bd91f39319c1c6fd6851732d9dcb8758734500abc8faf0648c03582a81d51f2d942fa5deecedf81116b894d0b65e93eccab557bf155e69d65bda83eccaf7bb
-DIST lean-4.2.0_rc4.tar.gz 16386559 BLAKE2B 4eb0bb47cd09ec7ccb04870a08b13c8b9c73a296b42e9c92c9f9885dfe416e75352db7c41725446dd27a0a9a68f3979fa91dadb93aba1af1321df94312d7fa99 SHA512 4d08bf182eb3822f12ec69af9aa0527581fe7f3ff4a10836b866622146b3572ced3635fdf0179a8764d233de427094f47219d619d205971794b41f1c1fc4b06d
 EBUILD lean-3.51.1.ebuild 1815 BLAKE2B 767ff4cc188049e3b54d903ff3a314012997369beadf7335a33e01193b0da69707e4b845946afde25a617e9e344df479adb70c8937e84dc1854fe2db9b0d979b SHA512 630f5690c1a4321e56d640186b894623fa5551de17af21793b4a66c32ccfb66697b4144ada36742262e5bd037d094b0448511433e73affdac36ad7e06874635d
 EBUILD lean-4.2.0.ebuild 1320 BLAKE2B 14ea248c9a6f0170f8abfca47ce379a6c48c6a2e216cfa8ef0e0ce259eeafad3ce68ca1bec290ddd521b24bb0797d3158dc3596c495a6ce728fbc88b86c95ffc SHA512 f3af28b8f952d86180af364a0f3eb611761a1573b3d41e18a6921f83c826a41cd9d94dd603214f6b6a80b0e6ae119e90310b76deff8ea621b5912f023dfbfb15
-EBUILD lean-4.2.0_rc4.ebuild 1320 BLAKE2B 14ea248c9a6f0170f8abfca47ce379a6c48c6a2e216cfa8ef0e0ce259eeafad3ce68ca1bec290ddd521b24bb0797d3158dc3596c495a6ce728fbc88b86c95ffc SHA512 f3af28b8f952d86180af364a0f3eb611761a1573b3d41e18a6921f83c826a41cd9d94dd603214f6b6a80b0e6ae119e90310b76deff8ea621b5912f023dfbfb15
 MISC metadata.xml 606 BLAKE2B 6478d84a762a59082fdea0a11a95b27c093782228c48dba58dc490ea9ac2cecef54cc3101dc98e385f3a29f85d84af21b7d2ae1a9f089ee0313158ecb44eb0e7 SHA512 02d2ac07b155c7a04c857d397d476a39864d02b10dd81c5830db5e21eb86c6dcff26da552a04717f5f587b326ddf8e2e8d27f1a138f88b391f0199d8004d8cb7
diff --git a/sci-mathematics/lean/lean-4.2.0_rc4.ebuild b/sci-mathematics/lean/lean-4.2.0_rc4.ebuild
deleted file mode 100644
index 30fd5379373b..000000000000
--- a/sci-mathematics/lean/lean-4.2.0_rc4.ebuild
+++ /dev/null
@@ -1,78 +0,0 @@
-# Copyright 1999-2023 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=8
-
-MAJOR="$(ver_cut 1)"
-
-CMAKE_MAKEFILE_GENERATOR="emake"
-PYTHON_COMPAT=( python3_{10..12} )
-
-inherit cmake flag-o-matic python-any-r1
-
-DESCRIPTION="The Lean Theorem Prover"
-HOMEPAGE="https://leanprover-community.github.io/"
-
-if [[ "${PV}" == *9999* ]] ; then
-	inherit git-r3
-
-	EGIT_REPO_URI="https://github.com/leanprover/${PN}${MAJOR}.git"
-else
-	SRC_URI="https://github.com/leanprover/${PN}${MAJOR}/archive/refs/tags/v${PV/_/-}.tar.gz
-		-> ${P}.tar.gz"
-	S="${WORKDIR}/${PN}${MAJOR}-${PV/_/-}"
-
-	KEYWORDS="~amd64 ~x86"
-fi
-
-LICENSE="Apache-2.0"
-SLOT="0/${MAJOR}"
-IUSE="debug source"
-
-RDEPEND="
-	dev-libs/gmp:=
-"
-DEPEND="
-	${RDEPEND}
-"
-BDEPEND="
-	${PYTHON_DEPS}
-"
-
-pkg_setup() {
-	python-any-r1_pkg_setup
-}
-
-src_prepare() {
-	filter-lto
-
-	sed -e "s|-O[23]|${CFLAGS}|g" -i src/CMakeLists.txt || die
-
-	cmake_src_prepare
-}
-
-src_configure() {
-	local CMAKE_BUILD_TYPE
-
-	if use debug ; then
-		CMAKE_BUILD_TYPE="Debug"
-	else
-		CMAKE_BUILD_TYPE="Release"
-	fi
-
-	local -a mycmakeargs=(
-		-DLEAN_EXTRA_CXX_FLAGS="${CXXFLAGS}"
-		-DLEAN_EXTRA_LINKER_FLAGS="${LDFLAGS}"
-	)
-	cmake_src_configure
-}
-
-src_install() {
-	cmake_src_install
-
-	rm "${ED}/usr/LICENSE"* || die
-
-	if ! use source ; then
-		rm -r "${ED}/usr/src" || die
-	fi
-}