7 files changed, 229 insertions, 0 deletions
diff --git a/sci-mathematics/Manifest.gz b/sci-mathematics/Manifest.gz
index cf07c06f8c9c..08dd00a25a4b 100644
--- a/sci-mathematics/Manifest.gz
+++ b/sci-mathematics/Manifest.gz
diff --git a/sci-mathematics/easycrypt/Manifest b/sci-mathematics/easycrypt/Manifest
index 1b90ed5de2be..dae52c1a9845 100644
--- a/sci-mathematics/easycrypt/Manifest
+++ b/sci-mathematics/easycrypt/Manifest
@@ -1,3 +1,5 @@
 DIST easycrypt-2024.09.tar.gz 1310681 BLAKE2B cfe81762d4f4567473fc1f98c889145ed8c42f0a48b9e8089de8eca6c15f088d36c4eb7f4b4c4889b6444323b38a2ab17d0703cf97470ddf3084094a37436d69 SHA512 ce1554046c87fbeb27763ffd7a40fb0d8abc8bdedce6884e864968c23b31aee2c66108e52233d4dd1cb408a48b2ac3cba3ef46aee0963a5c21f3c2d1a843c308
+DIST easycrypt-2025.02.tar.gz 1362823 BLAKE2B d0a9739178b459e9f1288286f9a40bd45735d8a4d1acdcc322a079b2fc7712b1a9ffb655cfc67ae9384234981496218cd9dc8c7385d2954b3544a6339a8f98c7 SHA512 61d35a3e1bb2e91be94a52f3cc4c75e209a95908a6fc558472dab863b6d9d82f0a39bbe35ba98f6ce92eb398465013fdddd73bc99b789a55bcca6975c0d72196
 EBUILD easycrypt-2024.09.ebuild 990 BLAKE2B a7545b457ce9d8127c05e543dbc92931ffcef034eb590252eb7a0e24552b2067d4fa4daf498e02c2281e6aceec50f5eff647444873f376c476a04ecaa550657f SHA512 7ba58288c3f6229ec5a3c904a123017c516364696a9ffca2b88b1c00d4e8460999e7b53f6502ee523ae7c14cfc6aae1c99de61a921dfc5bcdc93b02480798cf2
+EBUILD easycrypt-2025.02.ebuild 993 BLAKE2B d77a3c1acda3c25ba0ae8bd77d81cc79a417ec0343f9cc784e333b29be71ef55a418d78cb23b656e52a2986d5882cbe01eb6496e2f3dfbbd7412ff2569fb2961 SHA512 0fef6f02d3bdcdffb753cad81540c8f3495128f0346e81e8ee8abac89efda1023710837a408f723fd013ddcfe5f1e78f085f19e91128557b733f2e1ded92a1bf
 MISC metadata.xml 799 BLAKE2B 967a758171a2fe87b648a29bf2663beaae7834119e55a7619c98518c96cfe459e59fe5dc72a9faea071c0b488dc8144f1c0e43677ac63646f1ba12cf831f4a88 SHA512 411ff1acad400c3e70e546fd59b20db13b0f1db121aca9f1af23da708cd82340114bc966f64cfb5a35e84967c1131c660ab260f867639932c67edf47c859c4ca
