diff --git a/app-emacs/elixir-mode/Manifest b/app-emacs/elixir-mode/Manifest
index 83b2678f2f180..747c81efec34b 100644
--- a/app-emacs/elixir-mode/Manifest
+++ b/app-emacs/elixir-mode/Manifest
@@ -1,2 +1,2 @@
-DIST elixir-mode-2.3.2_p20220314.tar.gz 35711 BLAKE2B f4d712bce35f1056a2b2baf23077fff6204d572f215bf3afe31e26fc15691927afdbe880f942073e80dbe0ce3937dc619b24f89f821a6655f944a448db995744 SHA512 f4467459918db88408c2fa04fcb053fcdf2987c5907f0481034fa18bc3c7a805a7a01d071d7662f4d0db16aa02faa312f225b2b6f45587ccf06a616a1b6df485
 DIST elixir-mode-2.4.1.tar.gz 35948 BLAKE2B 0850da18c5897dce2c19fba5a41235c38b5f6841dcd08c3b9cd1a039d743c3c002f8066bdcb4484cfd99b63004329824d5f38321668aae3fa9d162a5145aac3e SHA512 df429d1cff45d9bcad0cd0d5cdd1776f1c419226881bacec1530750f0cb7418f14858af15176824cbc73916049ba091caaac486fce2c3f6d11ae9cb360ef6a87
+DIST elixir-mode-2.5.0.tar.gz 36761 BLAKE2B cf1157a7b47acc583595b7a80eb7c5717cb605d9188f0d38c41518d21a6eb5729eda5af81d889d11007a899a8e6f38c67d5dd950407c5a89a5290e68ceab3294 SHA512 dfd3d939ab5a46f70f782e8557d39c02d34d502ea43bb93aba754417d2c13c0c8e6743fb974aa2e2def3e29ab22d45a9015ce6e59b33b561387782d8fe0b1389
diff --git a/app-emacs/elixir-mode/elixir-mode-2.3.2_p20220314.ebuild b/app-emacs/elixir-mode/elixir-mode-2.5.0.ebuild
similarity index 57%
rename from app-emacs/elixir-mode/elixir-mode-2.3.2_p20220314.ebuild
rename to app-emacs/elixir-mode/elixir-mode-2.5.0.ebuild
index 0dbacc1193755..cc7f9f3b58193 100644
--- a/app-emacs/elixir-mode/elixir-mode-2.3.2_p20220314.ebuild
+++ b/app-emacs/elixir-mode/elixir-mode-2.5.0.ebuild
@@ -3,32 +3,35 @@
 
 EAPI=8
 
-COMMIT=e0d0466d83ec80ddb412bb1473908a21baad1ec3
-
 inherit elisp
 
 DESCRIPTION="Emacs major mode for editing Elixir files"
 HOMEPAGE="https://github.com/elixir-editors/emacs-elixir/"
-SRC_URI="https://github.com/elixir-editors/emacs-elixir/archive/${COMMIT}.tar.gz
-			-> ${P}.tar.gz"
-S="${WORKDIR}"/emacs-elixir-${COMMIT}
+
+if [[ ${PV} == *9999* ]] ; then
+	inherit git-r3
+	EGIT_REPO_URI="https://github.com/elixir-editors/emacs-elixir.git"
+else
+	SRC_URI="https://github.com/elixir-editors/emacs-elixir/archive/v${PV}.tar.gz
+		-> ${P}.tar.gz"
+	S="${WORKDIR}"/emacs-elixir-${PV}
+	KEYWORDS="~amd64 ~x86"
+fi
 
 LICENSE="GPL-2+"
-KEYWORDS="~amd64 ~x86"
 SLOT="0"
 IUSE="test"
 RESTRICT="!test? ( test )"
 
 BDEPEND="
-	test? (
-		app-emacs/ert-runner
-		dev-lang/elixir
-	)
+	test? ( dev-lang/elixir )
 "
 
 DOCS=( CHANGELOG.md README.md )
 SITEFILE="50${PN}-gentoo.el"
 
+elisp-enable-tests ert-runner
+
 src_test() {
 	ert-runner -L . -L tests --reporter ert+duration tests || die
 }