diff --git a/sci-mathematics/easycrypt/easycrypt-2025.02.ebuild b/sci-mathematics/easycrypt/easycrypt-2025.02.ebuild
new file mode 100644
index 000000000000..94f61fdf4523
--- /dev/null
+++ b/sci-mathematics/easycrypt/easycrypt-2025.02.ebuild
@@ -0,0 +1,50 @@
+# Copyright 1999-2025 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+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/r${PV}.tar.gz
+		-> ${P}.tar.gz"
+	S="${WORKDIR}/${PN}-r${PV}"
+
+	KEYWORDS="~amd64"
+fi
+
+LICENSE="MIT"
+SLOT="0/${PV}"
+IUSE="+ocamlopt"
+
+RDEPEND="
+	>=dev-lang/ocaml-4.08.0:=[ocamlopt?]
+	>=sci-mathematics/why3-1.8.0:=
+	dev-ml/batteries:=
+	dev-ml/camlp-streams:=
+	dev-ml/camlzip:=
+	dev-ml/dune-build-info:=
+	dev-ml/dune-site:=
+	dev-ml/num:=
+	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/flocq/Manifest b/sci-mathematics/flocq/Manifest
index 1ee6d7b79103..ca45d23ad40d 100644
--- a/sci-mathematics/flocq/Manifest
+++ b/sci-mathematics/flocq/Manifest
@@ -1,5 +1,7 @@
 DIST flocq-4.1.0.tar.gz 447412 BLAKE2B 1b993a0e86bd440602b16b94ed5aff4b95a3c732eca87c683d239702b285dee8eaaf7dad77f730ae4929bb24504e5fd12b9a181d48efac4c3db7f0606637c018 SHA512 677e0de1406b3c7e5504d114a5b18ec07c719bbad79a2cfb750ac309fd5ab09be5493afdb1786b5a188cece59fddcd4167e28bf3be4facbdea8fe3b11cdf1ab1
 DIST flocq-4.1.1.tar.gz 450132 BLAKE2B 00821a3e135156640320d1afd548bc1912953bba64cc675b7b6c94b4e3c792c444bfbb4ef1a3352adefa466548083e32c2b1e4b38747dcbc6ac6de6d72250a74 SHA512 7076b8d5e33b8225e0124b9f66f4e3e1ed3e30804c5bca28e30d5e176c1b8c5c3d777a28c243fada17ab4ed32f580c6d606b11f045d48f7acb15e03db59870c4
+DIST flocq-4.2.1.tar.gz 447822 BLAKE2B c91f3e51d28854b15c526634494377b07b76dfa0fdbeeb0a3c2c27a27152fc2dd1ef6908f434f4f3be76d9172acdd616a51bea97b937886a3bf64bac37fcba18 SHA512 73a93f1b7d7b0d1ad731a87c1fbf80d363cc479259059618170d488eb7ff2e101d4e3adf850796b3d20455c94ba093ad39d9ef80e3e03e53b20f6e9df1886736
 EBUILD flocq-4.1.0-r1.ebuild 802 BLAKE2B 70e7bb64272922f8e2408de98c662beb02b702a97cf51485f66dcd052e90f8207d9dbb2cadcc7b66f47dfde77a42a5d2f72c5d2088dc39e5208af109294dbc0f SHA512 2c5accf4fdda617c647252edff805bd04784c739d4a1c5c0d65b830edeac84355d8ad4231512d27fb5de7ab2c3d85b8e211c2caaf3a26809ff7c1f1b1822b0f2
 EBUILD flocq-4.1.1.ebuild 802 BLAKE2B 70e7bb64272922f8e2408de98c662beb02b702a97cf51485f66dcd052e90f8207d9dbb2cadcc7b66f47dfde77a42a5d2f72c5d2088dc39e5208af109294dbc0f SHA512 2c5accf4fdda617c647252edff805bd04784c739d4a1c5c0d65b830edeac84355d8ad4231512d27fb5de7ab2c3d85b8e211c2caaf3a26809ff7c1f1b1822b0f2
+EBUILD flocq-4.2.1.ebuild 807 BLAKE2B 83535fe70ab5a08a4198a47840ce2f52c3d1fa944537ba7d33a07dae44732c4140ea1c8c31407c4026bc1a506e88eb182d503fc9248ad45b20d860cc6d1b0417 SHA512 ed9aaee9055415f7762498416f546f224de30561625b0fe98bf49c10cad36e214216e3539fab2f39e96b8096d40889d3982b4242a2bb6a9bda5f68eabf0ed1c3
 MISC metadata.xml 685 BLAKE2B aa5fae67335fe3a4919e89654c550462d454586b6892aabd3d05940f2250d9368cc0195f1a761a8faf92245e8415711c99e28b6547a2c22c893a47f02aad4e89 SHA512 f2d195f05014e269699198abfa7c214a9ded40a635e32ff94b2d2d5c915d23a0664851118942c9e38b945721295aae2c80299f7370b8a2c2bbb4325b32bb8259
diff --git a/sci-mathematics/flocq/flocq-4.2.1.ebuild b/sci-mathematics/flocq/flocq-4.2.1.ebuild
new file mode 100644
index 000000000000..558a3dd17f20
--- /dev/null
+++ b/sci-mathematics/flocq/flocq-4.2.1.ebuild
@@ -0,0 +1,39 @@
+# Copyright 1999-2025 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+inherit multiprocessing
+
+DESCRIPTION="Formalization of floating-point arithmetic for the Coq proof assistant"
+HOMEPAGE="http://flocq.gforge.inria.fr/
+	https://gitlab.inria.fr/flocq/flocq/"
+SRC_URI="https://flocq.gitlabpages.inria.fr/releases/${P}.tar.gz"
+
+LICENSE="LGPL-3"
+SLOT="0"
+KEYWORDS="~amd64 ~x86"
+
+RDEPEND="
+	dev-lang/ocaml:=
+	>=sci-mathematics/coq-8.15:=
+"
+DEPEND="
+	${RDEPEND}
+"
+
+# Do not complain about CFLAGS etc since ML projects do not use them.
+QA_FLAGS_IGNORED='.*'
+
+src_compile() {
+	./remake --jobs=$(makeopts_jobs) || die
+}
+
+src_install() {
+	DESTDIR="${D}" ./remake install || die
+
+	dodoc AUTHORS INSTALL.md NEWS.md README.md
+
+	insinto "/usr/share/${PN}"
+	doins -r examples
+}
diff --git a/sci-mathematics/why3/Manifest b/sci-mathematics/why3/Manifest
index f2ec969686e3..2a6a677eb317 100644
--- a/sci-mathematics/why3/Manifest
+++ b/sci-mathematics/why3/Manifest
@@ -1,6 +1,8 @@
 AUX why3-1.7.2-signum.patch 406 BLAKE2B ab81e95db7537a31fd75e3d0551ee57cf664aa6f41779c2d72100b39c88ca0f3a90fa517e07dd1f17c3f93fff134802cb1e3fa192e15b66b8163e840c1e75dd8 SHA512 3491b58cc54bfdd8601242b2f78d7a8afbed8097758610dd38815e8ed90cf462d02ded16905838a51275fd16ed634f89ba11e38a8d573c78ca01477fcfa35237
 DIST why3-1.6.0.tar.gz 6850062 BLAKE2B 91db6f67a9d0fe24b7d7d18e6c5e9cd362563a55702bfb28c478754f53e831beb3033adde251214facd8d64ab923389b0b9fe7b240b6cd09f0b4b3e6f8eca143 SHA512 60d61b8337ab9f2fd2e6c7174eb0bab063f122417738cd75990c5c53120dd535bcedccb670567f5753853d6bc9f8efebb563d079e4d368372a7687193f1346b1
 DIST why3-1.7.2.tar.gz 7005562 BLAKE2B cd1b25e35147a319e5d5d1f1380ecfaa3555624c797459e8df5cb3b1558928d9c02b567645a2f2952b877c7135a5a393f4b734dd35e569bea6e6b073708901ce SHA512 7e80671480ce0dc3c69514bea2836f5899c686b43a4e8607c27d28e63f78150150dc45fcac5760dbee9721d363e456b1dcaeb1501fc9f63f360722a1021f675f