diff --git a/app-emacs/embark/embark-9999.ebuild b/app-emacs/embark/embark-9999.ebuild
new file mode 100644
index 0000000000000..38aa5db830445
--- /dev/null
+++ b/app-emacs/embark/embark-9999.ebuild
@@ -0,0 +1,50 @@
+# Copyright 1999-2023 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+NEED_EMACS=27.1
+
+inherit elisp optfeature
+
+DESCRIPTION="Conveniently act on minibuffer completions inside GNU Emacs"
+HOMEPAGE="https://github.com/oantolin/embark/"
+
+if [[ ${PV} == *9999* ]] ; then
+	inherit git-r3
+	EGIT_REPO_URI="https://github.com/oantolin/${PN}.git"
+else
+	SRC_URI="https://github.com/oantolin/${PN}/archive/${PV}.tar.gz
+		-> ${P}.tar.gz"
+	KEYWORDS="~amd64 ~x86"
+fi
+
+LICENSE="GPL-3+"
+SLOT="0"
+
+RDEPEND=">=app-emacs/compat-29.1.4.0"
+BDEPEND="${RDEPEND}"
+
+ELISP_REMOVE="avy-embark-collect.el embark-consult.el"
+
+DOCS=( README.org )
+SITEFILE="50${PN}-gentoo.el"
+
+src_compile() {
+	elisp_src_compile
+
+	elisp-make-autoload-file
+}
+
+src_install() {
+	elisp_src_install
+
+	doinfo ${PN}.texi
+}
+
+pkg_postinst() {
+	elisp_pkg_postinst
+
+	optfeature "Avy integration for Embark" app-emacs/avy-embark-collect
+	optfeature "Consult integration for Embark" app-emacs/embark-consult
+}
diff --git a/app-emacs/org-mode/Manifest b/app-emacs/org-mode/Manifest
index bc8c8a88afc79..3398cad58530f 100644
--- a/app-emacs/org-mode/Manifest
+++ b/app-emacs/org-mode/Manifest
@@ -1,6 +1,5 @@
 DIST org-9.4.6.tar.gz 4729335 BLAKE2B b88edaf8098124b2048ce57d6005d2af0de34e9b8fa94c24eb041a42a6fca1fd6da7f242be89e6b0ca5e7b80d879096f9114dca0ba86b20a5d26d2a185baa537 SHA512 7e50d7e9e2073bc0f06d2c861f59d4c9b8af4cf63c98f730c810a3a8721e65829fe9ef7ba0ac99f49bf9da427a4d5ad1d028e05c1a8ab6a3bea2ff2020c0e61d
 DIST org-mode-release_9.5.5.tar.gz 2049730 BLAKE2B 382e6585f693fd30def29da740d1329a52b4565382df90a37e3646324ee44106f1a99c2ea0c0862d77721cc9bfbec0736cb03065b59b2fdea0a68d8f8ea37c9a SHA512 ce06bab17ae7944c1623f935bbad0379d06390c72c43633ba0de2bc04ad362e18d9aaae96103eeaa23f7ea9e4e00976a97a914da87fb7941a13746b1fa77f591
-DIST org-mode-release_9.6.3.tar.gz 2208740 BLAKE2B 77d8e7de2230a3d4b5f3e85336519de1b2d55481522bedc206c5edb2cd56963f729d1e48fe483717fd4c295c6eb1b73e9335ab6a56c2903dd9ee54e15da0a8a0 SHA512 4a7040bab029c8384fa8689782672887baec7eea66ea99a32fd026eddb1659fa15e6c8ba99546fb7b8a16492d1fa476542acba3adef745079f583bd0e2b834e0
-DIST org-mode-release_9.6.4.tar.gz 2208733 BLAKE2B 4ac49b4af872750453dd29eb0fb7de75a140246defb98a1ee62b693fe5083b892eff32ffda6a87cdc4d22486c8246134bb7483e3ec335e23ee131e0f6894475d SHA512 fa117500e0618f20b55af6e7f3cee2d24bbcf396649fabc1420299d99599335c0697e865ac38e49a30d5f2cd00e6daf163f340364e51c306583a7198852df059
 DIST org-mode-release_9.6.5.tar.gz 2209154 BLAKE2B bce49c4cdf51550c83ad78b683e2cb400a4378ffa344e00201450fdbc403248b85ab7a69c64abb5edc45b64c7134bd286e4a7115c255c9f6ff4866425c303711 SHA512 89829a0ccd82a42ba4b612e3ee2208632a0b5d32419192ac47660f6e9ab05e9848a844b6625dab6426a27fc3009bf75925856574d0aab49fefe639b6f31cf2fc
 DIST org-mode-release_9.6.6.tar.gz 2209391 BLAKE2B fd88d0cf686007b7a4f90ad8870f614525efa2edcdf9198eb2576560e8a830ac69c05fe92d1080b191a0c10247669d2cc75306486a0c0ce1c9281ef56a779bd3 SHA512 a8e34bf6766204ac88ab3a0d2d20b5db911c66deef7b252e57691e7032cc0e34bee4d27b1fa4053d5b2011d08c9b1b1b556b5698109150d09018956095e42d5a