+DIST why3-1.8.0.tar.gz 7373730 BLAKE2B c650d0578c6ae28f01872f01ba2c6e58ebf00c8fc87f4040f51430aad6b94b52f031b17d5b75178a6a6d5f254f3d42dbbdb031f676335a2d896021c0663192a9 SHA512 8d30ac4a1280a7d7741ef862365e06aa3218a78fd01ca7f969f0d6515245c7259fcc81897bfe08c581c6b37639d1465ab4a96657f3baf4c747988df8201d4549
 EBUILD why3-1.6.0.ebuild 2349 BLAKE2B 946115ce4d70ed1505fb3072c7ad6e67c6c3ea0c97a03dd6141b069ef8b2502f43e44717ff9f3dbc5c4de367fb25d7dbd98369f8313ff75ba0471f35c320df04 SHA512 8a196dfa7a161c980e2023f1363d6ff91af3ca854e96539ca44d004efa2b5d813b480c79dd0d51e31796a0c0b6f886d094bd06751469dd8b236aad239ddaf1f7
 EBUILD why3-1.7.2.ebuild 2410 BLAKE2B 00e650a1716213d2be02c98e07157d44311996a6faf64c52193f7bbe1dcf16dde133a81468cc36e950a48c0891100096119960323b0045a79ae068599c6685b3 SHA512 aa928c405d247f6462b2e2571f5efe2e01993034d6515d6f0c4a3bb847fb352f319621ec1d31ffb3e6f8336cc32372cb6170e621bf9507e71866c5b1dddfd612
+EBUILD why3-1.8.0.ebuild 2764 BLAKE2B 1380a104d899b427a4009cf4ac38bfe813c802a1dede77666efafe8021eb259d1ee49ef9a49da345e2dc912ce308fb467641c85018fe8c8396eeb5381519f13d SHA512 6452354cb1a3f30541e2e50fbec3f307985af70ecee63cea2ddac9c51ef6d760e294eea21b24336150cfc8aa0ebd76c8c4fcebf7c568422c90ff58bb35a11c8f
 MISC metadata.xml 1902 BLAKE2B 1868834e446b471f4b3f7b11fc987661dee83790110fa31c73f0060fd8340891ff85ec16591d1326977760c726ec04bd06a4cca46fb1a87f792340a002cba247 SHA512 4dc9408d44eafc037bfce9c996570e58c161e07c3ded2a052954c834fcf8c3a36cf8429493bc705ced7445d199eaf207cabb5df1b0ed6b625015af518e55d9e9
diff --git a/sci-mathematics/why3/why3-1.8.0.ebuild b/sci-mathematics/why3/why3-1.8.0.ebuild
new file mode 100644
index 000000000000..7d4c10c81bae
--- /dev/null
+++ b/sci-mathematics/why3/why3-1.8.0.ebuild
@@ -0,0 +1,134 @@
+# Copyright 1999-2025 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://www.why3.org/"
+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 zip"
+
+RDEPEND="
+	!sci-mathematics/why3-for-spark
+	>=dev-lang/ocaml-4.05.0:=[ocamlopt?]
+	>=dev-ml/menhir-20170418:=
+	dev-ml/num:=
+	dev-ml/zarith:=
+	coq? (
+		>=sci-mathematics/coq-8.15:=
+		>=sci-mathematics/flocq-4.2.1
+	)
+	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?] )
+	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() {
+	rm configure || die
+	mv configure.in configure.ac || die
+
+	sed -e 's/configure\.in/configure.ac/g' \
+		-i 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
+
+	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
+
+	# Bad var replacement.
+	sed -e 's|\$(OCAMLC -|\$(ocamlc -|g' \
+		-i configure \
+		|| die
+}
+
+src_configure() {
+	local -x OCAMLC="ocamlc"
+
+	local -a myconf=(
+		--enable-verbose-make
+
+		--disable-frama-c
+		--disable-hypothesis-selection
+		--disable-infer
+		--disable-isabelle-libs
+		--disable-java
+		--disable-js-of-ocaml
+		--disable-pvs-libs
+		--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)
+		$(use_enable stackify)
+		$(use_enable zip)
+	)
+	econf "${myconf[@]}"
+}
+
+src_compile() {
+	emake
+
+	if use doc ; then
+		emake doc
+	fi
+}
+
+src_install(){
+	findlib_src_preinst
+	emake DESTDIR="${ED}" install install-lib
+
+	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
+}