+DIST org-mode-release_9.6.7.tar.gz 2209900 BLAKE2B 5e0c63722cba9708018da8e79bfd63a3d632cd7ac27144833e2f816b26cd558dc249c0c8a6b9f78f5c68af1d9218d43fa2f4fab7ab86645215d0ba40cb3d3f12 SHA512 f8225eb3d488faef54d97c812964010fefc19003950fd5b49fc1618b8ff0deb9d001c631820d99439f7527aa72f9c071578484b3b7b8d3c46baa53a7066de2fc
diff --git a/app-emacs/org-mode/org-mode-9.6.4.ebuild b/app-emacs/org-mode/org-mode-9.6.4.ebuild
deleted file mode 100644
index 2747f4956985e..0000000000000
--- a/app-emacs/org-mode/org-mode-9.6.4.ebuild
+++ /dev/null
@@ -1,50 +0,0 @@
-# Copyright 1999-2023 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=8
-
-inherit elisp readme.gentoo-r1
-
-MY_P="${PN}-release_${PV}"
-DESCRIPTION="An Emacs mode for notes and project planning"
-HOMEPAGE="https://www.orgmode.org/"
-SRC_URI="https://git.savannah.gnu.org/cgit/emacs/${PN}.git/snapshot/${MY_P}.tar.gz"
-S="${WORKDIR}"/${MY_P}
-
-LICENSE="GPL-3+ FDL-1.3+ CC-BY-SA-3.0 odt-schema? ( OASIS-Open )"
-SLOT="0"
-KEYWORDS="amd64 ppc x86"
-IUSE="doc odt-schema"
-RESTRICT="test"
-
-BDEPEND="doc? ( virtual/texi2dvi )"
-
-SITEFILE="50${PN}-gentoo.el"
-
-src_compile() {
-	emake -j1 \
-		ORGVERSION=${PV} \
-		datadir="${EPREFIX}${SITEETC}/${PN}"
-	use doc && emake -j1 pdf card
-}
-
-src_install() {
-	emake \
-		ORGVERSION=${PV} \
-		DESTDIR="${D}" \
-		ETCDIRS="styles csl $(use odt-schema && echo schema)" \
-		lispdir="${EPREFIX}${SITELISP}/${PN}" \
-		datadir="${EPREFIX}${SITEETC}/${PN}" \
-		infodir="${EPREFIX}/usr/share/info" \
-		install
-
-	elisp-site-file-install "${FILESDIR}/${SITEFILE}"
-	dodoc README.org CONTRIBUTE.org etc/ORG-NEWS
-	use doc && dodoc doc/org.pdf doc/orgcard.pdf doc/orgguide.pdf
-
-	local DOC_CONTENTS="Org mode has a large variety of run-time dependencies,
-		so you may have to install one or more additional packages.
-		A non-exhaustive list of these dependencies may be found at
-		<http://orgmode.org/worg/org-dependencies.html>."
-	readme.gentoo_create_doc
-}
diff --git a/app-emacs/org-mode/org-mode-9.6.3.ebuild b/app-emacs/org-mode/org-mode-9.6.7.ebuild
similarity index 98%
rename from app-emacs/org-mode/org-mode-9.6.3.ebuild
rename to app-emacs/org-mode/org-mode-9.6.7.ebuild
index 2747f4956985e..77e4614e18c62 100644
--- a/app-emacs/org-mode/org-mode-9.6.3.ebuild
+++ b/app-emacs/org-mode/org-mode-9.6.7.ebuild
@@ -13,7 +13,7 @@ S="${WORKDIR}"/${MY_P}
 
 LICENSE="GPL-3+ FDL-1.3+ CC-BY-SA-3.0 odt-schema? ( OASIS-Open )"
 SLOT="0"
-KEYWORDS="amd64 ppc x86"
+KEYWORDS="~amd64 ~ppc ~x86"
 IUSE="doc odt-schema"
 RESTRICT="test"
 
diff --git a/dev-lang/elpi/Manifest b/dev-lang/elpi/Manifest
index 3c296b8fd485b..9adfe9320b38f 100644
--- a/dev-lang/elpi/Manifest
+++ b/dev-lang/elpi/Manifest
@@ -1 +1,2 @@
+DIST elpi-1.16.10.tar.gz 2606110 BLAKE2B f9d36c5b6ef9db0bcdca18ac163fd863a2c065d763fd070ab44617894c23b4717d430ae2792224e2c4b0bc639bf6f044fee44c5f763c7552d2f234b4f53113a4 SHA512 6e7fc2ac06e8df0fd1db42467909d77e7b61de386cb6c31ae5c278f316efea646d0e0ba1bfd4a98e65268a4c3ec78ea93c616d8855fe6359637401d83bd5fc0f
 DIST elpi-1.16.9.tar.gz 2601448 BLAKE2B 37dd239cae112e6ec1c913dc9fdba60d829c0bbf61876f9c98b927d5d359ed5376ea1663da7e6c808bd62d61380973de7ae649d4a0dddef172f8d2599cc18c35 SHA512 89896c0f5d2e9a8ec6d7ef666a0d11c12b670e6951e277c2d29095b3fcbb5a977416cd1876c4c2d8c14b826782b095d3a453db03bebe3438f0eeacc08c7c87fc
diff --git a/dev-lang/elpi/elpi-1.16.10.ebuild b/dev-lang/elpi/elpi-1.16.10.ebuild
new file mode 100644
index 0000000000000..184849b51e67d
--- /dev/null
+++ b/dev-lang/elpi/elpi-1.16.10.ebuild
@@ -0,0 +1,47 @@
+# Copyright 1999-2023 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+inherit dune
+
+DESCRIPTION="Embeddable Lambda Prolog Interpreter in OCaml"
+HOMEPAGE="https://github.com/LPCIC/elpi/"
+
+if [[ ${PV} == *9999* ]] ; then
+	inherit git-r3
+	EGIT_REPO_URI="https://github.com/LPCIC/${PN}.git"
+else
+	SRC_URI="https://github.com/LPCIC/${PN}/archive/v${PV}.tar.gz
+		-> ${P}.tar.gz"
+	KEYWORDS="~amd64"
+fi
+
+LICENSE="LGPL-2.1+"
+SLOT="0/${PV}"
+IUSE="+ocamlopt test"
+RESTRICT="!test? ( test )"
+
+RDEPEND="
+	>=dev-lang/ocaml-4.08.0:=
+	>=dev-ml/menhir-20211230:=
+	dev-ml/atd:=
+	dev-ml/ppx_deriving:=
+	dev-ml/ppxlib:=
+	dev-ml/re:=
+	dev-ml/stdlib-shims:=
+"
+DEPEND="${RDEPEND}"
+BDEPEND="
+	test? (
+		dev-ml/ANSITerminal
+		dev-ml/cmdliner
+	)
+"
+
+DOCS=( AUTHORS.md CHANGES.md ELPI.md INCOMPATIBILITIES.md README.md )
+
+src_install() {
+	dune_src_install
+	einstalldocs
+}
diff --git a/dev-lang/typescript/Manifest b/dev-lang/typescript/Manifest
index b70e9dccd04c3..22061c9cc58d5 100644
--- a/dev-lang/typescript/Manifest
+++ b/dev-lang/typescript/Manifest
@@ -1,3 +1,3 @@
-DIST typescript-4.9.5.tgz 11620433 BLAKE2B c253379a4aadd3fe16c93f27c5b450e5965c4c4de6841737c3489c74baa2cf8f8f5d9ca0414b5519e26eaac1db058e3826a3aa504bb450a89d36dce7e21b5f99 SHA512 d455e4f44d879be433650ef3f8c7098872f8356d45d84cccbbd36af62df301a1aa89b69fa98c02554e96c9602ec90451cce971a2ef31652c972c437ca0a8f6e2
 DIST typescript-5.0.4.tgz 7051452 BLAKE2B ed08425d8324a910f2d328fb02f27e08f75334fb190d1c4625452d076d615726d0e852da06f0f25146a4b02c6c99cd569bbcf7c50f5d6ff32c88a40101a59656 SHA512 716f53e56f71637edc73e8df127694bd7f757e8c6d1e4cdadcdc37c24a05e2c4a52a7d0c38d7647449dd8a0fea3c15973649a9961dcdcdac90cc2887338fe1ab
 DIST typescript-5.1.3.tgz 7147721 BLAKE2B 5a18d18bcbe702c82a108624c189e6b03d72f74e16ccf6af2448c71c1decfcc7995b53524472e106c19ef01ec95df772ccfeed3e76fad1eb59f29bbe42668fb0 SHA512 5c7eb6ec4f6f91eaa1959150b8bf94b3201712789b4f491647615638d96be2c4e3bf1c89627c9e7e0ae4c8408bccce4d7a798acd1032dab47f3a560b0351e467
+DIST typescript-5.1.5.tgz 7147776 BLAKE2B 6aa416a68b17b30de0203a33bf9cd14ee519f50e860bd745a92d7571b3565b1c98d9369037dc4fcd19a5c9080085d67aea91bebd53c08ff757e1f4ed6b6e5320 SHA512 14e1fe58dfc342352f37a5a05be738325df28b43c7f9affcabe90d21f45e86fd702e158e35e770f398aefaf437f56a78f48cd3244b19da5c8b5e9045ee6905d6
diff --git a/dev-lang/typescript/typescript-4.9.5.ebuild b/dev-lang/typescript/typescript-5.1.5.ebuild
similarity index 96%
rename from dev-lang/typescript/typescript-4.9.5.ebuild
rename to dev-lang/typescript/typescript-5.1.5.ebuild
index 7857fd2f036d3..598301d43b338 100644
--- a/dev-lang/typescript/typescript-4.9.5.ebuild
+++ b/dev-lang/typescript/typescript-5.1.5.ebuild
@@ -11,7 +11,7 @@ S="${WORKDIR}"/package
 
 LICENSE="Apache-2.0"
 SLOT="0"
-KEYWORDS="amd64 ~arm64 ~ppc64"
+KEYWORDS="~amd64 ~arm64 ~ppc64"
 
 RDEPEND="net-libs/nodejs"
 BDEPEND=">=net-libs/nodejs-16[npm]"
diff --git a/sci-mathematics/coq/Manifest b/sci-mathematics/coq/Manifest
index 5bad33b4b1a29..027218b7c9b5c 100644
--- a/sci-mathematics/coq/Manifest
+++ b/sci-mathematics/coq/Manifest
@@ -1,5 +1,5 @@
 DIST coq-8.12.0.tar.gz 6774001 BLAKE2B dc1d6adf9d4bd50d46007fbf5fd43d1ea97b6b226d89ad943419d4cb7df1439950c94b5e3cc614eb789103d1ab50535909d4ba2079eafc2caa4fd91db30e747d SHA512 8a64624c578ce0ab781fb3b1f162bd8b095735ad891fdad2fb7c40849afbdc7c1360187c6b62a5ef2982566f4c6c78029240c611ae769943a5250af300eb1240
-DIST coq-8.13.0.tar.gz 7010242 BLAKE2B bf9ec96b6698a2371be3164f65424a8ffb273252afc05e046267cae4265c1be71f89d0345f9e40ab3a93f5063080fd0224502cc0de808c7a0ddbb0edacab5fca SHA512 c355f0a9183f3669debd5f8f4ab96786215d0cccc37d1c2ac95a2d3c6115c8b0ee7ff7e23464b18444e2648ef3f8c221f0f3a28acf91199751cea2b74ee3fe8e
 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
diff --git a/sci-mathematics/coq/coq-8.13.0-r1.ebuild b/sci-mathematics/coq/coq-8.13.0-r1.ebuild
deleted file mode 100644
index 51731bcf5803b..0000000000000
--- a/sci-mathematics/coq/coq-8.13.0-r1.ebuild
+++ /dev/null
@@ -1,88 +0,0 @@
-# Copyright 1999-2023 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=7
-
-inherit desktop findlib
-
-MY_PV=${PV/_p/pl}
-MY_P=${PN}-${MY_PV}
-
-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="gtk debug +ocamlopt doc"
-
-RESTRICT="test"
-
-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}
-	doc? (
-		media-libs/netpbm[png,postscript(+),zlib(+)]
-		virtual/latex-base
-		dev-tex/hevea
-		dev-texlive/texlive-latexrecommended
-		dev-texlive/texlive-pictures
-		dev-texlive/texlive-mathscience
-		dev-texlive/texlive-latexextra
-		)"
-
-src_configure() {
-	ocaml_lib=$(ocamlc -where)
-	local myconf=(
-		-prefix /usr
-		-bindir /usr/bin
-		-libdir /usr/$(get_libdir)/coq
-		-mandir /usr/share/man
-		-coqdocdir /usr/$(get_libdir)/coq/coqdoc
-		-docdir /usr/share/doc/${PF}
-		-configdir /etc/xdg/${PN}
-	)
-
-	use debug && myconf+=( -debug )
-	use doc || myconf+=( -with-doc no )
-
-	if use gtk; then
-		if use ocamlopt; then
-			myconf+=( -coqide opt )
-		else
-			myconf+=( -coqide byte )
-		fi
-	else
-		myconf+=( -coqide no )
-	fi
-
-	use ocamlopt || myconf+=( -byte-only )
-
-	export CAML_LD_LIBRARY_PATH="${S}/kernel/byterun/"
-	./configure ${myconf[@]} || die "configure failed"
-}
-
-src_compile() {
-	emake STRIP="true" -j1 world VERBOSE=1
-}
-
-src_test() {
-	emake STRIP="true" check VERBOSE=1
-}
-
-src_install() {
-	emake STRIP="true" COQINSTALLPREFIX="${D}" install -j1 VERBOSE=1
-	dodoc README.md CREDITS
-
-	use gtk && make_desktop_entry "coqide" "Coq IDE" "${EPREFIX}/usr/share/coq/coq.png"
-}
diff --git a/sci-mathematics/coq/coq-8.17.1.ebuild b/sci-mathematics/coq/coq-8.17.1.ebuild
new file mode 100644
index 0000000000000..f634026e1cda6
--- /dev/null
+++ b/sci-mathematics/coq/coq-8.17.1.ebuild
@@ -0,0 +1,112 @@
+# 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 edo
+
+DESCRIPTION="Proof assistant written in O'Caml"
+HOMEPAGE="http://coq.inria.fr/
+	https://github.com/coq/coq/"
+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="debug doc gui +ocamlopt test"
+RESTRICT="!test? ( test )"
+
+RDEPEND="
+	dev-ml/zarith:=
+	|| (
+		dev-ml/num
+		<dev-lang/ocaml-4.09.0[ocamlopt?]
+	)
+	gui? (
+		>=dev-ml/lablgtk-3.1.2:3=[sourceview,ocamlopt?]
+		>=dev-ml/lablgtk-sourceview-3.1.2:3=[ocamlopt?]
+	)
+"
+DEPEND="${RDEPEND}"
+BDEPEND="
+	dev-ml/findlib
+	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
+	)
+	test? ( dev-ml/ounit2 )
+"
+
+DOCS=( CODE_OF_CONDUCT.md CONTRIBUTING.md CREDITS INSTALL.md README.md )
+
+src_prepare() {
+	# Remove failing tests. bug #904186
+	rm -r test-suite/coq-makefile/timing || die
+
+	default
+}
+
+src_configure() {
+	export CAML_LD_LIBRARY_PATH="${S}/kernel/byterun/"
+
+	dune_packages=(
+		coq-core
+		coq-stdlib
+		coqide-server
+		coq
+	)
+	use gui && dune_packages+=( coqide )
+
+	emake clean
+
+	local -a 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}
+		-native-compiler $(usex ocamlopt yes no)
+	)
+	use debug && myconf+=( -debug )
+	edob sh ./configure "${myconf[@]}"
+}
+
+src_compile() {
+	emake DUNEOPT="--display=short --profile release" VERBOSE=1 dunestrap
+
+	dune-compile ${dune_packages[@]}
+
+	use doc && emake refman-html
+}
+
+src_install() {
+	dune-install ${dune_packages[@]}
+
+	if use gui ; then
+		make_desktop_entry coqide "Coq IDE" "${EPREFIX}/usr/share/coq/coq.png"
+	fi
+
+	# Dune installs into /usr/<libdir>/ocaml/<coq> but
+	# Coq wants /usr/<libdir>/<coq> ; symlink those directories
+	local sym
+	for sym in ${dune_packages[@]} ; do
+		dosym $(ocamlc -where)/${sym} /usr/$(get_libdir)/${sym}
+	done
+
+	einstalldocs
+}
diff --git a/sci-mathematics/opensmt/Manifest b/sci-mathematics/opensmt/Manifest
index 5c761352c1a56..fcea9ccf21265 100644
--- a/sci-mathematics/opensmt/Manifest
+++ b/sci-mathematics/opensmt/Manifest
@@ -1,2 +1,2 @@
-DIST opensmt-2.4.3.tar.gz 1912077 BLAKE2B d945d5b85d81b9b991f2f881f2d8f160dbefad8ce6484cf0d28c9a35c0fa64d18f45442a59cdd45bd29fcf526a09717d902d30376dfe2784de2d4df9627f803b SHA512 a2adbbdebb133d7e97428c0ac9bf4c2413c95bca61567c5475f889f550904fc33a385712536c9026b38a1645b73c943876fa36724b634db061cb7cc0932543f2
 DIST opensmt-2.5.0.tar.gz 1940493 BLAKE2B ee643815b9da8bdc4a3a074a438eacdfde778347f4090aa7403e34859a9d51a17db8992c38a0e9f7a808384b0413abfbe2aa7b360dda44181344528159666945 SHA512 d70972eae376b927694f893ff9b6e4bfba7d0cfffe63545b5a0d582b594c3538643c9ae0121e75cf85aec3876eb4a45df2766c3a7700d07da05d1d6081953f42
+DIST opensmt-2.5.1.tar.gz 1943888 BLAKE2B 17b58fc3e693e77ce70835820f7361db9efe1cac561f1fa3480a839fbdf003d2566617cd97a3e2772ad8e890356b6a5761457779c0ac3b0841c2df6aee74946e SHA512 359ff968d7dbd8d94d6c5687d5b84e19c47016df5b1c0d80374743b395b6257cb4b97aa354b264103bd19c522f55912f1c938e646daf37f6b413488db917fc61
diff --git a/sci-mathematics/opensmt/opensmt-2.4.3-r2.ebuild b/sci-mathematics/opensmt/opensmt-2.5.1.ebuild
similarity index 96%
rename from sci-mathematics/opensmt/opensmt-2.4.3-r2.ebuild
rename to sci-mathematics/opensmt/opensmt-2.5.1.ebuild
index f46f590a012c0..479c6c7e252f9 100644
--- a/sci-mathematics/opensmt/opensmt-2.4.3-r2.ebuild
+++ b/sci-mathematics/opensmt/opensmt-2.5.1.ebuild
@@ -36,7 +36,7 @@ BDEPEND="
 	test? ( dev-cpp/gtest )
 "
 
-PATCHES=( "${FILESDIR}"/${P}-musl.patch )
+# PATCHES=( "${FILESDIR}"/${PN}-2.4.3-musl.patch )
 
 src_prepare() {
 	cmake_src_prepare